SPINについて（概要）

■SPINについて
・SPINは、モデル検査ツールの１つ
・プロセス単位で手続き的にモデルを記述

＜＜モデル検査ツール＞＞
　　有限状態モデル＋対象システムが満たすべき性質
　　　　　　↓
　　　モデル検査ツール
　　　　　　↓
　　　成り立つ？成り立たないとき反例
　　　シュミレーション

モデル検査の例：SPIN,SMV,LTSA,UPPAAL、Java Path Finder
SPINは、
・デッドロック検証
・PLTL式検証のほか、
・表明（アサーション）や、ループ進行性のパラメタをいれて、検証できる
　　　・progress
　　　・never
　　　・assert（ブール式）

---

■モデル検査で扱う「システムの性質」とは？

・到達可能性
　　　→ある状態に到達する
・安全性
　　　→デッドロックにならないなど
　　　　望ましくない状態に陥らない
・活性
　　　→望ましい状態にかならず到達する
・公平性
　　　→ある状態が無限回起こる

ただし、モデル検査ツールすべてが、上記の性質を扱うわけではない。

---

■性質を表現するには？

SPINの場合

・PLTL（線形時相論理）を使う

　[] p （つねにPが成り立つ）
　＜＞ｐいつかPが成り立つ
　ｐUｑ　ｑがいつか成立し、それまでPがなりたつ

　　　＋

　否定、and、or

・安全性
　　→同時にクリティカルセクションに入らない

・活性
　　→飢餓状態（スタベーション）は発生しない
　　　ずっと待たされることはない
　　　いつかは、クリティカルセクションに入れる

---

■性質の記述パターン
・なかなか、表現がわからないので、

・表現のパターンがある（CTLもある）
　　　http://patterns.projects.cis.ksu.edu/
　　→スコープ（対象とする範囲を定めたもの）が大事

・パターン（大きく２種類）
　Occurenceパターン（おきる・おきない：発生を記述）
　Orderパターン（順序を表現）

---

■SPINに話を戻し、しくみは？

Promelaで記述したシステムモデル
　　　　↓
　　　Xspin
　　　　↓
　　　spinが検証用プログラム生成
　　　　↓
　　　コンパイル、実行

---

■SPINのモデル構成要素
おおきく、４つ
（１）記号定数定義
　　　　mtype={変数１,変数２};

（２）大域変数定義
　　　chan toS
(chan　＝＞　チャネルを示す）

（３）プロセス定義
　　　　proctype →本文

（４）init文
　　　init{
　　　　　プロセス生成

---

■文の中身

・データ型
・代入文
　　変数＝値
・制御構造（ガード文）
　　goto
　　if
　　do
・メッセージの送受信
　　出力チャンネル名！値１
　　入力チャンネル名？値１
　　chan チャンネル名＝[バッファサイズ] of ｛型の並び｝

バッファサイズ０だと同期、１以上の数を指定し、非同期にできる

マニュアル
・日本語
http://www.asahi-net.or.jp/~hs7m-kwgc/spin/Man/Manual_japanese.html

・Reference manual
http://spinroot.com/spin/Man/promela.html

---

■Xspinのちょーかんたんな使い方

・File→Openで読み込むか、ファイルをエディットする
・Run→SetSimulationParametersをチェック

・でてきたパネルで、Start

・以下のようにウィンドウが３つでてきて、実行

---

■デッドロックの確認

・Run→Set　Verification　Option

・そうすると、ダイアログが出てくるので、Run

・デッドロックがあると、errorsというのがでてきて、Suggested Actionダイアログが出る

・Run　Guided　Sumilationをクリック

・出てきた画面（３つ）のうち、左上のダイアログ「Run」をクリック
　　→右側にシーケンスがでる

---

■PLTLを使う

・Run→LTL　Property　Managerを選択
・Formulaに、式を書く
[] a && b && c

・aの条件式を、Symbol Definitionに書く
#define a x <5 ・generateをクリック

・Run Varificationをクリック

・新しく出てきたダイアログで、Runをクリック


※参考「いつかは、～にもどる」
[]（！（a && b && c） →　 []（＜＞ a && b && c））

クラウドより、ISPのほうが、安全ってことっすかね？

Wikileaksって、Amazonから、追い出されたじゃないですか・・・

Wikileaks、Amazonのサーバから追い出される
http://www.itmedia.co.jp/news/articles/1012/02/news034.html

ってことは、アメリカの意向に逆らった場合、
アメリカのクラウドにおいておくと、業務停止になる可能性がある
ってことですよね・・・
これって、ものすごいカントリーリスクですよねえ・・・

でも、実際にWikileaksって、サーバーうごいてるじゃないですか・・
それは、

内部告発サイト『Wikileaks』の内部は恐ろしいくらいカッコいい　完全に悪の秘密基地だこれ
http://2r.ldblog.jp/archives/3815031.html

ってことで、ISPが保護していてくれるから・・・

ってことは、やっぱり、クラウドにおくより、信頼できるISPにおいておいたほうが、
リスクは少ないってこと？

astah*を使って、ICONIX風一気通貫システム開発 その８：フレームワーク決定

「astah*を使って、開発の要求仕様から、プログラム作成までを、トレーサビリティを保って、どのように開発するかを書いてみる」という、このシリーズ、以下の手順で説明する予定ですが、

（１）作るべきもののユースケースを書く
（２）ユースケースシナリオを書く
（３）ロバストネス分析
（４）バウンダリ（画面）、エンティティ（テーブル等）の属性を埋めていく
（５）バウンダリの項目を元に、画面構成を考える。
（６）(必要があれば）エンティティを正規化して、ER図にする
（７）フレームワークを決定する
（８）画面クラスをソースコードに書き直す
（９）エンティティをDBのテーブルと、DAOに書き直す
（１０）コントローラーを書き直す

前回、（５）をやったので、今回は、「（７）フレームワークを決定する」について。

---

■概要と位置づけ

　（５）によって、画面項目と画面遷移、（６）によって、データベース側の項目は決まりました。
　つまり、論理的には、もう決まったので、ここからは、どのように、実装をしていくかを考えます。

　最近の開発の場合、フレームワークを使って開発するのが主流です。
　フレームワークが決まってしまうと、なにを開発すればよいかの大枠がきまります。
　なので、実装の最初は、まず、フレームワークに何を選ぶかを決めます。

　フレームワークが決定してしまうと、コンポーネント構成なども大体きまってしまいます。
　そして、システムの画面と、DBまでのつながりが大まかにきまるので、外部設計的にはひと段落と成ります。
　つまり、フレームワークが決定したら、外部設計をまとめて、お客さんに確認をとることで、外部設計的にはひと段落します（フレームワークが決まらないと、外部レイアウトが正しく決まりません。なので、この前で同意を取るのは、危険だったりします）。

---

■決め方の観点

　まず、何を決めるかですが、最近は、MVCで考えることが多いと思います。

　V＝ビュー：画面、ユーザーインターフェース

　C＝コントロール：画面とモデルのつなぎ

　M=モデル：処理部分。
　　　　モデルのロジック部分と、データベースアクセス部分がある。

　ってことで、

　・ビュー→コントロール
　　　ビュー自体は、HTMLファイルとか、JSPファイルとかになり、
　　　コントロール部分は、Javaのソースコードになる。
　　　これをつなぐところにフレームワークが「入ることが多い」
　　　（自動生成してしまうフレームワークとかもあるし、
　　　　画面をフレームワーク化とかも、ないわけじゃない）

　・モデル部分の管理
　　　各ビジネスモデルは、それぞれ作るにしても、それを管理する部分に
　　　フレームワークを使う。DIなんか・・

　・データベースアクセス
　　　データベースアクセス部分にフレームワークを使う。
　　　DAOを使ってアクセスする。
　　　O/Rマッピングなどを行うもの
　　　
　という部分に、どんなフレームワークを当てるか？ということを考えます。

　なお、この全部を、１つのフレームワークで行う場合、
　「フルスタックフレームワーク」といいます。

---

■たとえば・・・

　ビュー　→　コントロール：Struts
　モデル部分の管理　　　　：Spring
　データベースアクセス　　：Hibernate

など。この場合、Strutsを使うと、JSPなので、Web用のブラウザで見る場合はつなぎやすいけど、
AJAXをやる場合、つなぎにくい（出来ないわけではない。十分出来るんだけど、もっとふさわしい方法がある）そこで

　ビュー　→　コントロール：T2フレームワーク
　モデル部分の管理　　　　：Spring
　データベースアクセス　　：Hibernate

とかも、ありえるかもしれない。

このように、GUIとかによって、フレームワークが変わってきたりする。
もちろん、フレームワークを作るとか、使わないという選択肢もあるが、自作する、使わないということを、この場で、「決める」ことになる。