| Project/Area Number |
11680368
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| 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)
|
|---|
| Project Period (FY) |
1999 – 2001
|
| Project Status |
Completed (Fiscal Year 2001)
|
| Budget Amount *help |
¥2,800,000 (Direct Cost: ¥2,800,000)
Fiscal Year 2001: ¥900,000 (Direct Cost: ¥900,000)
Fiscal Year 2000: ¥900,000 (Direct Cost: ¥900,000)
Fiscal Year 1999: ¥1,000,000 (Direct Cost: ¥1,000,000)
|
|---|
| Keywords | Software reviews / Fault tree analysis / Design reviews / Specification testing / Formal verification / Formal specification / Formal engineering methods / Formal methods / 形式的工学手法 / ソフトウェア検証 / 厳密なレビュー / 仕様分析 / 形式的仕様 / システム進化 / テスト / 形式的証明 / 仕様テスト / 形式的仕様言語 / ソフトウェア信頼性 / SOFL / テスト支援環境 |
|---|
| Research Abstract |
We have conducted intensive research to explore rigorous techniques for verifying formal specifications and designs of software systems, and achieved several important results. Firstly, we have combined formal verification and the fault tree analysis technique to establish a rigorous reviews method. By this method, proof obligations for various properties of a specification are automatically derived from the specification, and then a review plan is automatically generated and represented graphically. By reviewing the tasks in this graphical representation, we can check whether the specification has faults or not. Secondly, 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. Finally, we have built a prototype of software tool to support specification testing and conducted a case study to evaluate the effectiveness of our testing method.
|
