SPINをインストールするという宿題はできましたでしょうか
では始めます
この授業
前回無線LANがつながらなかったこともありうまくいかなかったけれど
今日から本格始動
この教科書にそってやるけど
随時追加の問題を出したり
もう少し高度な内容をやったりする
モデル検査とSATソルバーの応用についてやる
モデル検査の説明から入りたいと思う
本を読んでいただいた方にはわかると思うけど
設計段階での適用してバグだしをする
実際のシステムを単純化しないといけないから
正当性を保障するものではない
一種のシミュレータ
網羅するシミュレータ
情報システムを
オートマトンで記述
要求する使用を論理式で記述
アサーションを埋め込むこともある
それらを満たすことを検査する
むしろ満たしていない部分、つまりバグを発見するのが目的
この教科書では、SPINを使わない、手計算の範囲で
信号機システムを紹介してある
ちょっと馬鹿っぽい例だけれどわかりやすいので
ここの信号機システムとはなにかというと
歩行者用の信号、車用の信号、押しボタン
これを記述してみよう
まず状態を洗い出す
・車用の信号機の色(赤青)
・歩行者用信号機の色(赤青)
・押しボタン(点いているか)
黄色は省略
モデルを作る場合には基本的に状態遷移図を作る
押しボタン信号の性質を素直に書けばいい
ボタンを押さなければその状態でぐるぐる回る
ボタンが押されると別の状態に移る
云々…いくつか突っ込みどころがあるような気がするけれど
この辺は仕様を書く段階でお客様のお話に応じて決める
この状態遷移系に車の状態を絡ませてシステムを記述する
状態図としては複雑になる
人手でチェックするのはなかなか大変
信号、車それぞれ個別だったら人間でも扱えるけれど
2つが一緒だったら厳しい
モデル検査系ではどういうことを検査するか
・安全性 safety
悪いことが決して起こらない
・活性 liveness
良いことはそのうち起こる
良い、悪いは価値観に依存するのであれなのだけれど
決して起こらないこととそのうち起こることがある
この2つの概念は良く出てくる概念なので覚えておいてください
例えばsafetyであれば
危険状態「歩行者用信号機が青で、車から横断歩道までの距離が0mである」
要求される性質「今も、将来もずっと、危険状態へ遷移することがない」
状態数が有限なので計算可能
liveness
「押しボタンが点灯したらいずれ必ず歩行者用信号は青になる」
性格には「押しボタンが点灯したらいずれ必ず歩行者用信号は青になる」が
未来永劫成り立つ
LTLという時相論理でこれらを記述する
ぜんぜん簡単
いわゆる命題論理と時相
演算子がある
G [] ずっと成り立つ
F <> いずれ成り立つ
モデル検査系
・Spin
フロントエンドとすればPromelaという並列
プログラミング言語
・NuSMV
この授業ではやらない
あとは演習