| Project/Area Number |
11694173
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Hosei University (2000-2001)
Hiroshima City University (1999) |
|---|
Principal Investigator |
SHAO-YING Liu Hosei University, Faculty of Computer and Information Sciences, Professor, 情報科学部, 教授 (90264960)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
OHBA Mitsuru Hiroshima City University, Department of Computer Science, Professor, 情報科学部, 教授 (50264966)
ARAKI Keijiro Kyushu University, Graduate School of Information Science and Communication Engineering, Professor, 大学院・システム情報科学研究院, 教授 (40117057)
TAMAI Tetsuo Tokyo University, Interfaculty Initiative in Information Studies, Professor, 教養学部, 教授 (60217172)
ARAI Noriko National Institute of Informatics, Associate Professor, 情報学基礎研究系・情報数理研究部門, 助教授 (40264931)
|
|---|
| Project Period (FY) |
1999 – 2001
|
| Project Status |
Completed (Fiscal Year 2001)
|
| Budget Amount *help |
¥8,900,000 (Direct Cost: ¥8,900,000)
Fiscal Year 2001: ¥2,300,000 (Direct Cost: ¥2,300,000)
Fiscal Year 2000: ¥3,100,000 (Direct Cost: ¥3,100,000)
Fiscal Year 1999: ¥3,500,000 (Direct Cost: ¥3,500,000)
|
|---|
| Keywords | Formal engineering methods / SOFL / Formal method / Formal specification / Rigorous review / Specification testing / Software engineering / Software tools / Object-Oriented Design / 形式工学手法 / ソフトウェア検証 / 厳密なレビュー / 仕様テスト / 仕様分析 / 形式的仕様 / システム開発 / ソフトウェア進化 / 形式的工学手法 / ソフトウェアテスト / 形式的検証 / ソフトウェア開発環境 / ソフトウェア分析 |
|---|
| Research Abstract |
We have achieved several important results on this project. Firstly, we have developed the SOFL specification language and method into a mature level and completed a book on the introduction to the latest development of SOFL. Secondly, we have developed a rigorous reviews technique by integrating formal proof and fault tree analysis, which supports systematically rigorous reviews of SOFL specifications and other kinds of formal specifications. Thirdly, we have developed an effective testing method for verifying and validating formal specifications, including both explicit and implicit specifications (e.g., with pre and post-conditions), by integrating program testing technique and formal proof approach. By this method formal specifications can be verified and validated before they are implemented. Fourthly, we have explored the power of formal refinement in capturing complete and accurate user requirements, which demonstrates the potential effectiveness in improving the productivity and reliability of software products, finally, we have investigated how formal methods can be used to define, predicate, and control software processes. Our results achieved on this project have contributed to the establishment of Formal Engineering Methods as a new research area.
|
