« Spinのツールを複数使い分け~xSpinとiSpin | トップページ | AADL/SysML/HOOD用アーキテクチャ分析・設計ツール »

2016年6月29日 (水)

SysML/UMLの状態図の制約や並行性の性質記述

要件仕様の内容,あるいはSysML/UMLの状態図に正確に制約や性質を記載することが大切であるが,SysML/UMLだけでは不可能であるし,また検証もレビューやテストで行うことは極めて非効率なので
Promelaでクラスの状態図の振る舞いを実装し,その後SpinにLTLを指定し,NeverClamを自動生成して用いるのが効率が良い。
 
公平性条件(無・弱・強)や並行性の条件(状態図のアクティビティへの割り込み,並行動作)など大抵のことは指定できる。
 
巷で良く見かけるSysML/UMLの状態図は公平性条件(無・弱・強)や並行性の条件(状態図のアクティビティへの割り込み,並行動作)などは無視あるいは考慮していないので,タスク間通信や排他制御の問題を表現できていないものが多い様だ。
 
今日はサンプル作りのために,良く例にある交差点の信号機の,NeverClamを自動生成し,promelaで書いた振る舞いに追加。その後C言語に変換し動作させる。

Spin

Spin2


|

« Spinのツールを複数使い分け~xSpinとiSpin | トップページ | AADL/SysML/HOOD用アーキテクチャ分析・設計ツール »

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