diff --git a/courseA/Alloy.html b/courseA/Alloy.html index dc49db3..b886006 100644 --- a/courseA/Alloy.html +++ b/courseA/Alloy.html @@ -1,5 +1,5 @@ - + + 【DTRAMの説明】 + + +

【DTRAM の概要説明】

+ 次に本実験で用いる DTRAM の概要について説明します．
+ 現時点では本ページの内容を完全に理解する必要はありません．課題に取り組む際に必要に応じて本ページを参照しながら進めるようにください．
+

アーキテクチャ記述言語とは？

+ DTRAM は仕様とアーキテクチャの両方を同時に記述することが可能な言語で，形式的仕様記述言語であると同時に形式的アーキテクチャ記述言語でもあります．
+ 形式的アーキテクチャ記述言語とは，システム全体の構造を箱や線などの図ではなく，厳密に意味が定義された言語の形式で記述する方法です．形式的アーキテクチャ記述言語では一般に，
+

システムの構成要素であるコンポーネント，
コンポーネント間の結びつき，
コンポーネント間のデータや制御の流れ

+ などが記述されます．
+ アーキテクチャ記述言語で記述されたアーキテクチャモデルは，システム全体のパフォーマンス，リアルタイム性能，リソース消費量や信頼性などの非機能的要件の予測や解析に用いられます．
+ また開発チーム内で，システムの全体構造についての理解を共有するためのドキュメントとしても利用されます． +

DTRAM とは？

+ DTRAM は仕様とアーキテクチャの両方を形式的に記述することが可能な言語です．形式的仕様記述言語として見ると表現能力が高いため，網羅的な解析はできません．
+ DTRAM では仕様そのものの解析より， +

仕様の仮想実行によるテスト，
記述したアーキテクチャで，記述した仕様が実現できるか否かのチェック，
通常のプログラミング言語で実装された実行可能なプロトタイプの自動生成

+ などを行うことを重視しています．
+ また，形式的アーキテクチャ記述言語としては記述の抽象度が高いため，同一のアーキテクチャ記述からさまざまな設計を持った実装を導出することができます． + 本実験では，DTRAM による仕様記述と仕様の仮想実行に着目していきます．そのため，DTRAM によるアーキテクチャのチェックやプロトタイプの自動生成は行いません．また，DTRAM のツールをPCにダウンロードして操作していただく必要もありません．
+

DTRAM による仕様記述:

+ DTRAM では，リソースとチャンネルを使って仕様とアーキテクチャを記述していきます．
+ DTRAM におけるリソースとは，システム外部から見えるデータのことです．Web サービスにおいて URL でアクセスされるリソースとほぼ同じものと考えて差し支えありません．DTRAM においてもリソースは階層構造を持つことができます．
+ チャンネルはリソースとリソースの間の通信路です．システム外部からの入力はイベントチャンネルと呼ばれる特殊なチャンネルによって受け付けられます．
+ リソースはチャンネルからメッセージを受け取ると状態遷移を行います．そのため，リソースは状態を持ちます．宣言型言語とは違って，状態が変わるたびに別のリソースが生成されることもありません．すなわち DTRAM では，時間経過を扱うことができます．
+ それでは，具体的に DTRAM の記述を見ていきましょう． +

DTRAM による仕様記述の例

例題仕様:

+ Alloy のときに記述したアドレス帳と同じ仕様を，今度は DTRAM を用いて記述することを考えます． + アドレス帳の仕様を再掲します． +

システムはアドレス帳を1つ持つ．
アドレス帳には所有者の名前が記載されている．
アドレス帳には連絡先の名前とアドレスの対応を任意個登録することができる．
アドレス帳において連絡先の名前が重複してはならない．
アドレス帳は連絡先の名前とアドレスの対応が1つも登録されていない状態を初期状態とする．
add 操作によって，指定した名前と指定したアドレスの対応をアドレス帳に登録することができる．
del 操作によって，指定した名前と対応するアドレスをアドレス帳から削除することができる．

DTRAM による記述例:

+ DTRAM では，チャンネル単位で仕様を記述していきます．たとえばリソースに対する操作毎に，イベントチャンネルを定義していきます．ここでは，初期化操作用のイベントチャンネルを Init，add 操作用のイベントチャンネルを Add，del 操作用のイベントチャンネルを Del とします．
+ channel でこれらのチャンネルを宣言します．チャンネルの宣言の中の out は，チャンネルを流れるメッセージを受け取るリソースを示しています．チャンネルにメッセージを送信するリソースも記述することができますが，本実験では使用しません．リソースについては次に説明します． +

+ DTRAM では，Web サービスと同様に階層化されたリソースを扱うことができます．リソースは状態を持ち，その状態を変更することができます．アドレス帳の仕様は次のような階層化されたリソースで表すこととします． +

book: アドレス帳全体
book.owner: アドレス帳の所有者
book.addr: アドレス帳に記載された連絡先の名前と住所の対応表
book.addr.{name}: 連絡先の名前 name に対応した住所

+ 下の仕様記述を見るとわかると思いますが，チャンネル Init を流れるメッセージを受け取るリソースは book.owner です．同様に，チャンネル Add 内のメッセージを受け取るリソースは book.addr，チャンネル Del 内のメッセージを受け取るリソースも book.addr になります．
+

+ メッセージを受け取ったリソースは状態遷移を行います．各リソースの状態遷移は状態遷移関数によって定義されます． + たとえば，Add チャンネルでメッセージを受け取った book.addr リソースの状態遷移は，状態遷移関数 book.addr(pre_addr: Map, add(name: Str, addr: Str)) = insert(pre_addr, name, addr) によって定義されています．
+ 状態遷移関数の関数名にはリソース名をそのまま用います．状態遷移関数の第1引数は遷移前の状態，第2引数は受け取るメッセージ，式の右辺は遷移後の状態を表しています．
+ この例では，メッセージ add(name, addr) を受け取った book.addr リソースが，状態を pre_addr から insert(pre_addr, name, addr) に変化させることが示されています．
+ この insert() 関数は，第1引数に渡された写像(対応表)に対し，第2引数と第3引数の対応を追加した結果得られる写像を返す関数です． + したがって，上の式の右辺は，遷移前の状態 prev_addr に，メッセージ add() の引数で渡された name と addr の対応を追加したものが遷移後の状態になることを示しています．
+ なお，変数名の右側の : の直後に変数の型を記述することができます．型推論によって型がわかる場合には，型を省略することもできます．状態の型が，List，Map，Json であるリソースは子リソースを持つことができます． +

+ Alloy と異なり，DTRAM では仮想実行に関する情報を仕様記述には記載しません． +

+channel Init {
+	out book.owner(pre_name: Str, init(name: Str)) = name
+}
+
+channel Add {
+	out book.addr(pre_addr: Map, add(name: Str, addr: Str)) = insert(pre_addr, name, addr)
+}
+
+channel Del {
+	out book.addr(pre_addr, del(name: Str)) = delete(pre_addr, name)
+}
+

実行の可視化:

+ DTRAM でも実行を可視化することができます．Alloy とは異なり，DTRAM では仮想実行をインタラクティブに進めていきます．まず，システムの初期状態を可視化したものが以下の図です， +

+ 可視化では1つのリソースが，1つの楕円で表されます．子リソースは親リソースの内側の領域に表示されます．リソースの上部にはリソース名が記され，リソースの中心にはリソースの現在の状態が記されています．
+

+ DTRAM の仮想実行では，メッセージを送りたいリソースをダブルクリックします．まず，book.owner リソースに，Init チャンネルを通じて，init("Suzuki") というメッセージを送ることを考えます．
+ book.owner リソースをダブルクリックします． +

+ リソースに送信できるメッセージを選択する画面が表示されるので，init を選択します． +

+ 次にリソースに送信するメッセージを入力します．ここでは，init("Suzuki") を入力します． +

+ 次の状態に遷移します．book.owner リソースの状態が，"Suzuki" に変わったことが分かります． +

+ 同様にして，book.addr リソースをダブルクリックして，Add チャンネルを通じて，add("Satou", "Tokyo") というメッセージを送ります．
+

+ book.addr リソースの子リソースとして，book.addr.Satou リソースが追加されたことが分かります． +

+ さらに，book.addr リソースをダブルクリックして，add("Tanaka", "Osaka") というメッセージを送ります．
+

+ book.addr リソースの子リソースとして，さらに book.addr.Tanaka リソースが追加されます． +

+ 次に，book.addr リソースをダブルクリックして， del("Satou") というメッセージを送ります．
+

+ del を選択して， del("Satou") を入力します． +

+ book.addr.Satou リソースが削除されました． +

+ DTRAM ではこのようにして実行が可視化されます． +

+
+【酒屋の在庫管理システムの仕様説明】へ + + + \ No newline at end of file diff --git a/img/Alloy/AlloySample.png b/img/Alloy/AlloySample.png deleted file mode 100644 index d9d4b0e..0000000 --- a/img/Alloy/AlloySample.png +++ /dev/null Binary files differ diff --git a/img/Alloy/AlloySimpleAddressBook.png b/img/Alloy/AlloySimpleAddressBook.png new file mode 100644 index 0000000..d9d4b0e --- /dev/null +++ b/img/Alloy/AlloySimpleAddressBook.png Binary files differ diff --git a/img/DTRAM/DTRAMSimpleAddressBook0.png b/img/DTRAM/DTRAMSimpleAddressBook0.png new file mode 100644 index 0000000..ff1963b --- /dev/null +++ b/img/DTRAM/DTRAMSimpleAddressBook0.png Binary files differ diff --git a/img/DTRAM/DTRAMSimpleAddressBook1.png b/img/DTRAM/DTRAMSimpleAddressBook1.png new file mode 100644 index 0000000..196159f --- /dev/null +++ b/img/DTRAM/DTRAMSimpleAddressBook1.png Binary files differ diff --git a/img/DTRAM/DTRAMSimpleAddressBook2.png b/img/DTRAM/DTRAMSimpleAddressBook2.png new file mode 100644 index 0000000..ffc3191 --- /dev/null +++ b/img/DTRAM/DTRAMSimpleAddressBook2.png Binary files differ diff --git a/img/DTRAM/DTRAMSimpleAddressBook3.png b/img/DTRAM/DTRAMSimpleAddressBook3.png new file mode 100644 index 0000000..de76774 --- /dev/null +++ b/img/DTRAM/DTRAMSimpleAddressBook3.png Binary files differ diff --git a/img/DTRAM/DTRAMSimpleAddressBook4.png b/img/DTRAM/DTRAMSimpleAddressBook4.png new file mode 100644 index 0000000..d8a7a97 --- /dev/null +++ b/img/DTRAM/DTRAMSimpleAddressBook4.png Binary files differ diff --git a/img/DTRAM/DTRAMSimpleAddressBook5.png b/img/DTRAM/DTRAMSimpleAddressBook5.png new file mode 100644 index 0000000..ea97b54 --- /dev/null +++ b/img/DTRAM/DTRAMSimpleAddressBook5.png Binary files differ diff --git a/img/DTRAM/DTRAMSimpleAddressBook6.png b/img/DTRAM/DTRAMSimpleAddressBook6.png new file mode 100644 index 0000000..fe4ecbc --- /dev/null +++ b/img/DTRAM/DTRAMSimpleAddressBook6.png Binary files differ diff --git a/img/DTRAM/DTRAMSimpleAddressBook7.png b/img/DTRAM/DTRAMSimpleAddressBook7.png new file mode 100644 index 0000000..419e5e7 --- /dev/null +++ b/img/DTRAM/DTRAMSimpleAddressBook7.png Binary files differ diff --git a/models/Alloy/SimpleAddressBook.als b/models/Alloy/SimpleAddressBook.als new file mode 100644 index 0000000..4eae20d --- /dev/null +++ b/models/Alloy/SimpleAddressBook.als @@ -0,0 +1,31 @@ +sig Name, Addr {} +sig Book { + owner: Name, + addr: Name -> lone Addr +} + +pred init[b: Book, n: Name] { + b.owner = n + no b.addr +} + +pred add[b, b': Book, n: Name, a: Addr] { + b'.owner = b.owner + b'.addr = b.addr + n -> a +} + +pred del[b, b': Book, n: Name] { + b'.owner = b.owner + b'.addr = b.addr - n -> b.addr[n] +} + +pred execute[] { + some disj b0, b1, b2, b3: Book, disj n0, n1, n2: Name, a0, a1: Addr | { + init[b0, n0] + add[b0, b1, n1, a0] + add[b1, b2, n2, a1] + del[b2, b3, n1 + } +} + +run execute for 2 but 4 Book, 3 Name diff --git a/models/DTRAM/SimpleAddressBook.model b/models/DTRAM/SimpleAddressBook.model new file mode 100644 index 0000000..9a9f38a --- /dev/null +++ b/models/DTRAM/SimpleAddressBook.model @@ -0,0 +1,11 @@ +channel Init { + out book.owner(pre_name: Str, init(name: Str)) = name +} + +channel Add { + out book.addr(pre_addr: Map, add(name: Str, addr: Str)) = insert(pre_addr, name, addr) +} + +channel Del { + out book.addr(pre_addr: Map, del(name: Str)) = delete(pre_addr, name) +} \ No newline at end of file