形式的仕様とプログラムの厳密なレビューの自動化についての研究

2003 年度 実績報告書

• 研究課題/領域番号: 15017280
• 研究機関: 法政大学
• 研究代表者: 劉 少英 法政大学, 情報科学部, 教授 (90264960)
• キーワード: 厳密なレビュー / 形式的仕様の検証 / 仕様に基くプログラムレビュー / 形式的仕様記述技術 / ソフトウェア分析 / テスト / 形式工学手法 / ソフトウェア工学

研究概要

平成15年度には、ソフトウェアシステムの機能仕様及びプログラムの正確性を検証する厳密なレビュー技術を確立するために、以下の具体的な研究を行った。第一、検証すべき性質からレビュータスク木(review task tree)を自動生成するために必要なルール及びそのルールの正確性を確立した。基本的には、それらのルールが、一階述語論理を基く、レビューの分割統治法の原理を応用することによる形成されたものである。生成されたレビュータスク木は、検証すべき性質とその分品間の関係を示すだけでなく、レビュータスクの順番も定義する。従って、レビューする目標が明確になる。第二、レビューのプロセスを容易に成されるために、レビュータスク木とテスト技術を統合してレビュープロセスを支援する技術を開発した。この技術は、幾つかのテストケースを生成する基準を含め、様々な種類の論理式の真値を判断できる細かく基準も定義した。第三、レビュー・タスク木技術を支援するために、プロトタイプツールを開発した。このツールでは、論理式で表している形式的な性質から、その性質の正確性を検証するために必要なレビュータスク木を自動的及び手動的に生成することができる。生成されたタスク木の中のそれぞれのタスクの正確性を検証するときに、ツールによる、検証するタスクを決められ、そのタスクを容易にレビューすることができる。それぞれのタスクのレビュー結果により、ツールはトプレベールタスクの正確性を自動的に決めることができる。第四、プログラムの正確性の検証に関しては、「形式的仕様から要求された機能を抽出」、「プログラムからパスを抽出」、「機能とパスの対応関係を構築」、及び「機能に対して、各パスの正確性をレビューする」の四つのステップから構成されたレビュープロセスを定義し、各セデップのタスクを完成するために必要な詳細な技術を開発した。第五、プログラムを容易にレビューできるために、レビュープロセスの支援ツールを開発した。そのツールによる、プログラムから制御の流れ図(control flow diagram)を自動的に生成、図の中のそれぞれの文とプログラムの中の同じ文に自動的に連結、図から自動的にプログラムパスを生成、更に、各パスの正確性をレビューすることによる、プログラム全体の正確性に自動的に決めることができる。

研究成果

• [文献書誌] Sirin Bekbay, Shaoying Liu: "A Study of Japanese Software Process Practices and a Potential for Improvement Using SOFL"Third International Conference on Quality Software (QSIC2003), IEEE Computer Society Press, Dallas, Texas, USA. November 6-7. 100-107 (2003)
• [文献書誌] Jeff Offutt, Shaoying Liu, Aynur Abdurazik, Paul Ammann: "Generating Test Data from State-Based Specifications"Journal of Software Testing, Verification and Reliability, John Wiley & Sons, Ltd. No.13. 25-53 (2003)
• [文献書誌] Shaoying Liu: "An Approach to Transforming Visual Formal Specifications to Java Programs (extended version)"The Journal of Three Dimensional Images. 17・1. 121-128 (2003)
• [文献書誌] Shaoying Liu: "Utilizing Specification Testing in Review Task Trees for Rigorous Review of Formal Specifications"Proceedings of Asia-Pacific Software Engineering Conference (APSEC03), IEEE Computer Society Press. December 10-12. 510-519 (2003)
• [文献書誌] Shaoying Liu: "A Property-Based Approach to Reviewing Formal Specifications for Consistency"Proceedings of 16th International Conference on Software & Systems Engineering and Their Applications, Paris, France. December 2-4. 1/6-6/6 (2003)
• [文献書誌] Wuwei She, Shaoying Liu: "Formalization, Testing and Execution of a Use Case Diagram"5th International Conference on Formal Engineering Methods (ICFEM2003), LNCS, Springer-Verlag, Singapore. November 5-7. 68-85 (2003)
• [文献書誌] Xiaolei Gao, Huaikou Miao, Shaoying Liu, Ling Liu: "The Availability Semantics of Predicate Data Flow Diagrams"Second International Workshop on Grid and Cooperative Computing (GCC2003), LNCS, Springer-Verlag, China. December 7-10. 1426-1433 (2003)
• [文献書誌] Yuting Chen, Shaoying Liu: "SOFL Specification-Based Testing (short paper)"Proceedings of 10th Workshop on Foundation of Software Engineering (FOSE 2003) Wakayama Prefecture. November 13-15. 129-132 (2003)
• [文献書誌] Shaoying Liu: "Formal Engineering for Industrial Software Development using the SOFL Method"Springer-Verlag. 428 (2004)