講義名

ソフトウェア開発先端技術演習 I

開講学期

前期・集中講義

単位

2単位

担当教員

田辺良則（国立情報学研究所）,早水公二（株式会社フォーマルテック）

講義の目的

本講義では、産業界において業務としてモデル検査の適用を実施する際に必要となる技術やノウハウ，さらにモデル検査の成果や有効性をアピールするための報告書の作成方法までを，受講者自身が実践と経験を通して自力で会得する． 受講者が，業務においてモデル検査を自ら実践，推進する立場に立っていると仮定し，「実践の場＝現場」そのものを想定したシミュレーション形式で講義を進める．受講者が企業内の他の技術者からモデル検査の適用を依頼されたという状況を想定する．また，受講生が成果を経営層にアピールし，モデル検査を社内で本格導入させるために自身が推進者となることを希望するという状況も含んでいる．また，モデル検査を適用する題材は，適用しやすいようにあらかじめ整理された題材ではなく，実際の製品に関する資料（仕様書，ソースコード等）に基づいた題材とすることで，より実践に近い経験を積むようにする． シミュレーションを実施するために必要なモデル検査に関する知識は，本講義の中で教授する．

キーワード

モデル検査，SMV，ソフトウェア検証，形式手法，時相論理，CTL

履修の条件

• C言語で記述されたプログラムが理解できること．
• 命題論理について学習済であることが望ましい．

教科書

• 資料を配布する．

参考書

• 産業技術総合研究所システム検証研究センター著「モデル検査 初級編―基礎から実践まで4日で学べる」 (ナノオプトメディア), 2009.
• B. Berard et al, “Systems and Software Verification: Model-Checking Techniques and Tools,” Springer, 2001.

講義計画

• 第1-3回：モデル検査とSMV
• 第4-5回：モデル検査の方針立案
• 第6-7回：モデル設計
• 第8-9回：モデル製作
• 第10-11回：CTL
• 第12-13回：モデル検査実施と反例解析
• 第14-15回：成果発表

成績評価

パターン指向ソフトウェア開発に関する理解の状況を，講義時間内の演習回答，最終発表，レポートを総合して評価する．