Supporting Planning and Refactoring of Refinement Structure of Event-B Models

(邦訳:Event-Bモデルの詳細化構造の計画とリファクタリングの支援手法)
 
小林 努
国立情報学研究所 コンテンツ科学研究系 特任研究員

[背景]システムを多段階の抽象度で厳密にモデル化・分析する手法が有用
[問題]
どのような抽象化を行うかの計画・変更が難しい
[貢献]
計画・変更手法を提案し,開発コスト削減・再利用性向上

 高信頼なソフトウェアシステムの構築のために,プログラムコードを書く前に,システムの仕様を数学的表現でモデル化し検証する手法が提案されてきた.中でも近年注目されている手法Event-Bでは,厳密なモデルを,その複雑さを複数段階に分散しつつ構築・検証できる.

 Event-Bでは,まずシステムの一部の要件だけに関する抽象的なモデルを構築し,後で他の要件を追加した具体的なモデルを改めて構築し,抽象・具体モデル間の整合性を検証することを繰り返す.このように異なる抽象度のモデルを別々に作るため,開発者は各段階でシステムのどの要素・要件を含めるか(以下,詳細化構造と呼ぶ)を決定できる.各段階のモデルの内容は詳細化構造次第で大きく変わるため,詳細化構造はモデル構築・検証の複雑さやモデルの保守・発展性に強く影響する.

 Event-Bを開発に適用する際には以下の問題がある.まず,Event-Bモデルは一度構築された後にも利用される.構築されたモデルは保守・改良され,また他のモデルの構築のために既存のモデルを再利用する需要も高い.しかし,モデルを構築後に大きく変更してその後の利用に役立てる研究は行われていない.また,開発者はモデルの構築前に詳細化構造の計画を立てる必要があるが,直観に従って計画すると,整合性のないモデルや,詳細化機構を活かし切れない複雑なモデルを構築してしまうことが多い.しかし,対象システムの要件の依存関係が入り組んでいるため,整合性や複雑さの軽減を考慮した計画立案は困難である.

 既存手法では詳細化構造は明示的に扱われていなかったが,本研究では詳細化構造が上記の問題の解決に重要と考え,詳細化構造を定義し,以下の手法を提案した.

 まず,元のモデルの内容と整合性を保ったままその詳細化構造を再構成する手法を提案した.提案手法は,元のモデルと整合性があり,一部の要素だけで記述されたモデルの構築を補助することで,詳細化の分割を補助する.また,複数段階を1段階にまとめる詳細化の合成も提案した.ケーススタディでは,提案手法により各段階を分割して理解や証明の容易性を上げ,また,汎用的な要素に関する記述を抽象モデルとして抽出して再利用性を上げた.

 さらに,望ましい詳細化構造を計画する手法を提案した.あらゆる詳細化構造の可能性から,整合性に問題の起こる構造を排除し,効果的に複雑さを軽減する構造やよく採用される詳細化戦略に従った構造を発見するための基礎を定義した.さらに,要素の意味や要素・要件間の依存関係を考慮しつつ効果的に詳細化構造の探索を行う手法を構築した.ケーススタディでは,対象システムに関する非形式的な情報を入力とし,提案手法で問題がなく効果的な詳細化構造を計画できた.

 上記の2つの手法の適用結果の考察に加え,詳細化構造の計画に必要な情報の獲得の可能性に関する議論も行った.結果として,本研究の提案手法がEvent-Bとその詳細化機構のより体系的・積極的な利用を促進すると結論付けた.


 
 
 (2017年6月5日受付)
取得年月日:2017年3月
学位種別:博士(情報理工学)
大学:東京大学



推薦文
:(ソフトウェア工学研究会)


抽象から具体へのモデルの多段階構造のリファクタリングなどを支援する,斬新だが応用が広い手法を提案した.証明復元など理論的基盤から,ツール実装と有用性評価までしっかりなされ,形式手法の旗艦会議(FM)など国際的な場で高く評価された.


著者からの一言


振り返ってみると,苦しみも多かったですがそれ以上に実りのある学生生活でした.その間,指導教員の本位田真一先生や共同研究者の石川冬樹先生をはじめとして多くの方に大変お世話になりました.この場をお借りして改めて御礼申し上げます.今後も科学技術に少しでも多くの貢献ができるよう,精進してまいります.