2002 Fiscal Year Final Research Report Summary
A Study on Verification of Software Components in Object-Based Distributed Environments
| Project/Area Number |
11480067
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
FUTATSUGI Kokichi JAIST, School of Information Science, Professor, 情報科学研究科, 教授 (50251971)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
AMANO Noriki JAIST, School of Information Science, Associate, 情報科学研究科, 助手 (30313703)
MORI Akira JAIST, School of Information Science, Associate (AIST , Researcher, now), グループリーダ (30311682)
|
|---|
| Project Period (FY) |
1999 – 2002
|
| Keywords | components / algebraic specification / CafeOBJ / PigNose / formal methods / verification / resolution / high-assurance software |
|---|
| Research Abstract |
We have developed base technologies with which we can formally verify that given components meet their specifications and the software tool supporting the technologies. It will be necessary to develop such technologies for the software industry in the coming years. We have used CafeOBJ, an algebraic specification language and system, with a variety of functionalities that make is possible to write specifications as components. CafeOBJ is also suitable for abstract machines as well as abstract data types, and provides strong module facilities. Some concrete outcomes in this study are as follows : 1. Design and development of a theorem prover : the resolution engine PigNose that resolves CafeOBJ term denoting first-order predicate formulas has been incorporated into the CafeOBJ system. We have confirmed its usefulness by applying it to some examples. 2. Development methodology based oil components : we have made foundation for developing high-assurance software by putting together software components. 3. Verification case studies : we have applied the verification method based on CafeOBJ to several reliable systems such as railroad signaling systems and security systems and confirmed its usefulness.
|
