| 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)
|
|---|
| 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.
|
