並行システムの設計検証入門セミナー
ツールを使いながら並行システムの基礎を学ぶハンズオンセミナーを受講しようかなって思った。．
ツール SyncStitch がインストールされた MS-Windows PC （マウスが必須です）
以下のページの Releases から syncstitch-4.3.1-win.zip をダウンロードしてください。
https://github.com/hatsugai/SyncStitch
mac, Linux でもビルドすれば動作しますが、当方で動作確認ができないため、サポート外とさせていただきます。ご自分でリスクを取られる分にはかまいません。
<この項は書きかけです。順次追記します。>
This article is not completed. I will add some words in order.
トップエスイー実践講座 第6巻
並行システムの検証と実装 形式手法CSPに基づく高信頼並行システム開発入門 監修 東野 輝夫 著者 磯部 祥尚
https://www.kindaikagaku.co.jp/book_list/detail/9784764904354/
をkindleで購入した。
macOS, Linuxサポート検討中。
主要目次
- CSP, FDR, JCSP 概論
- CSP入門
- FDR入門
- JCSP入門
- CSP理論（動作表現）
- CSP理論（動作解析）
- FDR検証
CSP: Communicating Sequential Processes
C. A. R. Hoare December 4, 2022
http://www.usingcsp.com/cspbook.pdf
FDR: Failures-Divergence Refinement
FDR2
https://www.cs.ox.ac.uk/projects/concurrency-tools/download/fdr2manual-2.94.pdf
FDR2 User Manual 17 May 2012
Formal Systems (Europe) Ltd
http://www.fsel.com/
Oxford University Computing Laboratory http://www.cs.ox.ac.uk/projects/concurrency-tools/
FDR3
FDR4
JCSP
Communicating Sequential Processes for JAVA
docker/syncstitch 導入してみる。
SyncStitch
A Refinement Checker based on CSP
Copyright (C) 2020-2022 Hisabumi Hatsugai
Documents
SyncStitch Reference
Dependencies
ocaml-csp
Guedra
Guedra-draw
In addition, GTK+ 3 is needed for macOS, which can be installed through Homebrew:
brew install gtk+3
Install
Download an executable file from the release page.
Build
see and run build-SyncStitch.sh
$ docker run -it gcc /bin/bash
# apt update; apt -y upgrade
ocaml
ocaml-csp
参考文献
[1] Philip Armstrong, Gavin Lowe, Tomasz Mazur, Joel Ouaknine, and Bill Roscoe. CSP
model checking: New technology and techniques.
http://www.comlab.ox.ac.uk/projects/cspmodel checking/.
[2] G. Behrmann, A. David, and K. G. Larsen. A Tutorial on UPPAAL. 2004.
http://www.uppaal.com/.
[3] J. Bowen. The Occam archive. http://formalmethods.wikia.com/wiki/Occam.
[4] Ronald S. Cok. Parallel Programs for the Transputer. Prentices-Hall, 1991. より日本語訳 「Transputer/occam による並列プログラミング入門」 が出版されている.
[5] CSPJAPAN. CSP 0537. http://www.cspjapan.org/.
[6] University of Oxford Department of Computer Science. Concurrency tools.
http://web.comlab.ox.ac.uk/projects/concurrency-tools/.
[7] E. W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of pro-
grams. Commun. ACM, Vol. 18, No. 8, pp. 453-457, 1975.
http://www.cs.toronto.edu/~chechik/courses05/csc410/readings/dijkstra.pdf
[8] C. A. R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.
http://www.usingcsp.com/cspbook.pdf よりダウンロード可能。 また、丸善よ
り日本語訳が出版されている: C.A.R. ホーア (著), 吉田 信博 (訳) ホーア CSP モデ VOA, 2002.
[9] G. Holzmann. The SPIN Model Checker. Addison-Wesley, 2004.
[10] Maven Hub. The jcsp library - JCSP-1.1-rc5.
http://mavenhub.com/mvn/central/org.codehaus.jcsp/jcsp/1.1-rc5.
[11] Y. Isobe and M. Roggenbach. Webpage on CSP-Prover.
http://staff.aist.go.jp/y-isobe/CSP-Prover/CSP-Prover.html.
[12] Y. Isobe and M. Roggenbach. A generic theorem prover of CSP refinement. In Nicolas Halbwachs and Lenore D. Zuck, editors, TACAS 2005, LNCS 3440, pp. 108-123.
Springer, 2005.
https://staff.aist.go.jp/y-isobe/publication/CSP-Prover-TACAS05.pdf
[13] Y. Isobe and M. Roggenbach. A complete axiomatic semantics for the CSP stable-
failures model. In Christel Baier and Holger Hermanns, editors, CONCUR 2005,
LNCS 4137, pp. 158-172. Springer, 2006.
https://staff.aist.go.jp/y-isobe/CSP-Prover/papers/CSP-Prover-CONCUR06.pdf
[14] Jonathan Lawrence. Practical application of CSP and FDR to software design. In
A.E. Abdallah, C. B. Jones, and J. W. Sanders, editors, Communicating Sequential
Processes - The First 25 Years, LNCS 3525, pp. 151-174. Springer, 2004.
[15] Formal Systems (Europe) Limited. Failures-Divergence Refinement: FDR2.
http://www.fsel.com/.
[16] Formal Systems (Europe) Limited. Failures-Divergence Refinement: Fdr2 user man-
ual. http://www.fsel.com/documentation/fdr2/fdr2manual.pdf.
[17] K. L. McMillan. Symbolic Model Checking. Springer, 1993.
[18] Peter Welch (University of Kent). Communicating sequential processes for java
(JCSP). http://www.cs.kent.ac.uk/projects/ofa/jcsp/.
[19] University of Kent. JCSP networking - some tutorial examples.
http://projects.cs.kent.ac.uk/projects/jcsp/svn/jcsp/trunk/JCSP Networking.pdf.
[20] National University of Singapore. PAT: Process analysis toolkit.
http://www.comp.nus.edu.sg/"pat/.
[21] Jan Peleska. Applied formal methods - from CSP to executable hybrid specifications. In A.E. Abdallah, C. B. Jones, and J. W. Sanders, editors, Communicating Sequential Processes-The First 25 Years, LNCS 3525, pp. 293-320. Springer, 2004.
[22] A. W. Roscoe. The Theory and Practice of Concurrency. Prentice Hall, 1998. *
http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/pubs.html (No.68)よりダウンロード可能.
[23] A. W. Roscoe, Paul H. B. Gardiner, Michael Goldsmith, J. R. Hulance, D. M. Jackson, and J. B. Scattergood. Hierarchical compression for model-checking CSP or how tocheck 1020
dining philosophers for deadlock. In TACAS 1995, LNCS 1019, pp. 133-152, 1995.
[24] Mark Russinovich. Process Explorer v11.21. 2008.
http://www.microsoft.com/technet/sysinternals/.
[25] P. Ryan, S. Schneider, M. Goldsmith, G. Lowe, and B. Roscoe. The Modelling and
Analysis of Security Protocols: the CSP Approach. Addison-Wesley, 2001.
[26] Davide Sangiorgi and David Walker. PI-Calculus: A Theory of Mobile Processes.
Cambridge University Press, New York, NY, USA, 2001.
[27] Steve Schneider. Concurrent and Real Time Systems: The CSP Approach. John Wiley
& Sons, Inc., New York, NY, USA, 1st edition, 1999.
[28] Steve Schneider and Rob Delicata. Verifying security protocols: An application of
CSP. In A.E. Abdallah, C. B. Jones, and J. W. Sanders, editors, Communicating
Sequential Processes - The First 25 Years, LNCS 3525, pp. 244–263. Springer, 2004.
[29] P. Welch, N. Brown, J. Moores, K. Chalmers, and B. Sputh. Integrating and extending JCSP. In Communicating Process Architectures 2007, pp. 349–370. IOS Press, 2007. http://www.cs.kent.ac.uk/projects/ofa/jcsp/jcsp-paper-2007.pdf.
[30] XMOS. イベント駆動型マルチコアプロセッサ. http://www.xmos.com/jp.
[31] 磯部祥尚. トップエスイー講座 「並行システムの検証と実装」 . http://staff.aist.go.jp/y-isobe/topse/vic/.
[32]. Prominent network. http://members.jcom.home.ne.jp/1355/.
[33] 吉岡信和, 青木利晃, 田原康之. SPIN による設計モデル検証 モデル検査の実践ソフトウェア検証 (トップエスイー実践講座) 近代科学社, 2008.
[34] 中島震. SPIN モデル検査検証モデリング技法 近代科学社, 2008.
自己参照
docker ひさびさで先に進まぬ
https://qiita.com/kaizen_nagoya/items/707444af0fb4d4808fd3
職業プログラマ以外のプログラマに贈る現代計算機事情
https://qiita.com/kaizen_nagoya/items/f199d82bbfae47f3dd87
並行システムの検証と実装 形式手法CSPに基づく高信頼並行システム開発入門 磯部 祥尚 著
https://qiita.com/kaizen_nagoya/items/26306952534a7b713eca
＜この記事は個人の過去の経験に基づく個人の感想です。現在所属する組織、業務とは関係がありません。＞
This article is an individual impression based on the individual's experience. It has nothing to do with the organization or business to which I currently belong.
文書履歴(document history)
ver. 0.01 初稿 20240313
最後までおよみいただきありがとうございました。
いいね 💚、フォローをお願いします。
Thank you very much for reading to the last sentence.
Please press the like icon 💚 and follow me for your happy life.