Uppaalにおける検証モデルのつくりかた

■全体像

（１）もとのステートチャート図

（２）時間情報を加えたステートチャート図

（３）検証
　（３）－１　検証モデル
　（３）－２　ツールでの検証
　（３）－３　反例の分析

---

■（３）－１　検証モデルの手順
・環境コンポーネントのモデル化
・時間制約の詳細化
・検証したい性質の定義
　　オブザーバー
　　検証式

---

■（３）－１－１　環境コンポーネントのモデル化
・検証対象コンポーネントとの相互作用があるところを定義
　　→相互作用にかかわる、必要最低限の制御ロジックでいい


■（３）－１－２　時間制約の詳細化

詳細化する前に＝既存データに対するモデル化
・ステートチャートの状態＝ロケーション
・状態遷移＝遷移
・時間制約をモデルで表現するが・・・
　　　デッドロックになる場合がある

詳細化－１：実装に必要になる時間制約の抜けを補充
詳細化－２：検証のための時間制約を追加

●（３）－１－２：補足　時間制約になる、時間要素
・実装段階までには明確化、プログラムに直接反映される時間
　　適切なタイミングでアクションを起こすための時間
　　アルゴリズムの判定要素として使う時間
　　例外判定のための時間

・設計段階では想定するが、プログラムに直接反映しない
　→環境をシミュレーションするもの

・設計段階で想定するが、プログラムにはなく、検証には必要
　→計算時間

・要求側から、こうなっているべきという時間
　→要求仕様に書かれている

●　（３）－１－２：補足　留意点
・時間要素が漏れなく反映されているか
・意に反した非決定的な挙動はないか
・初期値／参照関係は実態とあっているか
・検証対象との相互作用
・実測地なのか、想定値なのか？
・調整可能な時間かどうか？
・インタラクションに直接対応する想定値のみを設定すると、漏れが発生することも
・誤差
　　→センシングする時間がαのとき、５０で分岐→５０ぴったりでなくαの誤差を考慮

---

■（３）－２　ツールでの検証

マニュアル見てやってください

---

■（３）－３　反例の分析

・symblic trace
・concreat trace
・クロック変数の値の変化を確認
・影響を与える範囲を抽出

ハイプサイクルと製品ライフサイクルの関係って、どう思います？

ハイプサイクルは、

「黎明期」「流行期」「反動期」「回復期」「安定期」

ないしは、

黎明期→ピーク期→幻滅期→啓蒙活動期→生産の安定期

のように進みますよね・・・

---

一方製品ライフサイクルは、

導入期、成長期、成熟（市場飽和）期、衰退期

のように進みますよね。

で、この関連

ハイプサイクルの「黎明期」＝製品ライフサイクルの「導入期」

これはいい。また、

ハイプサイクルの「安定期」＝製品ライフサイクルの「成熟期」・「衰退期」

っていうのも、たぶんいいと思う。

のこりの、

ピーク期→幻滅期→啓蒙活動期

が、

製品ライフサイクルの

導入期、成長期、成熟（市場飽和）期

のどこに、位置づくかということ。

---

■ハイプサイクルは、成長急落成熟パターン？
Wikipediaの「製品ライフサイクル」の説明には、

「成長急落成熟パターン」っていうのがある。

これにハイプサイクルを当てはめると、

成長　＝　ピーク期
急落　＝　幻滅期
成熟　＝　啓蒙活動期（・安定期）

っていうことになりそうだ。まとめると、

---

ハイプサイクルは、製品ライフサイクルの代表的パターン、成長急落成熟パターンであり、

製品ライフサイクル　　ハイプサイクル

　導入期　　　　　　　黎明期

　成長期
　　　成長　　　　　　ピーク期
　　　急落　　　　　　幻滅期
　成熟期　　　　　　　啓蒙活動期
　　　　　　　　　　　生産の安定期
　衰退期

といえそうだ。

---

　製品ライフサイクルの成長前期に、参入を始めるのが良いとされるけど、

　ハイプサイクルの場合、
　　　株の買い方（普通、落ちきった後の上がり調子のところで買い）
　と同じと考えると、
　
　つまり、啓蒙活動期に参入を考えるほうがよさそう。

QMLを、はじめたい！ その１ とりあえず、Qtをダウンロード

突然だけど、Qtをはじめてみる。っていうか、QMLをはじめたい。
理由は、かんたんそうで、たのしそうだから
（「簡単そう」の理由については、別のときに書くかも・・・）

まずは、インストールだよね。
Qtをはじめるには、

Qt をはじめよう！ 第1回: Qt をはじめよう！
http://qt-labs.jp/2010/03/15/qt-getting-started.html
からはじめるのが、「ビンボー人には」よさそうだ。
（金持ちの人は、たぶん、「入門 Qt 4プログラミング」から読むんでしょう・・・きっと）

たぶん、第二回　Windows編から、よめってことね！

ここへ、いけと・・・
http://qt.nokia.com/downloads-jp
ご、ごめん。。。よくわかんない（＾＾；）なにを（左と右どっちを）ダウンロードするの？
第二回の説明だと、

　　Qt SDK for Windows のダウンロード* (322 MB)

ってことなので、左をダウンロードした。
（ちなみに、クリックすると、画面が変わり、ブロックした云々でるので、そのブロックを解除して、ダウンロードした。変わった画面で、E-mailとか入力するところは、とりあえず何もしなかった）

時間かかる・・・

ダウンロードが終わったら、そのExeファイルをダブルクリックして実行した。

次からの画面は、ここに書いてあるとおりなんだけど、「コンポーネントの選択」のところ、「Qt Creator」は、文中では「選択した状態にして」とかいてあるけど、そこの図のように、選択するも何も、選択されている状態になっていた。
　Pythonなんたらかんちゃらも、そうなっていた。Symbianはもともとない。Postなんちゃらかんちゃらは、図でも文章でもチェックしてないので、そのまま（チェックしない）にしておいた。

　あとは、同じ。

　おお、Qt　Creatorが動くところまで来た！

　で、次は・・・？


P.S　そうそう、「入門 Qt 4プログラミング」の訳者の杵渕さんは、今、何してるんだろう・・・

12月12日(日)のつぶやき

11:53 from web
中小企業が（コンピューターの）システム化できないのは、会社が（業務的、非コンピューターの）システム（＝手順）を持ってないからだよね!
うん、違うか？システム化できていないから中小企業なのか・・・
by xmldtp on Twitter