並行システムの設計検証入門セミナー
ツールを使いながら並行システムの基礎を学ぶハンズオンセミナーを受講しようかなって思った。．
https://principia.connpass.com/event/315368/
ツール 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
https://www.cs.ox.ac.uk/files/6237/Document.pdf
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 not completed. I will add some words and/or centences in order.
Qiita Calendar 2024
2024 参加・主催Calendarと投稿記事一覧 Qiita(248)
https://qiita.com/kaizen_nagoya/items/d80b8fbac2496df7827f
主催Calendar2024分析 Qiita(254)
https://qiita.com/kaizen_nagoya/items/15807336d583076f70bc
博士論文 Calendar 2024 を開催します。
https://qiita.com/kaizen_nagoya/items/51601357efbcaf1057d0
博士論文(0)関連記事一覧
https://qiita.com/kaizen_nagoya/items/8f223a760e607b705e78
自己記事一覧
Qiitaで逆リンクを表示しなくなったような気がする。時々、スマフォで表示するとあらわっることがあり、完全に削除したのではなさそう。
４月以降、せっせとリンクリストを作り、統計を取って確率を説明しようとしている。
2025年２月末を目標にしている。
一覧の一覧( The directory of directories of mine.) Qiita(100)
https://qiita.com/kaizen_nagoya/items/7eb0e006543886138f39
仮説（0）一覧（目標100現在40）
https://qiita.com/kaizen_nagoya/items/f000506fe1837b3590df
Qiita(0)Qiita関連記事一覧（自分）
https://qiita.com/kaizen_nagoya/items/58db5fbf036b28e9dfa6
Error一覧 error(0)
https://qiita.com/kaizen_nagoya/items/48b6cbc8d68eae2c42b8
C++ Support(0)
https://qiita.com/kaizen_nagoya/items/8720d26f762369a80514
Coding(0) Rules, C, Secure, MISRA and so on
https://qiita.com/kaizen_nagoya/items/400725644a8a0e90fbb0
Ethernet 記事一覧 Ethernet(0)
https://qiita.com/kaizen_nagoya/items/88d35e99f74aefc98794
Wireshark 一覧 wireshark(0)、Ethernet(48)
https://qiita.com/kaizen_nagoya/items/fbed841f61875c4731d0
線網（Wi-Fi）空中線(antenna)(0) 記事一覧(118/300目標)
https://qiita.com/kaizen_nagoya/items/5e5464ac2b24bd4cd001
なぜdockerで機械学習するか 書籍・ソース一覧作成中 (目標100)
https://qiita.com/kaizen_nagoya/items/ddd12477544bf5ba85e2
プログラムちょい替え（0）一覧:4件
https://qiita.com/kaizen_nagoya/items/296d87ef4bfd516bc394
言語処理100本ノックをdockerで。python覚えるのに最適。:10+12
https://qiita.com/kaizen_nagoya/items/7e7eb7c543e0c18438c4
Python(0)記事をまとめたい。
https://qiita.com/kaizen_nagoya/items/088c57d70ab6904ebb53
安全（0）安全工学シンポジウムに向けて: 21
https://qiita.com/kaizen_nagoya/items/c5d78f3def8195cb2409
プログラマによる、プログラマのための、統計(0)と確率のプログラミングとその後
https://qiita.com/kaizen_nagoya/items/6e9897eb641268766909
転職(0)一覧
https://qiita.com/kaizen_nagoya/items/f77520d378d33451d6fe
技術士(0)一覧
https://qiita.com/kaizen_nagoya/items/ce4ccf4eb9c5600b89ea
Reserchmap(0) 一覧
https://qiita.com/kaizen_nagoya/items/506c79e562f406c4257e
物理記事 上位100
https://qiita.com/kaizen_nagoya/items/66e90fe31fbe3facc6ff
量子(0) 計算機, 量子力学
https://qiita.com/kaizen_nagoya/items/1cd954cb0eed92879fd4
数学関連記事１００
https://qiita.com/kaizen_nagoya/items/d8dadb49a6397e854c6d
coq(0) 一覧
https://qiita.com/kaizen_nagoya/items/d22f9995cf2173bc3b13
統計(0)一覧
https://qiita.com/kaizen_nagoya/items/80d3b221807e53e88aba
図(0) state, sequence and timing. UML and お絵描き
https://qiita.com/kaizen_nagoya/items/60440a882146aeee9e8f
色(0) 記事100書く切り口
https://qiita.com/kaizen_nagoya/items/22331c0335ed34326b9b
品質一覧
https://qiita.com/kaizen_nagoya/items/2b99b8e9db6d94b2e971
言語・文学記事 １００
https://qiita.com/kaizen_nagoya/items/42d58d5ef7fb53c407d6
医工連携関連記事一覧
https://qiita.com/kaizen_nagoya/items/6ab51c12ba51bc260a82
水の資料集(0) 方針と成果
https://qiita.com/kaizen_nagoya/items/f5dbb30087ea732b52aa
自動車 記事 １００
https://qiita.com/kaizen_nagoya/items/f7f0b9ab36569ad409c5
通信記事１００
https://qiita.com/kaizen_nagoya/items/1d67de5e1cd207b05ef7
日本語（０）一欄
https://qiita.com/kaizen_nagoya/items/7498dcfa3a9ba7fd1e68
英語(0) 一覧
https://qiita.com/kaizen_nagoya/items/680e3f5cbf9430486c7d
音楽 一覧(0)
https://qiita.com/kaizen_nagoya/items/b6e5f42bbfe3bbe40f5d
「@kazuo_reve 新人の方によく展開している有益な情報」確認一覧
https://qiita.com/kaizen_nagoya/items/b9380888d1e5a042646b
鉄道（０）鉄道のシステム考察はてっちゃんがてつだってくれる
https://qiita.com/kaizen_nagoya/items/faa4ea03d91d901a618a
OSEK OS設計の基礎 OSEK(100)
https://qiita.com/kaizen_nagoya/items/7528a22a14242d2d58a3
coding (101) 一覧を作成し始めた。omake:最近のQiitaで表示しない5つの事象
https://qiita.com/kaizen_nagoya/items/20667f09f19598aedb68
官公庁・学校・公的団体（NPOを含む）システムの課題、官（０）
https://qiita.com/kaizen_nagoya/items/04ee6eaf7ec13d3af4c3
「はじめての」シリーズ ベクタージャパン
https://qiita.com/kaizen_nagoya/items/2e41634f6e21a3cf74eb
AUTOSAR(0)Qiita記事一覧, OSEK(75)
https://qiita.com/kaizen_nagoya/items/89c07961b59a8754c869
プログラマが知っていると良い「公序良俗」
https://qiita.com/kaizen_nagoya/items/9fe7c0dfac2fbd77a945
LaTeX(0) 一覧
https://qiita.com/kaizen_nagoya/items/e3f7dafacab58c499792
自動制御、制御工学一覧（０）
https://qiita.com/kaizen_nagoya/items/7767a4e19a6ae1479e6b
Rust(0) 一覧
https://qiita.com/kaizen_nagoya/items/5e8bb080ba6ca0281927
関連資料
' @kazuo_reve 私が効果を確認した「小川メソッド」
https://qiita.com/kazuo_reve/items/a3ea1d9171deeccc04da
' @kazuo_reve 新人の方によく展開している有益な情報
https://qiita.com/kazuo_reve/items/d1a3f0ee48e24bba38f1
' @kazuo_reve Vモデルについて勘違いしていたと思ったこと
https://qiita.com/kazuo_reve/items/46fddb094563bd9b2e1e
Engineering Festa 2024前に必読記事一覧
programの本質は計画だ。programは設計だ。
https://qiita.com/kaizen_nagoya/items/c8545a769c246a458c27
登壇直後版 色使い(JIS安全色) Qiita Engineer Festa 2023〜私しか得しないニッチな技術でLT〜 スライド編 0.15
https://qiita.com/kaizen_nagoya/items/f0d3070d839f4f735b2b
プログラマが知っていると良い「公序良俗」
https://qiita.com/kaizen_nagoya/items/9fe7c0dfac2fbd77a945
逆も真：社会人が最初に確かめるとよいこと。OSEK(69)、Ethernet(59)
https://qiita.com/kaizen_nagoya/items/39afe4a728a31b903ddc
統計の嘘。仮説（127）
https://qiita.com/kaizen_nagoya/items/63b48ecf258a3471c51b
自分の言葉だけで論理展開できるのが天才なら、文章の引用だけで論理展開できるのが秀才だ。仮説（136）
https://qiita.com/kaizen_nagoya/items/97cf07b9e24f860624dd
参考文献駆動執筆(references driven writing)・デンソークリエイト編
https://qiita.com/kaizen_nagoya/items/b27b3f58b8bf265a5cd1
「何を」よりも「誰を」。１０年後のために今見習いたい人たち
https://qiita.com/kaizen_nagoya/items/8045978b16eb49d572b2
Qiitaの記事に３段階または５段階で到達するための方法
https://qiita.com/kaizen_nagoya/items/6e9298296852325adc5e
出力(output)と呼ばないで。これは状態(state)です。
https://qiita.com/kaizen_nagoya/items/80b8b5913b2748867840
coding (101) 一覧を作成し始めた。omake:最近のQiitaで表示しない5つの事象
https://qiita.com/kaizen_nagoya/items/20667f09f19598aedb68
あなたは「勘違いまとめ」から、勘違いだと言っていることが勘違いだといくつ見つけられますか。人間の間違い(human error(125))の種類と対策
https://qiita.com/kaizen_nagoya/items/ae391b77fffb098b8fb4
プログラマの「プログラムが書ける」思い込みは強みだ。３つの理由。仮説（168）統計と確率(17) , OSEK(79)
https://qiita.com/kaizen_nagoya/items/bc5dd86e414de402ec29
出力(output)と呼ばないで。これは状態(state)です。
https://qiita.com/kaizen_nagoya/items/80b8b5913b2748867840
これからの情報伝達手段の在り方について考えてみよう。炎上と便乗。
https://qiita.com/kaizen_nagoya/items/71a09077ac195214f0db
ISO/IEC JTC1 SC7 Software and System Engineering
https://qiita.com/kaizen_nagoya/items/48b43f0f6976a078d907
アクセシビリティの知見を発信しよう！（再び）
https://qiita.com/kaizen_nagoya/items/03457eb9ee74105ee618
統計論及確率論輪講（再び）
https://qiita.com/kaizen_nagoya/items/590874ccfca988e85ea3
読者の心をグッと惹き寄せる7つの魔法
https://qiita.com/kaizen_nagoya/items/b1b5e89bd5c0a211d862
「@kazuo_reve 新人の方によく展開している有益な情報」確認一覧
https://qiita.com/kaizen_nagoya/items/b9380888d1e5a042646b
ソースコードで議論しよう。日本語で議論するの止めましょう（あるプログラミング技術の議論報告）
https://qiita.com/kaizen_nagoya/items/8b9811c80f3338c6c0b0
脳内コンパイラの3つの危険
https://qiita.com/kaizen_nagoya/items/7025cf2d7bd9f276e382
心理学の本を読むよりはコンパイラ書いた方がよくね。仮説（34）
https://qiita.com/kaizen_nagoya/items/fa715732cc148e48880e
NASAを超えるつもりがあれば読んでください。
https://qiita.com/kaizen_nagoya/items/e81669f9cb53109157f6
データサイエンティストの気づき!「勉強して仕事に役立てない人。大嫌い!!」『それ自分かも?』ってなった!!!
https://qiita.com/kaizen_nagoya/items/d85830d58d8dd7f71d07
「ぼくの好きな先生」「人がやらないことをやれ」プログラマになるまで。仮説（37）
https://qiita.com/kaizen_nagoya/items/53e4bded9fe5f724b3c4
なぜ経済学徒を辞め、計算機屋になったか（経済学部入学前・入学後・卒業後対応） 転職(1)
https://qiita.com/kaizen_nagoya/items/06335a1d24c099733f64
プログラミング言語教育のXYZ。 仮説（52）
https://qiita.com/kaizen_nagoya/items/1950c5810fb5c0b07be4
【24卒向け】9ヶ月後に年収１０００万円を目指す。二つの関門と三つの道。
https://qiita.com/kaizen_nagoya/items/fb5bff147193f726ad25
「【25卒向け】Qiita Career Meetup for STUDENT」予習の勧め
https://qiita.com/kaizen_nagoya/items/00eadb8a6e738cb6336f
大学入試不合格でも筆記試験のない大学に入って卒業できる。卒業しなくても博士になれる。
https://qiita.com/kaizen_nagoya/items/74adec99f396d64b5fd5
全世界の不登校の子供たち「博士論文」を書こう。世界子供博士論文遠隔実践中心 安全(99)
https://qiita.com/kaizen_nagoya/items/912d69032c012bcc84f2
小川メソッド 覚え（書きかけ）
https://qiita.com/kaizen_nagoya/items/3593d72eca551742df68
DoCAP（ドゥーキャップ）って何ですか？
https://qiita.com/kaizen_nagoya/items/47e0e6509ab792c43327
views 20,000越え自己記事一覧
https://qiita.com/kaizen_nagoya/items/58e8bd6450957cdecd81
Views１万越え、もうすぐ１万記事一覧 最近いいねをいただいた213記事
https://qiita.com/kaizen_nagoya/items/d2b805717a92459ce853
amazon 殿堂入りNo1レビュアになるまで。仮説(102)
https://qiita.com/kaizen_nagoya/items/83259d18921ce75a91f4
100以上いいねをいただいた記事16選
https://qiita.com/kaizen_nagoya/items/f8d958d9084ffbd15d2a
小川清最終講義、最終講義（再）計画, Ethernet(100) 英語(100) 安全(100)
https://qiita.com/kaizen_nagoya/items/e2df642e3951e35e6a53
＜この記事は個人の過去の経験に基づく個人の感想です。現在所属する組織、業務とは関係がありません。＞
This article is an individual impression based on my individual 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.