まとまりのない話だけど・・・
■UMLに時間
UMLの中でも、ステートチャート図、さらに、UML Profile for SPTを使って考える
UML Profile : UMLにつけるこめんとみtainamonn
UML Profile for SPT:時間に関してのコメント。今回は3つのステレオタイプを使う
RTtimeout RTstart
その時間とどまってから実行
SAaction SAworstcase,SAdelay:doアクティビティの最大、最小時間
これがなければ、瞬時に実行
CRsynch なし:完全同期(相手が準備完了になるまでブロック)
つけないとき、キューの長さ1
こいつをつかって、Uppaalに落とす。
ステートチャートのアクティビティ1個が、Uppaalの1ロケーション
■開発プロセスとUML
開発プロセス
要求分析 :ユースケース図、システム構成図、シナリオ記述、非機能要件
システム分析 :アクティビティ図、シーケンス図(分析モデル)
ドメイン定義 :クラス図/パッケージ図
エンティティ分析 :クラス図(分析モデル)
ドメイン内部の分析 :クラス図、コラボレーション図、ステートチャート図
アーキテクチャ設計 :非機能要件→各図へのコメント追加
詳細設計 :クラス図、シーケンス図、ステートチャート図
ドメイン内部の設計=基本設計
そのあと、実装→テストとなっていく。
■検証モデルをつくるために、設計モデルに必要な要件
・個々の処理フローがわかる(ないしは、未定のところがわかる)
・入出力と処理の関係がわかる
・(Uppaalで行う場合)時間情報がわかる
■適用する際に考えること
・検証モデル:なにを検証したいか(対象)
・検証したい性質:何について検証するか