| 研究概要 |
大規模ソフトウェアの設計においては,システムを複数のモジュールに分解し,モジュールごとに入出力の満たすべき/果たすべき役割仕様をフォーマルに定めるDesign by Construct DbCがB.Meyerによって大事だと提唱されている.本研究ではDbCに基づき記述したプログラムモジュールの仕様とそれを実装した関数型プログラムに対し,後者が前者を満たすことを形式的に保証するための検証方法を,申請者の従来の研究成果を踏まえて考案し,その有用性を,考案した手法に基づく検証支援系の試作と検証実験を通じて,評価することを目的とする.本年度は以下の研究を行った.(1)Javaコードに仕様記述のためのアサーションを記述支援する方法論を提案し有用性を示した.この方法論は従来の動的解析方法と静的解析方法を組みあわせて有効なアサーション導出を行うものである.この研究ではjavaを対象としたが,静的解析の方法論は関数型プログラムに応用が可能と考える.
(2)ソフトウェアの上位設計に対して,いくつか満たすべき性質を与え,モデル検査を支援する方法論を提案し,その有用性を示した.ソフトウェアの対象としてWEBアプリケーションを対象と限定するかわりに,効率的にモデル検査するためにモデル検査用のモデルを自動導出する方法論を与えた.またソフトウェアの仕様記述法として標準的なUMLで記述された複数の上位設計記述間の無矛盾性を保証するための方法論を2つ発表した.後者については関数田プログラムへの適用を今後考えて生きたい.(3)モデル検査の応用として無線ネットワークのパラメータ設定に応用する研究を国際会議と学術論文にまとめた.(4)関数型プログラムのモジュール指向定理証明支援システムについては,今年度.net framework上で支援系を実装を鋭意行った.実装結果と例題検証の結果を近日中に研究会に発表予定である.
|
