ディペンダブル・システムのための形式手法の実践ポータル

Selex Communications - 船舶通信システム

ドメイン	船舶
開発対象	船舶通信システム IECS
国	イタリア
開発組織	Selex Communications
形式手法（言語、ツール）	SPIN (ステート図や、PSC: Property Sequence Chartsに基づく検証プロパティをCHARMYで記述し、SPIN用に変換。)
適用範囲・規模（形式手法）
適用対象のソフト種別	制御
適用目的・工程	仕様記述、設計
実装言語
実装規模
効果	各プロパティの検証および、デッドロックや到達不能パスや正しくない最終状態が存在しないことを検証できた。

（出典: Daniela Colangelo, Daniele Compare, Paola Inverardi, and Patrizio Pelliccione, Reducing Software Architecture Models Complexity: a Slicing and Abstraction Approach, Formal Techniques for Networked and Distributed Systems-FORTE 2006）

詳細情報

検証内容

• デッドロックが無いこと、正しくない最終状態が存在しないこと、到達不能なパスが存在しないこと。その他、Activate Service (ユーザがサービスを非活性化させていないとき、ActivateServiceリクエストの送信後、サービスがアクティベートされる)、Deactivate Service、Reconfiguration Service、Modify Equipment、Modify Equipment by Serviceの各プロパティ。

検証規模

SPINでのデッドロックフリー等の検証時のモデルのサイズは以下のとおりであった。
• 状態数: 1.3e+08
• 遷移数: 6.2e+08
• メモリ使用量: 2.0Gb

各プロパティの検証については、状態爆発を起こしてしまったため、スライシング技術を利用してモデルサイズを削減し、検証を実施した。

期間

判断

形式手法を利用した動機

手法・ツール選択理由

障害と工夫

モデルのサイズを小さくするため、CARMYで記述されたソフトウェアアーキテクチャモデルから、TESTORを拡張して構築したDEPCOLアルゴリズムやスライシング技術によって検証すべき部分を抽出した。

組織

体制

教育

その他

情報源

Daniela Colangelo, Daniele Compare, Paola Inverardi, and Patrizio Pelliccione, Reducing Software Architecture Models Complexity: a Slicing and Abstraction Approach, Formal Techniques for Networked and Distributed Systems-FORTE 2006

このページの先頭へ戻る