« AADL/SysML/HOOD用アーキテクチャ分析・設計ツール2 | トップページ | モデル検査と動作環境調整 »

2016年7月11日 (月)

SysMLやUMLの状態図では並列・並行動作をするシステムの仕様を適切に表現できない

今日は朝から動的モデルのシミュレーション。
 
LTLなどの時相理論は,時間軸上の振る舞いを論理式で表現することで,並列・並行動作をするシステムの「進行性(Progress)」「応答性(Responsibility)」「安全性(Safety)」「活性(Liveness)」などの重要な性質を記述することが可能なのだが、SysMLやUMLの状態図では無理がある。
 
「進行性(Progress)」「応答性(Responsibility)」「安全性(Safety)」「活性(Liveness)」などの重要な性質を記述がないSysMLやUMLの状態図をいくらレビュー(インスペクション)しても妥当性検証や正当性検証にならないので,最悪不毛なレビュー(インスペクション)活動になる。
 
詳細設計レベルであれば、状態図やシーケンス図を机上でレビューしてもデッドロック、ライブドックのような不具合を見抜くことは困難である。
 
良く見かけるSysMLやUMLの状態図には,並列・並行に動作することを完全に無視しているか、モデルに並行・並列や割り込み動作を適切に表現できていないものが多いので、状態図でシステムやオブジェクトの状態空間を適切にモデル化しているという工学的な趣旨や根拠が意味不明なモデルが多い。

Proc


|

« AADL/SysML/HOOD用アーキテクチャ分析・設計ツール2 | トップページ | モデル検査と動作環境調整 »

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