ソフトウェア開発の形式的な発展手法

点击翻译按钮获取中文摘要

本プロジェクトの目的は、品質と信頼性の高いソフトウェアを開発するための実用的及び形式的な発展手法(evolution approach)に関する研究を行なうことである。当初の研究計画の実現に向けて,平成10年度は,以下の研究を遂行した.1. 形式的仕様を求精する既存なルールを検討し、ソフトウェア発展のためのルールを提案した。このルールでソフトウェアを漸増的に発展することの検証ができる。さらに、このルールと既存な求精のルールの関係も検討して確立した。本研究に関して,以下の論文を発表した.“An Evolution Approach for Software Development Using SOFL Methodology",in Proceedings of International Workshop on Software Evolution Process.2. SOFLという形式的仕様言語で鉄道の踏切制御システムの仕様書を作成した.このシステムは,直接,人命に係るために,絶対的な信頼性を要求される安全性が必須な(Safety Critical)システムである.これらの応用事例に適用した結果に基づき,SOFL言語及び,SOFL方法論のソフトウェア発展に関する部分を改良し、実用的な方法論を確立した。本研究に関して,以下の論文を発表した.“Applying SOFL to Specify A Railway Crossing Controller for Industry",in Proceedings of WIFT'98.3. ソフトウェア発展の一つ有効な方法は部品に基ずく(component-based)開発方法である。部品を使ってより複雑な部品を構成する手法及び作成した新しい部品の正しさを検証するルールを研究した。本研究に関して,以下の論文を発表した.“Interacting Frameworks for Catalysis",in Proceedings of Second IEEE International Conference on Formal Engineering Methods.4. ソフトウェア発展の一つ重要なことは、発展した仕様又は設計の無矛盾及び有効性の検証である。形式的証明とプログラムテストの技術を結合し、仕様又は設計の以上の二つ性質を検証する有効的な「仕様テスト」という方法を提案した。本研究に関して,以下の論文を投稿した.“Verifying Consistency and Validity of Formal Specifications by Testing",Formal Methods Congress'99.