« 『AssuranceCASE』の資料作成 | トップページ | assuranceCASEのモデリングと『ソフトシステム方法論』 »

2016年10月24日 (月)

SpinでLTLで記述した命題を評価した

Promelaにより抽象したモデルを実装し,Spin上で仕様を満たすかLTLで命題を作成し評価しました。
 
取りあえず:
Verification Result = [Valid]
となりましたが,想定通りの完全な結果ではないため,今一つ納得いかないので,少し並列動作するプロセスの割り付けを変えて処理を行い,再評価したいと思います。

Valid

|

« 『AssuranceCASE』の資料作成 | トップページ | assuranceCASEのモデリングと『ソフトシステム方法論』 »

「パソコン・インターネット」カテゴリの記事