*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] );

トップ   編集 差分 バックアップ 添付 複製 名前変更 リロード   新規 一覧 単語検索 最終更新   ヘルプ   最終更新のRSS