********************************************************************** セッションS4-a テーマ:形式検証(モデル検査) 講師:片平 典幸 氏(財団法人福岡県産業・科学技術振興財団) 日時:2011/9/1 13:00〜14:20 参加人数:25名(終了時) ********************************************************************** 実践的モデル検査を考えよう 概要: 形式検証(モデル検査)の必要性について ・検証の意味 ・モデル検査のうれしさについて ・具体的な検査の仕方 ・自分自身で実際にモデル検査ツールを作っている 目次 形式検証とはなにか? 実践的なモデル検査をしてみる Garakabu2ってなんだ? 時相論理 時間を含めたモデル化、検査を実施できる 形式手法とは ・数学を基盤としたソフトウェア、ハードウェアシステムの仕様記述、開発、検証の技術の総称 ・水準0〜水準2までがある。 ・モデル検査は水準0に含まれる(軽い形式手法) ・プログラム意味論の分類 形式検証とは ・形式的記述(形式手法)にしたがった記述内容に対し、数理的に検査を行う検証技術 ・妥当性確認・・・意図した用途に関する要求仕様を満たしているか ・期待した通りのことが書いてあるか? ・モデル検査・・・チェックしたい条件に対して数理的網羅検査で正しさを確認する。 ソースコードにモデル検査をする意味とは? 現場に適用した言葉に対して言葉を使い分ける必要がある ・実際の開発現場では、意味論をどうのこうのが問題ではなく、正しい設計・実装をするために形式手法を使う ・一般にソフトウェア開発で使われるのは、軽量形式手法 モデル検査と形式手法の関係は? ・形式検証とは、 形式手法で記述されたモデルを数理的に検証する技法のこと。 形式手法=モデル検査ではないという意見もある。 結局、形式検証のうれしさとは? ・形式的に記述されたモノ(モデル、仕様書)は、その段階で正しさの検証ができることである。 要は、設計書段階で検査ができることが、現場での最大のうれしさ。 →記述対象物の信頼性が向上するのは、いうまでもない モデル検査の「モデル」 ・ここでいうモデルは、状態遷移(振る舞い)を記述したものを指す UML 状態遷移表 状態遷移図 などなど・・・ ・形式的に振る舞いが記述されている場合、プログラミング言語も振る舞いモデルと考えられます。 C言語を形式的言語と考え、モデル検査するツールもあります。 モデルとは? 抽象化イメージ?、言語?、未知のモノ? 世間的には MBD, MDD この2つは厳密には異なるが、 開発現場では一致しているものでないと、開発現場ではうれしくない! 形式検証とテストとの違い ・数理的網羅検査なので、すべての組み合わせの検査を行うことができる(設計フェーズで) ・実際のコードを書く以前の段階で検査が行えるのが特に重要 形式検証で検査できること ・こんなとき、いつかこうなるという検査ができる。(時相論理) ・設計レベルでの検査(妥当性確認)ができる。 ・あってはならない挙動を見つけることができる。 ツールによりこの機能があるものとないものがある。 実践的なモデル検査 具体的な例を説明 ・両替器のモデル検査 両替器のモデル 両替をする人のモデル (モデルはハード/ソフトによらない) ・検査したいこと ・ありえない状態遷移をしていかないこと ・コインが足りないときは、両替しない ・コインがなくなるまで、両替できれば両替する。 ・紙幣一枚ずつしか両替できない機能を確認する。 その前に・・・ なんで検査したいか 両替器の制御設計が正しくできているか確認するため。 では、制御を状態遷移で書いてみる (発表者の作成しているモデル検査ツールでの状態遷移モデル化を例として、解説) ・あるイベントの発生などの組込みソフトウェアでよくある設計の記述を行うのに適している。 モデル検査は数理的なものである ・つまり、文章的な表現の検査ができない [時相論理式について] 時相論理(LTL)の記述 [F], [G] オートマトンには時系列な変化の概念がある 時間は0.5次元(未来方向のみ) 現在から将来を含めた検査表現を時相論理といいます。 時相論理式で検査できるもの 単項演算系、二項演算系 上記を組み合わせることで、現在から未来への状態遷移条件に対するいろいろな検査ができる。 時相論理であらわされるモノの例 ・車はいつか止まる [F] (BODY_FORWARD=STOP) ・バッグギアを入れるまで、車は全身している(BACK_GEAR=true) ・モーター用バッテリーが使用可能になるまで、エンジン走行をしている。 (Garakabuzでの実際の形式検証の様子の紹介) ・SPINではPromelaによる専用言語での記述を行い、自然言語的な記述を使用する。また、テキストベースのシステムである。 ・Garakabuzでは、視覚的な表示を行うことで、より検証を行う人の負担を減らすようにしている。 [まとめ] [なぜ検証?] 従来のソフトウェア開発のテストは、要求仕様書から作られたソースコードにおけるロジックの正しさの確認になってしまい、元々の要求仕様の正しさを確かめていたわけではない。したがって、要求仕様そのものの正しさの確認を行うことができる検証が現在注目されている。 [形式検証ツール] SPIN, mnSMV, UPPAAL, Vdim, Garakabu2, CBMCなど [検証とモデル駆動開発との親和性] 形式検証は粒度の高い工程、すなわち仕様決定段階などでの検証手法を提供できる。 上流でのモデル化するため、V字開発の左側の部分に一貫性を保つことが可能となる。 要求仕様段階では、詳細なタイミング処理を書くことができないことが多い。 そのため、早い段階でタイミングを含め形式化ができるモデル検査は非常に重要である。 [フィードバックの容易さ] 検証の敷居は高い。SPINなどでは自然言語な出力結果が得られるが、 図などを用いて見える化されている方が格段にわかりやすい。 [検証の重要さ] 大規模化するソフトウェアに対し、今後上流での検証ができる形式検証の重要性が増してくると考えている。 ふくおかISTの紹介 三次元半導体の研究 HALT試験室 電波暗室 質疑応答: [質問] SPINでもよくある状態爆発は、Garakabu2ではどうしている? [回答] Garakabu2で使用しているロジックはSMTと呼ばれる、一般的な検証ツールで使われるSATよりも状態爆発が起こりにくものを使っている。しかし、現在の実装ではSPINの方が状態爆発を起こしにくい。今後実装の最適化が求められる。また、クラスタによる、並列化プログラミングを用いた方法のサポートを現在考えており、近日公開予定(ET2011?) 以上。