| 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
|
| Project Status |
Completed (Fiscal Year 2002)
|
| Budget Amount *help |
¥14,600,000 (Direct Cost: ¥14,600,000)
Fiscal Year 2002: ¥3,600,000 (Direct Cost: ¥3,600,000)
Fiscal Year 2001: ¥3,500,000 (Direct Cost: ¥3,500,000)
Fiscal Year 2000: ¥3,400,000 (Direct Cost: ¥3,400,000)
Fiscal Year 1999: ¥4,100,000 (Direct Cost: ¥4,100,000)
|
|---|
| 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.
|
