#freeze
[[Fukunaga Lab Wiki]]

「並行システムのモデル化・検証・実装」
本位田真一 監修 磯部祥尚 著

を読み進めていく。


第一回
*第一回

2014/04/15(火)
第一章 FDR , CSP , JCSP 概論

主にこれから学んでいく、モデル検査器FDR,プロセス代数CSP,JAVAライブラリJCSPについて見た。

プロセス代数では、複雑なプロセスでも、イベントの実行可能性に着目した等価性を考えることで、わかりやすい逐次的なプロセスと等価であると示すことで、どのようなプロセスかを判別することができる。

FDRやJCSPの使い方を見た。

[[スライド(pptxファイル):http://tmubdell.math.se.tmu.ac.jp/wiki/M_ZEMI_DATA_2014/0415_M_Zemi.pptx]]

第二回
*第二回

2014/04/22(火)
第二章 CSP検証の基礎

第一章では曖昧だった等価性の意味を明確に定義し、新しい概念である詳細化関係についても学んだ。
実際にFDRを用いて検証した。

[[スライド(pptxファイル):http://tmubdell.math.se.tmu.ac.jp/wiki/M_ZEMI_DATA_2014/0422_M_Zemi_Nishimura.pptx]]



第三回
*第三回

2014/04/29 (火)
第三章 CSP実装の基礎

JCSPプログラミングの基礎となるチャネルについて、実際にJCSPによる実装で検証した.

[[スライド(pptxファイル):http://tmubdell.math.se.tmu.ac.jp/wiki/M_ZEMI_DATA_2014/0429_M_Zemi.pptx]]


*第四回

2014/05/13 (火)
第四章 CSP入門

内部選択や隠蔽などの基本演算子を再確認し、「哲学者の食事問題」を取り扱った。
また、等価性や詳細化関係などの証明をCSP規則をもとに行えることを確認した。

[[スライド(pptxファイル):http://tmubdell.math.se.tmu.ac.jp/wiki/M_ZEMI_DATA_2014/0513_M_Zemi.pptx]]


*第五回

2014/05/20(火)
第五章 FDR入門

FDRでのデータの扱い方を確認し、FDRの詳しい機能・使い方を説明した。

[[スライド(pptxファイル):http://tmubdell.math.se.tmu.ac.jp/wiki/M_ZEMI_DATA_2014/0520_M_Zemi_Nishimura.pptx]]


*第六回

2014/5/27 (火) 及び 2014/6/3 (火)

これまで定義してきたCSP演算子をJCSPによる実装の為の変換

[[スライド(pptxファイル):http://tmubdell.math.se.tmu.ac.jp/wiki/M_ZEMI_DATA_2014/0527-0603_M_Zemi.pptx]]


*第八回

2014/06/10(火),
2014/06/24(火),
2014/07/01(火)

第七章 CSP , FDR , JCSP 応用

1つのPC上で並行動作する複数のプロセスをネットワークチャネルを利用して、
複数のPC上で分散プログラムとして実行することが可能である例を見てきた。


[[スライド(pptxファイル):http://tmubdell.math.se.tmu.ac.jp/wiki/M_ZEMI_DATA_2014/0610_M_Zemi.pptx]]

[[演習プログラム(zipファイル):http://tmubdell.math.se.tmu.ac.jp/wiki/M_ZEMI_DATA_2014/NetParCom.zip]]

[[CNSServerを通した複数のWorkerの利用により、素数をリストアップするプログラム(zipファイル):http://tmubdell.math.se.tmu.ac.jp/wiki/M_ZEMI_DATA_2014/Prime.zip]]

<**プログラムは学内限定でダウンロード可能**>


トップ   新規 一覧 単語検索 最終更新   ヘルプ   最終更新のRSS