モデル検査 上級編 の商品レビュー

産業技術総合研究所システム検証研究センター【著】

2012/03/01

SPINを使っていましたが，
産総研のSMVのセミナを受講したら，
SMVがとてもモデル記述が楽だということが分かりました。

最初のうちはCTLがうまく書けませんでした。
本書の例を入れて行くうちに，だんだん馴染んできつつあります。

産総研のセミナはぜひ受講するとよいと思いました。

さつきのWEBで入力するときは
1:
になっている行は
True:
に変更しないとエラーになるかもしれません。

さつきのWEBではLTLは受け付けておらず，
CTLで検証することになっているようです。