| 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)
ディアコネスク ラズウ゛ァ 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (30293393)
|
|---|
| Project Period (FY) |
1998 – 2001
|
| Project Status |
Completed (Fiscal Year 2001)
|
| Budget Amount *help |
¥12,700,000 (Direct Cost: ¥12,700,000)
Fiscal Year 2001: ¥2,800,000 (Direct Cost: ¥2,800,000)
Fiscal Year 2000: ¥3,100,000 (Direct Cost: ¥3,100,000)
Fiscal Year 1999: ¥3,000,000 (Direct Cost: ¥3,000,000)
Fiscal Year 1998: ¥3,800,000 (Direct Cost: ¥3,800,000)
|
|---|
| Keywords | components / reliable / support tool / CafeOBJ / module system / specifications / distributed (real-time) systems / verification / 機能的性質 / 非機能的性質 / 代数仕様 / ソフトウェア発展 / 射影型振舞仕様 / 詳細化検証 / 木アーキテクチャ / オブジェクト指向 / 形式仕様 / 振舞い仕様 / 方法論 / 閲覧システム / 形式仕様言語 / 代数モデル / UML / 振舞仕様 |
|---|
| 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
|
