1997 Fiscal Year Final Research Report Summary
Formal Methods and Intelligent Software Engineering Environments
| Project/Area Number |
08044167
|
|---|
| Research Category |
Grant-in-Aid for international Scientific Research
|
| Allocation Type | Single-year Grants |
|---|
| Section | Joint Research |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Hiroshima City University |
|---|
Principal Investigator |
LIU Shaoying Hiroshima City University, Computer Science, Associate Professor, 情報科学部, 助教授 (90264960)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
HINCHEY Michael New Jersey Institute of Technology, Computer Science, Professor, 情報科学部, 教授
HO-STUART Chris Queensland Univ.of Technology, Computer Science, Lecturer, 情報科学, 講師
SUN Yong The Queen's Univ.of Belfast, Computer Science, Lecturer, 情報科学部,, 講師
OFFUTT A Jeff George Mason Univ., Information and Systems Engineering, Associate Professor, 情報科学部,USA, 助教授
ARAKI Kejiro Kyushu University, Information Eng., Professor, 大学院・システム情報科学研究科, 教授 (40117057)
|
|---|
| Project Period (FY) |
1996 – 1997
|
| Keywords | Formal Methods / Formal Specification / Software Engineering Environments / Software Verification / Software Testing / Rigorous Reviews / Formal Semantics / SOFL |
|---|
| Research Abstract |
We have made substantial progress towards the goals of the FM-ISEE project taht are to develop a more powerful, user-friendly and practical formal method for developing raliable software systems than those currently existing, and to conduct research on the construction of an intelligent software engineering environment to support the formal methods. In the fiscal year of 1997 we have achieved the following specific results :
1. The practical formal method SOFL is designed and improved.
2. Both the existing formal method Z and the proposed SOFL are applied to complicated information systems and the results are compared and evaluated.
3. "Formal Engineering Methods" are proposed and developed to provide an new, Practical approach to applying formal methods in industry at large. compared with formal methods, formal engineering methods offer three progresses : (1) integrate graphical notation, natural languages, and formal notation for specifications ; (2) emphasize evolution approach rather than the existing refinement approach for transforming specifications ; and (3) substitute formal proofs with rigorous reviews for system verification and validation.
4. Specification testing and specification-based testing techniques are investigated. These two techniques are intended to solve different problems. The former aims to verify and validate formal specifications while the latter aimes to ensure that the programs implemented based on the specifications satisfy the specifications and the user requirements.
5. To help the construction of a complier and support environment for SOFL,the axiomatic semantics and operational semantics of SOFL are defined.
6. The prototypes of the graphical user interface and spedification testing support tool for SOFL are built. Eight (8) papers are published in the refereed journals and internationals based on the above research.
|
