概要
本研究では船舶用システムに用いられている組み込みシステムを対象としたモデ
ル化および検証について述べる．組み込みシステムは，幅広い分野で利用されて
おり基盤技術の 1 つとなっている．そのため，こられが誤りなく動作するとい
うような高い信頼性に対する要求は非常に大きい．

本研究では，数理的技法の 1 つであるモデル検査を用い，組み込みシステムを
検証できる枠組をモデルチェッカ SPIN 上に構築し，実際に使用されている船舶
用システムの 2 つのモジュールを実装し検証を行った．その結果，一方のモジュー
ルに関しては検証をしたい論理式に対して反例が出力され，他方のモジュールで
は特定の形のデッドロックが生じないことを証明することができた．また，時間
概念のモデル化に関しては問題が残ったもののモデルチェッカ SPIN を用いて実
際の組み込みシステムを検証することができた．

発表論文
"モデル検査器を使った船舶用システムの検証について," 
第4回システム検証の科学技術シンポジウム，pp.109--115, November, 2007.

"Modeling and Verification of Marine Equipment Systems Using a Model Cheker," 
IAENG International Conference on Software Engineering (ICSE'08), to appear.