2001 Fiscal Year Final Research Report Summary
Development of Formal Specification Language for Writing Specifications as Components Based on Functions
| Project/Area Number |
10558043
|
|---|
| 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 Advanced Institute of Science and Technology, School of Information Science, Professor, 情報科学研究科, 教授 (50251971)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
OGATA Kazuhiro Advanced Institute of Science and Technology, School of Information Science, Research Associate, 情報科学研究科, 助手 (30272991)
WATANABE Takuo Advanced Institute of Science and Technology, School of Information Science, Associate Professor, 情報理工学研究科, 助教授 (20222408)
|
|---|
| Project Period (FY) |
1998 – 2001
|
| Keywords | components / reliable / support tool / CafeOBJ / module system / specifications / distributed (real-time) systems / verification |
|---|
| Research Abstract |
In this research, we have used the specification language CafeOBJ having several machineries for writing specifications as components. CafeOBJ is the algebraic specification language that has been developed by mainly the head investigator. It can be used to spepify objects in object-orientation and abstract machines as well as abstract data types. The powerful module system that CafeOBJ has also helps write specifications as components.
What we have done are as follows :
Verification : Safety critical systems affecting human lives such as railroad signaling systems, air-traffic control systems, patient monitoring systems, etc. are typically distributed (real-time) systems. We have developed and proposed a method for verifying those systems with the help of the CafeOBJ system. Several case studies that we have done show its usefulness.
Support Tool : We have developed a foundation for developing, reliable software by combining components. We have also designed and implemented a support tool for making software according to the foundation
|
