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

• Project/Area Number: 16016279
• Research Category: Grant-in-Aid for Scientific Research on Priority Areas
• Allocation Type: Single-year Grants
• Review Section: Science and Engineering
• Research Institution: Hosei University
• Principal Investigator: 劉 少英 法政大, 情報科学部, 教授 (90264960)
• Project Period (FY): 2004 – 2005
• Project Status: Completed (Fiscal Year 2005)
• Budget Amount: ¥5,000,000 (Direct Cost: ¥5,000,000); Fiscal Year 2005: ¥2,600,000 (Direct Cost: ¥2,600,000); Fiscal Year 2004: ¥2,400,000 (Direct Cost: ¥2,400,000)
• Keywords: ソフトウェアシステム / ソフトウェア検証 / ソフトウェアレビュー / 形式的手法 / ソフトウェア工程 / ソフトウェア分析 / ソフトウェアテスト / ソフトウェア開発

Research Abstract

平成16年度には、ソフトウェアシステムの機能仕様とプログラムの整合性(consistency)と正当性(validity)を検証する厳密なレビュー技術の自動化方法の確立及びその方法を支援するツールの開発のために、以下の具体的な研究を行った。第一、検証すべき性質を形式的仕様から自動的に抜き出すアルゴリズムと支援ツールを開発した。第二、レビュータスク木と仕様テスト技術を統合してレビュープロセスを確立し、その技術を支援するツールを構築した。第三、プログラムは形式的設計仕様を満たすかどうかを検証するために、機能定義と実行パスの関係に基く仕様によるプログラムをレビューする方法を確立し、その方法の有効性を評価するために、銀行のATMシステムに応用することによりレビューの実験を行い、実験の結果を分析、その方法の有効性を確立した。第四、仕様によるプログラムをレビューする方法を高効率に支援するために、支援ツールを開発した。そのツールによりプログラムのレビューを行うには、仕様に定義された機能をプログラムで実装されたかどうかを検証だけでなく、定義されてないプログラムコードの正しさも検査できる。更に、以上の研究でソフトウェア検証の新たな課題も発見し、今後の研究を展開するには役に立つ材料を獲得した。

Research Products

• [Journal Article] An Automated Rigorous Review Method for Verifying and Validating Formal Specifications (2004)
  • Author(s): Shaoying Liu
  • Journal Title: Second International Symposium on Automated Technology for Verification and Analysis LNCS3299 Pages: 15-19
• [Journal Article] An Investigation of the Approach to Specification-based Program Review through Case Studies (2004)
  • Author(s): Fumiko Nagoya, Shaoying Liu, Yuting Chen
  • Journal Title: 9th IEEE International Conference on Engineering of Complex Computer Systems April Pages: 249-258
• [Journal Article] An Approach to Detesting Domain Errors Using Formal Specification-based Testing (2004)
  • Author(s): Yuting Chen, Shaoying Liu
  • Journal Title: 11th Asia-Pacific Software Engineering Conference December Pages: 276-283
• [Journal Article] An Approach to Integration Testing Based on Data Flow Specifications (2004)
  • Author(s): Yuting Chen, Shaoying Liu, Fumiko Nagoya
  • Journal Title: 1st International Colloquium on Theoretical Aspects of Computing September Pages: 405-419
• [Journal Article] A Framework for Developing Dependable Software Systems Using the SOFL Method (2004)
  • Author(s): Shaoying Liu
  • Journal Title: 1st Workshop on Dependable Software February Pages: 131-140
• [Book] Formal Engineering for Industrial Software Development Using the SOFL Method (2004)
  • Author(s): Shaoying Liu
  • Total Pages: 408
  • Publisher: Springer-Verlag