ソフトウェア開発における形式化技術と環境 米崎直樹 東京工業大学情報理工学研究科

リアクティブシステム Request event Environment Service event environment Reactive system Service event

リアクティブシステムの特徴 Safety critical Non-stopping Human interactive Communication oriented 　非常に状態数の多いシステムのあらゆる実行の可能性を確かめる必要がある。

リアクティブシステムの形式的 開発方法 仕様記述言語 仕様の検証 再利用 ソフトウェアプロセスへの組み込み 　これらをサポートする理論とそれに基づくシステムの実現

仕様記述言語 Ｔ 制限された時間論理を使用する。 Nextオペレータを用いない。 （時間の詳細化に対応するため。） 仕様記述言語　Ｔ 制限された時間論理を使用する。 （実現不能な記述を出来る限り許さないため。） Nextオペレータを用いない。 （時間の詳細化に対応するため。） オブジェクト指向モジュール構造を持つ。 抽象化、詳細化オペレーションに対応可能であること。 一階述語化、実時間化に対応可能であること。 形式論理式へのトランスレータを持つ。 差分的検証に対応したモジュール構造を持つ。

□All l in Lifts, Exist f in Floors , loc(l,f); Ｔによる仕様記述例 3階建て、リフトの数が 1個のエレベータシステム system elevator_system(3, 1 ;); class elevator_system(n, m;) {set: Floors = {floor[1..n]}; Lifts = {lift[1..m]}; has: floor[1] : NonTopFloor; floor[2..n_floors-1] : MiddleFloor; floor[n_floors] : NonBottomFloor; lift[1..n_lifts] : Lift; 全てのオブジェクトに対する式を 記述できるように有限領域を定義 □All l in Lifts, Exist f in Floors , loc(l,f); エレベータシステムの 部品を定義

状態の詳細化 　　　開始点・終了点を表す様相↑,↓

例:エレベータシステム stop:エレベータは停止している open:ドアが開く、close:ドアが閉じる を加えて詳細化 　を加えて詳細化 新たに追加する仕様 　「ドアが開いていたら、動き出す前に閉じる」

例:エレベータシステム

□(Button . Press→Button . Light Until I); Button (I : prop) { Press, Light：prop; service { □(Button . Press→Button . Light Until I); 　□(I → Button . Light Until Button . Press); }} ボタンが押されたら、Iに対応するイベントが起きるまで 点灯し続ける。　 Iに対応するイベントが起きたら、ボタンが押されるまで 消灯されたままである。

記述実験 エレベータシステム 赤外線通信プロトコルIrLAP オブジェクト数７、約１００行 ２台、４フロアまで仕様検証可能 オブジェクト数約100、約１０００行 プリコンパイラにより１８７ＫＢの時間論理式が得られた。

検証 いずれも全自動で実行可能 仕様の検証 仕様のより抽象的な仕様に対する検証 実現の仕様に対する検証 無矛盾性、強充足可能性、段階的充足可能性、段階的強充足可能性、実現可能性 これらの判定方法をその正しさと共に示した。 仕様のより抽象的な仕様に対する検証 演繹的証明　（ＫＷに対する完全な検証体系） 適切さの論理の導入 （ER　十分に強く完全で、決定可能な体系） 実現の仕様に対する検証 モデルチェキング 我々のタブローシステムが汎用的に利用可能 いずれも全自動で実行可能

実現可能でない仕様のクラス 仕様の例

バージョン変化と再利用 仕様記述 変更 （実）時間論理式 再利用 検証 自動合成

差分的検証 仕様 1 仕様 2 仕様 n 仕様 n+1 差分 検証 n + 差分 → 検証 n+1 合成 n + 差分 → 合成 n+1 ループチェックの有限表現を持つタブロー

検証の高速化 大規模な仕様の検証では状態爆発が 起こる ・不要な中間状態の省略 ・仕様をモジュールに分割 モジュール間で共有する命題を少なく

タブローの規模が小さく、展開は高速で行える モジュール分割による検証の高速化 モジュール毎にタブローを構成 タブローの規模が小さく、展開は高速で行える モジュール間で共有する命題の制約だけを 統合し、全体を検証 状態数が減少

仕様と外部イベント制約 仕様： 外部イベント制約（要求制約）: 外部（要求）イベントの生起パターンと応答イベントの生起パターンの関係 ある外部イベント系列に対し、仕様を満たす応答系列が存在しないとき、仕様は外部イベントを制約するという。

制約の抽出 要求制約式： 要求イベント列の制約を表す式 制約を満たす要求イベント列については、式を満たす応答列が 必ず存在するための最弱の制約式 要求イベント列の制約を表す式 制約 リアクティブ システム 要求イベント列 応答イベント列

充足可能性判定手続き サブモジュール サブモジュール サブモジュール 要求制約式 要求制約式 要求制約式 メインモジュール 充足可能性判定

実効結果 Satisfiability Checking Strong Satisfiability Checking 5000 10000 (sec) (sec) 5000 10000 15000 20000 25000 2 3 4 (the number of floors) Satisfiability Checking Strong Satisfiability Checking

仕様検証に適切な論理 ER 明らかなトートロジを証明しない。 因果関係の無い｀ならばの式｀を証明しない。 完全性で、決定可能な体系を構築。 ラベル付き推論システムの良い応用。 適切さの論理体系として見た場合にも意義が大きい。 この論理を基礎にした論理体系の研究が、論理学分野の研究者により始められた。

（現実的な検証のための理論） 差分的検証、On the flyでの検証 検証のスケーラビリティ 抽象検証とその再利用性 ループチェックの有限データ表現 検証のスケーラビリティ これについては、一般的な理論構築には至らなかった。 抽象検証とその再利用性 状態の抽象化、詳細化については検証のcompositionalityが保てる。 検証の失敗からの修正情報の抽出 仕様の満たす性質による分類が有効 仕様獲得履歴の形式的表現方法とその理論 仕様の変更　⇒ 仕様の持つ性質が変化 どのような場合にどのような性質が保存されるかを示した。

(ソフトウェアプロダクト) 仕様記述言語Ｔのプリコンパイラ。 時間論理タブローシステム。 タブロービューワー。 充足可能性、段階的充足可能性、 　　強充足性判定システム。 仕様作成支援ツール。

まとめと展望 時相論理による仕様記述が現実的に使える 可能性を示した。 再利用を含めて評価する必要がある。 　可能性を示した。 再利用を含めて評価する必要がある。 全く形式的な仕様から現実規模の問題が扱える時期が来つつある。ソフトウェアの開発パラダイムを変える可能性がある。 ラダー設計への適用を行う。 理論的にも興味ある様相体系を与えた。

外部への発表 学術論文誌　　　　　　　　　　　　　　１７ 国際会議(フルペーパ査読付き)　　４１ 研究会等　　　　　　　　　　　　　　　　３０ 関係する招待講演　　　　　　　　　　　７