*LTSAまとめサイト [#e3937379] *LTSAとは [#l0006181] モデリング検査ツール FSP(Finite State Processes)で書いた式から 状態遷移図をグラフィカルに生成して、イベントが起こるとどのステートに遷移するか手動で動かしてみることができる。 *LTSAのモデルからprologのプログラムに変換するスクリプト [#za2f4a6e] -[[組み込みソフトウェアの設計&検証>http://shop.cqpub.co.jp/hanbai/books/33/33441.html]] の著者の藤倉 俊幸様作成のスクリプトです。 ※作者様の許可を頂いて掲載しております。 ※作者様の許可を頂いて掲載しております。ありがとうございます。 [[ダウンロード>http://garyo.sakura.ne.jp/LTSA/index.php?plugin=attach&pcmd=open&file=%B8%F8%B3%AB%CD%D1Prolog%B2%BD%BD%E8%CD%FD.zip&refer=FrontPage]] [[LTSAのモデルからprologのプログラムに変換するスクリプト使用方法]] *LTSAダウンロード先 [#p9d22d8c] http://www.doc.ic.ac.uk/~jnm/book/ こちらの[[here>http://www.doc.ic.ac.uk/~jnm/book/ltsa/download.html]]をクリックし [[download ltsa>http://www.doc.ic.ac.uk/~jnm/book/ltsa/ltsatool.zip]]をクリックします *LTSA使い方 [#k15a6f97] +日本語による解説 -[[ 並行システムのモデル化と分析 -- ツールLTSAを用いて>http://www.graco.c.u-tokyo.ac.jp/~tamai/concurrency.html]] +[[FSP Quick Reference>http://www.doc.ic.ac.uk/~jnm/book/ltsa/Appendix-A-2e.html]] -Finite State Processes -[[モデル検査(2)プロセス代数に基づくモデリング>http://www.google.co.jp/url?sa=t&ct=res&cd=4&url=http%3A%2F%2Flis2.huie.hokudai.ac.jp%2F~kurihara%2Fclasses%2FProgram%2Ffsp.ppt&ei=BMc-SPfrCo_ssgKZoqyUCw&usg=AFQjCNE0Bs_NuBBm5MdmNDNWEqg-w_w7Fw&sig2=bh2THKCPHTfk5sB3ijo-7w]]FSPの解説(日本語) *簡単な使い方 [#p64f3271] [[簡単な使い方]] *プラグイン [#v9b66c7c] **MSC [#c89c0a97] シーケンス図から状態遷移図を作ってくれるLTSAプラグイン。ただしVer3.0では使えない -http://www.doc.ic.ac.uk/ltsa/msc/ *参考書籍 [#hb7f704e] -[[組み込みソフトウェアの設計&検証>http://shop.cqpub.co.jp/hanbai/books/33/33441.html]] LTSAを使ったモデル検証の説明が載っています #counter( [total| today| yesterday] );