システム検証基礎演習 10/9

SPINをインストールするという宿題はできましたでしょうか
では始めます
この授業
前回無線LANがつながらなかったこともありうまくいかなかったけれど
今日から本格始動

この教科書にそってやるけど
随時追加の問題を出したり
もう少し高度な内容をやったりする

モデル検査とSATソルバーの応用についてやる

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