並列処理を検証する、CSP関連のまとめ

　並列処理関係の検証をするとき、CSPで記述して、確認するけど、その一連＆関係するもののまとめ

---

■CSPで検証する手順

１．CSPで、関係を記述する
　　→状態遷移図なんかを応用して記述できる

２．記述したCSPをType Checkerで確認する
　　→文法ミスを確認してくれる。FDRに直接かけると、エラーだらけの場合、よくわからない

３．FDR2にかける
　　　３－１．まず、読み込ます
　　　３－２．デッドロックフリーとか、詳細化関係(同じかどうか）のチェック
　　　３－３．もし、問題あれば、デバッガでトレース確認
　　　３－４．ちなみに、計算とかもさせられる（Evaluate機能）

４．状態遷移を詳細に見たいのであれば、状態遷移導出ツールProBEが使える

５．Javaでシミュレーションさせたいとなると、JCSPを使う。

---

■CSPと、そのほかのモノとの関係

CSPで記述してFDRで調べる方法も、モデル検査の１つ。
モデル検査としては、他に、SPIN、SMV、UPPAAL、LTSAなどがある。

まず、このちがいについて。

SPIN、SMVとCSPの大きな違いは、前者が、時相論理を使うこと。
時相論理で表現できないような性格のものは、SPIN,SMVでは扱えない。
一方、CSPは、モデルはCSPで記述する（詳細化関係を調べるが、それもCSP）。
時相論理がかけないヒトも（かけないコトも）チェックできる。

LTSAは、FSPという記述言語で状況を記述する。このFSPは、CSPに似ている。
で、LTSAは、LTSっていう図にしてくれるんだけど、あれは、図を楽しむものなの？？
→よくわかってない・・

UPPAALは、そもそも時間概念が扱えるので、かなり違う。

---

■JCSPとJPFについて

　JCSPは、並行システムのシュミレーションをするけど、同じく並行システムを調べるものとして、
JPF（Java PathFinder）がある。

　この違いについて。

　JCSPは、CSP表現したものをJavaでシミュレートしやすくしたもの。
　なので、楽しむことは出来ても、エラーについては、実機確認の域を出ない。

　一方、JPFは、ある程度のケースについて（深さは自分で設定仕様と思えばできるけど、普通デフォルトで使うよな）自動的に検証してくれる。

　たとえば、哲学者の食事問題の戦略について調べようとする。

　CSPで記述し、FDRにかければ、デッドロックするかどうかはわかる。
　このCSP記述を元に、JCSPを記述した場合、対応関係を持ちながら記述することは出来るが、
　楽しめるだけで、必ずしもデッドロックするかどうかはわからない。

　一方、哲学者の食事問題をJavaで記述し（CSPの記述と離れてしまってもよい）
　JPFで検証した場合、ある程度のケースを(場合わけして）検証して、
　デッドロックをちゃんと検出する。

EventBの書き方について

前に、ツールの話は書いたので、今回は、書き方について。

Event-Bは、Bとちがって、２つの部分に分かれる。
MachineとContext（別々のファイルになる）

Contextは、おもにSet（集合）の内容を記述する。記述項目は、こんなかんじ

CONTEXT
EXTENDS
SETS
CONSTANTS
AXIOMS

一方、MACHINEは、Contextを取り込んで、実際にいろんな記述をしていく。項目内容はこんな感じ
MACHINE
(REFINES)
SEES
VARIABLES
INVARIENTS
THEOREMS
EVENT
(VARIANT)
END

このうち、REFINESとVARIANTはリファインメント（あるEvent-B記述をさらに詳細化したもの）で使用します。
SEESで、参照するCONTEXTを指定する。

ってことで、以下、CONTEXTから。

---

■CONTEXTの内容について

CONTEXTは、以下のことを書く。
CONTEXT
EXTENDS
SETS
CONSTANTS
AXIOMS

　つまり、集合と定数という、型とか、固定的な値（変数のように、インスタンスでないもの。クラス定義するようなもの）を宣言する。
　以下、それぞれについてみていく。

●CONTEXT
　CONTEXT　コンテキスト名
　コンテキストの名前を指定する
　
●SETS
　SETS
　　　集合名１;
　　　　：
　　　集合名N

　集合を宣言していく。

●CONSTANTS
　CONSTANTS
　　　定数名１;
　　　　：
　　　定数名N
　定数を「宣言」していく。

●AXIOMS
AXIOMS
ラベル１: 定数１：型１

　ここで、定数の型を指定する。
　型は、NAT1など、あらかじめあるものか、上記SETSで指定したもの

(例）
CONTEXT SampleContext1
SETS
MYSET
CONSTATNTS
val1
AXIOMS
　　axm1 : val1 : MYSET
END

---

■MACHINEの内容について

　実際の記述は、MACHINEでやる。Bとちがい、リファインメントしたものでもなんでも
MACHINE。MACHINEには、以下の内容を書く。

MACHINE
(REFINES)
SEES
VARIABLES
INVARIENTS
THEOREMS
EVENT
(VARIANT)
END

以下、こんなかんじ。
●MACHINE
　MACHINE マシン名

　マシン名を適当に決めて書く

●SEES
　SEES
　　コンテキスト名

　利用するコンテキストを指定する

●VARIABLES
　VARIABLES
　　変数名

　利用する変数を宣言する

●INVARIANTS
　INVARIANTS
　　ラベル名：変数：不変条件
　変数の不変条件をかく。つまり、変数が満たすべき制約を書く。
　ということは、変数の型とか、範囲とか、変数間の関係とか。
　条件をいくつか書くと、条件間のANDとなる
　（ORは条件内にORと書く）

●EVENTS
　イベントをかく。
　はじめに、INITIALIZATIONがあるので、そこに初期化条件を書く。
　BEGINのあとに、
　　　ラベル名：式
　の形。代入は：＝

　INITIALIZATIONを書いたら、つぎから、書きたいイベント（処理）をかく。
　処理自体は、BEGINの中に、同じように書く。

●VARIANT
　変わっていく変数(負のすうにはならない）で、どんどん減少していくもの
　停止性を証明するためには、必要

---

こんなかんじかな。一部しか書いてないけど・・・
まちがってたら、ごめん。

Event-Bのツールのインストールと使い方

　形式仕様記述には、Bメソッドというのがある。これは、どちらかというと、下流よりだが、もっと、上流工程までもサポートしたものとして、Event-Bがある。今日は、そのEvent-Bのお話。

---

■Event-Bのインストール

今回は、Rodin-Platformというのを使う。

（１）まずは、Event-Bのページにアクセス
　　　　http://www.event-b.org/

（２）左側に、Rodin Platformというのがある。それをクリック

（３）まんなからへん（表のInstallationとかかれた桁のなか）に

　　Download the Core: Rodin Platform file for your

　とかかれている。ここのCore以降をクリックすると、ダウンロードページに飛ぶ

（４）Download　Nowとかかれたところをクリックして、ダウンロード

（５）ダウンロードが終わったら解凍

（６）解凍したものの中を見ると、rodin.exeというのがあるから、それをダブルクリックすると
　　　立ち上がる。
　　　　→Eclipseのプラグインってことです。

つぎに、こいつがAtrlierBを使うみたいなので、それをインストールする
はじめに出てくる画面（きたないピンク色の画面。出てこなかった場合、
Help→Welcomeで表示できる）の下のほう（Important Installation notes）
に書いてあるんだけど、

（７）Help → Install New Software....
　　　で、インストール画面を出して

（８）出てきた画面の一番下、
Contact all update sites during install to find required software
のチェックをはずす

（９）一番上、WorkWithのプルダウンのリストを開いて、

Atlier B Provers　・・・（URLが書いてある）・・・

を選択。

（１０）下のリストに、Atlier　Bが出てくるので、
　　それを、チェックしてNext

（１１）あとは、普通のプラグインインストールと同じ

---

■Event-B、コンポーネントの作成

　インストールが終わり、Welcome画面を修了させると、こんなふうに、プロジェクトの画面になる
　右上をクリックして、わざと、全部のパースペクティブがわかるようにしている。
　　Event-B
　　Prove
　　Resource
　の３つのパースペクティブがある。


　この状態で、まずは、作成してみる。

　メニューバーから
　File→New→Event-B　Projectを選択
　出てきたダイアログで、プロジェクト名を適当に入れる。

　プロジェクトが出来たら、コンポーネントをつくる。
　下のように、プロジェクトを右クリック、

　New→Event-Bコンポーネントを選択する。

　出てきたダイアログで、コンポーネント名を入れる（changeMeのところ）
　なお、Event-Bは、Bと違い、Machineのほかに、Contextというのも使う。
　(使わないときもある）。今回は、Machineにする

---

■コンポーネントの編集

そうすると、以下のような画面になる。

このツールは、あらかじめ、こんなふうに大枠が出来ていて、
記入したいところの左側三角形をクリックし、＋の丸囲みを
クリックして、書き込んでいく
（－をクリックすると、その行削除）

そうすると、こんな感じになる

---

■証明

で、証明するには、「Proving」のパースペクティブにして、
チェックマークをクリックする

うまくいくと、チェックになって、そこをクリックすると、
したに、緑のひげくんがでる

だめだと、？になって、そこをクリックすると、
したに、あかいがっかりくんがでる。

---

ツールの使い方は、ここまで

ソフトシステムズ方法論（SSM)

　ソフト・システムズ方法論やソフト戦略思考に書かれている、ソフトシステムズ方法論について、メモメモ。

ちなみに、ここ
ソフトシステム方法論「SSM」とはなんだ（1）
http://www.atmarkit.co.jp/farc/rensai/ssm01/ssm01.html
にも説明がある。

---

■SSMとは

　認識の違いを理解した上で、考え方を修正していく（そして、アコモデートできる落としどことをみつける）方法論

　認識の違いを理解するために、意図的活動モデルを使う
　認識から変革への学習サイクルを循環させる（そうして考え方を修正していくんだね）

---

■SSMのステージモデル（７ステップ）

　はじめに、こんなふうにかんがえたようだ（リンク先もこれが載ってる）

　　　現実世界　　　　　　　　　　　　　　　　システム思考

１、問題状況がある
　　　↓
２．問題状況を表現する　　　→
　　　　　　　　　　　　　　　　　　３、関連する意図的活動システムの基本定義
　　　　　　　　　　　　　　　　　　　　　↓
　　　　　　　　　　　　　　　　　　４、基本定義に名づけられた概念的活動モデル
　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　
　　　　　　　　　　　　　　←
５、モデルと現実世界の比較
　　　↓
６、変革（システム的に望ましく、文化的に実行可能）
　　　↓
７、行為（問題状況を改善するための）

---

■もっといいアプローチ

　上記の方法より、こっちのほうがいいよと、チェックランドさんがいっている。

○文化的探索　　　　　　　　　　　　　　　　　　　　○論理的探索
                       現実世界の問題状況
　　　　　　　　　　　　↓　　　　　　↓
　　＜文化としての状況理解＞　　　　　課題・論点
　・介入の分析　　　　　　　　　　　　　　　↓
　　　社会システム分析　　　　　⇔　　関連システム→活動モデル→状況☆
　　　政治システム分析　　　　　　　　　　　↓
　　　　　　↓　　　　　　　　　　　　モデルと現実世界の差異★
　　　　　　　　　　　　　　　　　　　　　　　↓
　　　　　　　　変革：システム的に望ましく、文化的に実行可能
　　　　　　　　　　　　　　↓
　　　　　　　　行為（問題状況を改善するための）

以下、こっちの方法論の、論理的探索、文化的探索のやり方を書きます。
（リンク先は、前者の７ステージに基づいたやり方が書いてあります）

---

■論理的探索の方法

　上記の右側の手順。以下の４段階。１～３が☆に該当、４が★に該当

１．関連システムの選択
　　　２つの関連システムがある
　　　　　基本課業型システム：現実社会に対応
　　　　　論点主体型システム：概念化されたもので、実社会に存在しなくてもOK
　　　→メタファーを使うといいらしいよ・・・まじ？？


２．関連システムの名前付け
　　　名前をつける→基本定義をする
　　　　＊基本定義は入力→変換→アウトプットのプロセスとして表現するみたい。

３．関連システムのモデル化
　　　・基本定義を、CATWOE分析、XYZ分析して、さらに詳細化していく。
　　　　その手順は、以下のとおり

　　３－１．CATWOE（「きゃとふー」でいいの？）分析を考慮して基本定義を記述
　　　　CATWOE分析（以下を決める）
　　　　　・顧客（C)
　　　　　・行為者（A)
　　　　　・変換プロセス（T)
　　　　　・世界観（W)→変換プロセスは、なぜ必要か
　　　　　・所有者（O)→やめさせることができる人と考える
　　　　　・環境制約（E)

　　３－２．XYZ分析によって、主活動を定義する
　　　　　Zを達成するために
　　　　　Yによって
　　　　　Xを行う

　　３－３．関連する他の活動を洗い出す

　　３－４．まとめて、サブシステムに（活動群により）

　　３－５．判定基準を定義＆（サブシステムに）追加する
　　　　　３つの基準がある
　　　　　　　・可動性：ほんとにアウトプットを生産できる？
　　　　　　　・効率性
　　　　　　　・有効性：目標にあっている？

　　３－６．モニターして、コントロールを（サブシステムに）追加する
　　　　　　モニター：監視して
　　　　　　コントロール：制御する

４．モデルと現実世界との比較
　　異なった利害間でアコモデートできる落としどことをみつけるために、比較する。
　　比較方法は、以下のようなものがある。
　　　　・インフォーマルな議論
　　　　・公的な質問
　　　　・モデルを動かし、シナリオを記述
　　　　・現実世界のモデル化

---

■文化的探索の方法

　上記の左側の手順。以下の４段階

１．文化としての状況の理解
　　　リッチピクチャーを書く
　　　　　・状況を伝える
　　　　　・関係性は対処療法的なものは挙げない
　　　　　・文章による説明（凝縮した表現）

２．介入の分析
　　役割分析：以下の３つの役割を特定
　　　　　・依頼者（クライアント）
　　　　　・問題解決者
　　　　　・問題所有者

３．社会システムの分析
　　社会システム＝継続的に変化する、以下の３要素の相互作用
　　　　　・役割
　　　　　・規範
　　　　　・価値

４．政治システムの分析
　　異なる意見がアコモデーションにたどり着くまでのプロセス
　　　→最終的には、「権力の配分」

---

ってかんじならしい。聞き間違い、勘違いがあるかも。あったらごめん。

アスペクトの書き方

昨日、アスペクト指向のAspectJの話を書いた。
そこで、元のソースはいいとして、横断的関心事として記述する、アスペクトの内容について。

---

■手順

　手順は、以下の３ステップで考えるといいかも

（１）今回、どの箇所に割り込ませるかを、ジョインポイント（割り込み可能箇所）から選ぶ

　　　ジョインポイントは、こんなかんじ。

　　　　　・クラスの
　　　　　　　　→staticの初期化：staticinitialization
　　　　　　　↓
　　　　　・コンストラクタの
　　　　　　　　→呼び出し:call
　　　　　　　　→実行：execution
　　　　　　　↓
　　　　　・インスタンスの
　　　　　　　　→事前初期化？：preinitialization
　　　　　　　　→初期化：initialization
　　　　　　　↓
　　　　　・メソッドの
　　　　　　　　→呼び出し：call
　　　　　　　　→実行：execution
　　　　　　　↓
　　　　　・フィールドの
　　　　　　　　→参照：get
　　　　　　　　→代入：set
　　　　　・例外
　　　　　　　　→実行：handler
　　　　　・アドバイス
　　　　　　　　→実行：adviceexecution

　　各クラスやメソッド等の上記位置の割り込ませたいところを選ぶ　　　　　
　　　　　　　　

（２）上記（１）の箇所を、条件などをつけて、記述する（＝ポイントカット記述）
　　　昨日の例、execution(public String Sample.hello(..));
　　　のように、選んだジョインポイントのあとに（）で条件をつける。
　　　条件には、* .. + ! && || などが使える。
　　　また、アドバイスで変数を使えるように、ポイントカット変数を置くこともある。


（３）上記（２）の箇所で行う処理（＝アドバイス）を記述する。
　　　ポイントカットの前に入れるか、後に入れるかの指定
　　　　　（before,after,例外を投げたときafter throwing、
　　　　　　スタブとして実行する＝ジョインポイントの処理をしないaround）
　　　をしたあと、ポイントカットをかいて、そのあと、処理内容を書く。

　　　アドバイスの外部の変数を利用するには、上記ポイントカット変数を使うか、
　　　thisJoinPointという、特殊な変数を使う。

---

■書き方

ポイントカットの書き方に２つあり、１つは昨日例のように、ポイントカットに名前をつけ、

pointcut helloCut():execution(public String Sample.hello(..));

あとで、その名前（ここではhelloCut()）を利用して、ポイントカットを指定する方法、
before() : helloCut()

と、直接ポイントカットを書いてしまう方法

before() : execution(public String Sample.hello(..))

がある。

前者の例でいくと、昨日書いたように、

public aspect アスペクトの名前 {

　pointcut ポイントカット名():ジョインポイント(条件(ポイントカット変数とか）);
　　　　　　：
　　　ポイントカット続く
　　　　　　：


　beforeとかafterとか() : ポイントカット名()
｛

　　　　　アドバイスの処理
　｝
　　　　　　：
　　　　　アドバイスつづく
　　　　　　：
}

となる。

EclipseのAspectJ、AJDTの使い方

アスペクト指向でJavaをやる、AspectJをEclipseでやるプラグイン
AJDTについて、インストールと、使い方

---

■インストール(Eclipseのバージョン3.4の場合）

Eclipseのメニューバーの「ヘルプ｝（help）→
「InstallSoftware」とか、「ソフトウエア更新」を選択すると、

ダイアログが出てくるので、「サイトの追加」、
新しく出てきたダイアログで、

http://archive.eclipse.org/tools/ajdt/34/update

を指定すると、Aspect-Jのやつが、元のダイアログに出てくるので、チェックして、
「インストール」
ライセンスのレビューで、「使用条件の条項に同意します」
で、ひたすらインストールするのを待つ（５５％くらいがとっても長く、そのあと一気にくる）

なお、Eclipseのバージョンが違う場合は、違うのを入れることになる。

---

■Aspect-Jの使い方（プロジェクトを作る）

「ファイル」→「新規」→「プロジェクト」
で出てくるダイアログから、「AspectJ」の（それしかなかったら、＋ボタンをクリックして、広げて）
「AspectJ　Project」をクリック。

次のダイアログでプロジェクト名を入れる。

そんなかんじで、とにかく、最後まで行き、プロジェクトをつくるとき、以下のダイアログがでるかも。

そしたら、「いいえ」をクリックして、とりあえず無視。

---

■Aspect-Jの使い方（元ソースを作る）

ふつうに、そのプロジェクトに、クラスを追加し、以下のようにクラスを作成する

public class Sample {

	public static void main(String[] args)
	{
		Sample s = new Sample();
		System.out.println(s.hello());
	}
	
	public String hello()
	{
		return "HelloAspectJ";
	}
}

これを、ふつーに実行すると、当然、"HelloAspectJ"と表示される。

---

■Aspect-Jの使い方（アスペクト）

そうしたら、パッケージエクスプローラー（左側）で、プロジェクトを選択し、
右クリックで出てくるポップアップダイアログから
「新規」→「その他」を選択、
出てくるダイアログで、「AspectJ」→「Aspect」を選択。
次へをクリックすると、アスペクトのダイアログが出るから、そこに、以下のようにアスペクトを書く

public aspect SampleAspect {
	pointcut helloCut():execution(public String Sample.hello(..));
	
	before() : helloCut()
	{
		System.out.println("Hey!!");
	}
}

---

■Aspect-Jの使い方（実行）

ここで、パッケージエクスプローラー（左側）で、プロジェクトを選択し、
右クリックで出てくるポップアップダイアログから
「実行」→「AspectJ/Java　Application」を選択すると、

アスペクトがウィーブされて、

Hey!!
HelloAspectJ

（Hey!!が前にはいってる）

と表示される。

Uppaalの使い方

Uppaal（http://www.uppaal.com/）の使い方を忘れそうなので、メモメモ

---

■編集

（１）立ち上げる
　　→Templateという名前のテンプレートが開く

（２）左側のナビゲーションツリーのDeclarations（日本語化してある場合「宣言」）をクリック
　　→右側の描画ペインが大域情報編集ペインにかわる

（３）大域情報を大域情報編集ペインに記入する
　　　大域クロック変数
　　　大域変数
　　　大域通信チャネル

（４）左側のナビゲーションペインで、「Template」をクリック
　　→描画ペインが表示される

（５）テンプレートの「名前」を変えて、テンプレート名をいれ、
　　　右にパラメータを設定する

（６）ナビゲーション側にある（５）で書き換えた名前をクリック、
　　　すると、下にDeclarations（日本語化してある場合「宣言」）が
　　　でてくるので、それをクリック
　　　→編集画面になるので、局所変数などを宣言する

（７）ナビゲーション側にある（５）で書き換えた名前をクリック
　　　描画ペインに戻るので、ロケーション（上の○に下に星？のやつ）を
　　　クリックして、ロケーションを置く（描画ペインでクリックすると置ける）

（８）続けて、→をクリック、ロケーションの始点をクリックして、終点をクリック
　　　すると、エッジが引ける

（９）太い→で選択できる。それをクリック後、ロケーション（○）をダブルクリックすると
　　　ロケーション編集というダイアログが出る。
　　　ここで、名前や不変条件、初期、アージェント、コミットの指定ができる

（１０）太い→で選択できる。それをクリック後、エッジ（→）をダブルクリックすると、
　　　エッジの編集というダイアログが出る。
　　　そこで、ガードに繊維可能条件、同期に同期通信イベント、更新に変数の更新（代入）を設定する

（１１）全部のロケーションとエッジを書いたら、ナビゲーションペインから「システム宣言」を
　　　クリック、プロセス割り当て編集を行う

　　　P1＝P(1)　のように、プロセス＝テンプレート（引数）を何個か書き、
　　　最後に
　　　System P1,P2,　　のように、System　プロセス,・・・という具合に書く

---

■シュミレーション

（１２）上記で編集が終わったので、シュミレーションを行う。
　シュミレータータブをクリックする。

（１３）左上が、実行可能なものを表示するので、そこを適当にクリックすると、
　　　　右上のオートマトンの状態や、右下のシーケンス図が動く

---

■検証
（１４）べりファイアタブをクリックする
（１５）検証式を「クエリ」に入れると（２番目のボックス）、「概要」（１番目のボックス）に入ってくる
（１６）追加ボタンをクリックすると、次のの検証式を入れられる。
（１６）検査したい検証式をクリックして、一番上の「検査」ボタンをクリックすると、一番下のボックスに結果がでる
（１７）反例トレースを出す場合は、検証のメニューで
　　　　　オプション→診断トレース→いくらか
　　　　を選択して「検査」、その後、「はい」をクリックして、シミュレーションタブをクリックして
　　　　シュミレーションを表示させると、判例とレースが見れる。

Android端末に、MeGooやUbuntu等を載せて、デュアルブートする話

Japan Linux Conference 2010の「MeeGoのAndroidプラットフォームへの移植」で聞いてきたお話。

---

●Android端末の特徴

メモリフラッシュ部分が

　misc
　recovery
　boot
　system
　cache
　userdata

のように分かれていて、recoveryとbootそれぞれに、カーネルイメージ、カーネルパラメータ、initrdが組み込まれている。このinitrdをルートファイルシステムとして利用し、/proc,/dev/,/systemなどをマウントしていく。

---

●移植方法
　したがって、カーネルをどうロードさせるか？ということと、ルートファイルをどこに置くかという問題がある。

・カーネルのロード方法
（１）Boot領域上書き
（２）PC経由からカーネル転送、ロード：fastbootコマンドで、zImageを転送
（３）recovery領域を上書き、リカバリーモードで起動

・ルートファイルシステムの場所
（１）System領域上書き
（２）userdata領域上書き
（３）SDカード（PC上でルートファイルシステムを作る）

---

●Nexus　OneでMeeGoを動かす

　カーネルのロード方法は（２）、ルートファイルシステムの場所は（３）を選択

手順１：MeeGoルートファイルシステムの作成
　　KickStartファイルの作成
　　mic2実行
　　ddでmicroSDにコピー

手順２：カーネルの作成
　　MSM（Qualcomm’s Mobile Station Modem）向けを入手
　　カーネルコンフィグレーションにmahimahi_defconfigを使用
　　　　initrdを使わない、xorgは使う
　　コンパイル

手順３：fastbootでカーネル転送、ロード

---

●その他

Wiki（http://wiki.meego.com/ARM/MSMQSD）に詳しいやり方あり。

---

ちなみに、表題のデュアルブートは、
カーネルのロード方法は（３）、ルートファイルシステムの場所は（３）を選択
すると、

普通に立ち上げると、Android、リカバリーモードだと、新規に入れたOSになる。
（デュアルブート）。
カーネルをUbuntuにすれば、Ubuntuが立ち上がる・・・はず？？

日にちがたっているし、この分野については、まったくのど素人なので、間違ったことかいてたらごめん。

KAOSによるセキュリティ要求分析

KAOSによるセキュリティ要件の獲得・分析（田原、Axel,Emmanuel）
“特集セキュリティ要求工学の実効性”, 情報処理, Vol.50, No.3, 2009.
などによる、KAOSによるセキュリティ要求分析。

KAOSによる障害分析と同じ。障害→セキュリティ

■手順

1. セキュリティゴールの分析
　保護する資産は何？

2. セキュリティ障害の識別
　セキュリティゴールに対する、悪意のある障害を含む攻撃者のゴールを反ゴールに

3. 反ゴール分析
　反ゴールを成立させる条件を出して行き、末端のゴールを出す
　反ゴールで利益を得られる攻撃エージェントを確認

4. 資産のオブジェクトの反モデルと攻撃者の反モデルを作る
　反モデル：攻撃者、攻撃者のゴールや能力、監視、ソフトの脆弱性
　　　　　　を扱える程度に充実したモデル

5. すべての反要求に対する、攻撃者の潜在能力（盗聴・成りすましなど）である操作の導出

Secure Troposによるセキュリティ要求分析

Haralambos Mouratidis, Paolo Giorgini: Secure Tropos: a Security-Oriented
Extension of the Tropos Methodology. International Journal of Software Engineering
and Knowledge Engineering 17(2): 285-309 (2007)
に記載されている、Secure Troposによるセキュリティ要求分析方法

■特徴
・i*のモデル自体を拡張
　　→セキュリティ制約がある
・ツールあり http://www.securetropos.org/
　（日本語使えない）

■構成要素

i*の構成要素をセキュリティ風にした、基本的なモデル要素
　　・アクター
　　・ハードゴール
　　・ソフトゴール
　　・セキュリティ制約（i*拡張。８角形）


セキュアな実体
　　・セキュアハードゴール
　　・セキュアアクション（対策とか？５角形）

■手順
・セキュリティ分析・設計手順
（１）初期要件整理→ステークホルダー（アクター）分析
　　・セキュリティ制約

（２）後期要件整理→システム分析
　　・アタックシナリオ分析：アタッカーエージェント考慮

（３）アーキテクチャ設計→タスクを割付
　　・（ここでも）アタックシナリオ分析：アタッカーエージェント考慮

（４）詳細設計

・参考：Haralambos,田口,「セキュアトロポス(Secure Tropos)概論」
“特集セキュリティ要求工学の実効性”, 情報処理, Vol.50, No.3, 2009.

i*によるセキュリティ要求分析（Liuの方法）

Liu, et. al, “Security and Privacy Requirements Analysis within a Social Setting”, RE2003
に記載されている、i*によるセキュリティ要求分析方法

１．攻撃者特定→攻撃者モデル
	攻撃者をアクタとして特定
	悪意のあるユーザを“User As Attacker”アクタとして特定
	→赤色で

２．悪意特定→悪意モデル
	攻撃者のゴールとして悪意を特定
	→悪意に関する部分はすべて赤色

３．脆弱性分析→脆弱性モデル
	攻撃の影響を受ける可能性がある要素を特定
	→悪意のゴールやタスクから負の貢献を受ける要素が脆弱
	→濃い灰色で区別

４．攻撃方法特定→攻撃方法モデル
	悪意を達成する手段である、タスクとして特定
	→Liu手法は、具体的な特定方法はない。
	→HazOpの適用
		・攻撃者が持つ、ドメインモデルの要素を分析対象
		・ガイドワードの適用→悪意が達成可能な逸脱状態特定→悪意ゴールのサブゴール
		・逸脱状態の原因として、攻撃方法を特定

５．対策特定→対策モデル
	各攻撃方法に対し、「その攻撃に対抗（回避／検出）したい」というソフトゴールを設定
	そのソフトゴールにに正の貢献関係を持つタスクとして、対策を特定
	対策の優先度付けにFMECAの適用

SQLは、Vistorパターンに書き換えられる その１：概要

　よく、原稿用紙に書いたら、何枚にもわたるであろう、SQLを書く人がいる。
　このようなSQLは、サーバ側の処理を圧迫するし、メモリもいっぱい使う。

＊メモリもいっぱい使う理由：複雑なSQLは、作業用のメモリを消費するほか、
　その後も結果を保持しておくので＝同じSQLが来たとき、早くレスポンスするため）。

　なので、こういうSQLはやめて、

・テーブルのDAOは、
（１）テーブルデータそのもの（例：SELECT * FROM 受注データ;）
（２）ないしは、テーブル間でとても結びつきの強いものだけ（受注と受注明細の連結）
（３）上記（１）、（２）に対し、インデックスを張った項目のWHERE句のみ


・SQLは、SQL１つを１クラスとし、そのクラスが、上記DAOを読み込んで実現する

　とする。とくに、これに、デザインパターンのVisitorパターンを利用する。

---

つまり、

●DAOについて

・各DAOは、INSERT,SELECT,UPDATE,DELETEのメソッドを持っている。
　ただし、SELECTに関しては、WHERE句しか、対応しない
　（あらかじめ関連の強いものは、そのDAOを持っておく。それ以外のJOINは、ここでは許さない。
　　SUMとかも、ここではしない）


・各DAOは、Acceptorのacceptを実装しておく
　　　acceptの書く内容は、「visitor.visit(this);」だけ



●SQLに該当するもの

・抽象クラスとして、Visitorを用意する
　　→じつは、こうすると、SQLごとに用意しないといけなくなるので、めんどっちいい。
　　　本当のVisitorパターンは、こうするのかもしれないけれど、普通のクラスでVisitorを
　　　用意しておき、そのクラスでは、

　　　　public void visit (各DAOクラス acceptor1 )
	{	//	なにもしない
	};

　　　というように、何もしないクラスを、DAO分、用意しておく




・SQL１つに対して、実装したVisitorクラスを１つ用意する。以下のような感じ

public class SQL1 extends Visitor {
	//	DAOその１で取ってきたSELECTデータ
	ResultSet dao1;
	
	//	DAOその２で取ってきたSELECTデータ
	ResultSet dao2;
		：
		：

	public SQL1()
	{
		DAO1 d1 = new DAO1();
		visit(d1);

		DAO2 d2 = new DAO2();
		visit(d2);
		：
		：

	}

        public void visit ( From句で書かれるDAOその１ acceptor1 ) {
　　　　　　　//そのDAOのデータを取ってきて、
		dao1 = acceptor1.select();
        }

        public void visit ( From句で書かれるDAOその２ acceptor2 ) {
　　　　　　　//そのDAOのデータを取ってきて、
		dao2 = acceptor2.select();
        }
		：
		：


        public ResultSet query ( ) {
		//	上記DAOをもとに、SQLで書きたいような内容を処理して、
		//	結果を返す
        }
}

●呼び出すとき

SQL1 sql1= new SQL1();
で、データを読み込むので、あとは、

ResultSet ret=sql1.query();

で結果が返ってくる。

---

こうやるメリット（NoSQLでも対応できる）とか、
細かな話(トランザクションの実現、条件値をどのように渡すか）
などについては、今時間がないので、別の機会にかきます。

尖閣ビデオのどこを見たのかを、田中康夫議員、服部良一議員は明らかにすべき

　もはや、YouTubeやニコニコ動画では

　　　本当の尖閣

　と検索すれば、尖閣ビデオのコピーがさんざん見れる状況に成ってしまいましたね。

　これじゃあ、もう、削除しても意味ないでしょう。

　これらのビデオをみると、中国は、故意に衝突させたように見えると思う。
　あきらかに、「ぶつかりに行っている」。

---

　ところで、以下の記事

「尖閣ビデオ」見た議員から異論　「これが衝突？」の感想も
http://www.j-cast.com/2010/11/02079854.html

によると(以下斜体は上記サイトより引用）


ビデオをみた印象を「期待はずれだった」「これが『衝突』なのか」と明かしたのは、田中康夫・新党日本代表だ。ブログ「にっぽん改国」（11月1日夕）で、「豈（あに）図らんや、『う～む、この程度だったのか』が偽らざる印象」「『衝突』『追突』『接触』の何れと捉えるか、批判を恐れず申し上げれば主観の問題ではないか、と思われる程度の『衝撃』」などと指摘した。ほかの複数の出席議員も同様の見解を「僕に呟きました」とも書いている。


さらに


また、朝日新聞によると、視聴議員の社民党、服部良一・衆院議員は、「捕まえたこと自体に疑問を持っている」と、中国漁船の船長逮捕についてコメントしている


　この２人に関しては、自分はどこの部分をみて、このように判断したのかを明言すべきだろう。

　もし、これをみて、まだそのように言うのであれば、日本の国民の感覚と合っているかどうか、次の選挙で問うべきである。たぶん、そのくらい感覚がずれていると思う。
　もし、このビデオをみて、「自分の見たものとは違う」というのであれば、政府は、わざと事実に反するように編集して、議員たちに見せたことになる。その責任を、政府は問われるべきである。

　果たして、どちらなのか？

　もし、ここを明言しないと、場合によっては、この２人に、さらに問題が飛び火するような気がするのだが・・・

---

　それにしても、ここまで、情報が公開された社会っていうのも、すごいね。
　YouTubeの社会現象は、こうやって進んでいくのかもしれない。

　そのうち、戦争場面とかも、リアルタイムでアップされていくんだろうねえ・・・

　YouTube　VIPスレとか出来たりして・・・
　・・・もう、あるのかな？

NoSQLの位置づけを分類してみる

こんな感じなのかしら・・・間違ってたらごめん。

---

■NoSQL概要

（１）NoSQL
　　　（１－１）分散Key-Valueストア
　　　　　　　→Dynamo（Amazon）、BigTable（Google）、HBASE、Apache Cassandra
　　　　　　　　Kumofs,ROMA

　　　（１－２）ドキュメント指向データベース
　　　　　　　→CouchDB、MongoDB

　　　（１－３）その他・・・って、あるかな？


（２）RDB
　　　→Oracle,MySQL,PostgreSQL

※ただし、これらの分類は絶対的ではなく、MongoDBは、なんでもありだそうな。

NoSQLは、構造が決まっていない場合でも（ドキュメントやキーバリューとして）保存できる。
そのため、半構造データの操作に適している。
一方、構造化されたデータであれば、RDBのほうが、扱いやすい。

---

■BigTable,HBASEなどの位置づけ

You Tubeに尖閣ビデオが流出だそうだけど・・（９：３０追記）

本家にも書いたけど、尖閣の、漁船が衝突してきたときのビデオがYouTubeに流出したみたい。

URLは（消されてなければ）こんな感じなんだけど・・・

本当の尖閣　海上保安庁１
http://www.youtube.com/watch?v=JXkawnuyTn8

尖閣の真実　海上保安庁２
http://www.youtube.com/watch?v=bY0tgl6YLGI

尖閣侵略の真実　海上保安庁3
http://www.youtube.com/watch?v=3eJsXP4HLVs

本当の尖閣　海上保安庁４
http://www.youtube.com/watch?v=gOUvdNjs_Cg

日本の尖閣　海上保安庁５
http://www.youtube.com/watch?v=q3JYT0G94-E

どうなる尖閣　海上保安庁６
http://www.youtube.com/watch?v=A7h0S1nk9Hk

これって、わざと？
じゃなかったら、日本のセキュリティって（＾＾；）
（でも、今まで流出しないで、なぜ今・・・）

---

９：３０追記

今見たら、全部消されてました。そりゃーそーだ。
でも、ダウンロードした人も多いだろうから、
また、誰かが公開する可能性はあるよね。

はじめ、釣りか、なんか、意図があって故意に？と思ったけど、
尖閣沖中国漁船衝突映像流出　海上保安庁、幹部が集まり対応を協議
http://headlines.yahoo.co.jp/videonews/fnn?a=20101105-00000373-fnn-soci
ってことは、まじ流出しちゃったの・・・（＠＿＠！）

これ、中国が、いろいろ言ってきそうなのは当然として、
アメリカが、「おまいらの国、軍事機密管理は大丈夫なのか？」と
クレーム入れられても仕方ないレベルだよね！