SPIN: Simple Promela(protocol meta langauge) Interpreter

静岡大学の出身研究室で訳していた本の紹介。

Promelaという、元々は Protocol Meta Languageとして、通信規約を記述する言語。
その後、Process Meta Languageとして幅広く利用できることを示した。

Promelaの処理系が、Simple Promela Interpreter(SPIN)

出始めの

コンピュータプロトコルの設計法―正しいプロトコルの設計と検証へ導く総合解説書 
![413zZXb6L0L._SX353_BO1,204,203,200_.jpg](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/51423/0c81a240-6eb3-98cb-e87d-4af78f0a8d45.jpeg)
https://www.amazon.co.jp/dp/4906391109/

p.3
>のろしと警報

p.4
##1 
Histories. With an English translation by W.R. Paton
by Polybius; Paton, W. R. (William Roger), 1857-1921
https://archive.org/details/historieswitheng00polyuoft/page/n6

p.5
> プロトコル設計の最も難しい点は、予期できないことを明確に予想しておかなければならないことにある。

p.6
##2 
Sidereus Nuncius: The Starry Messenger
http://www.sites.hps.cam.ac.uk/starry/galsidnun.html
http://people.reed.edu/~wieting/mathematics537/SideriusNuncius.pdf

p.7
A.N. Edelcrantz, Avhandling om Tlelegrapher

The Use of Optical Telegraphs in England and Elsewhere (Die optis- che Telegraphie in England und anderen La ̈ndern)
Gerard J. Holzmann
https://pdfs.semanticscholar.org/242a/c5fa581c4ceaeda821d5ca00a034918a0104.pdf

p.9

p.20
>SDL（the Specification and Description Language), Lotos(The language of temporal ordering specification), Estelleの紹介あり。

# 参考資料
A multi-paradigm language for reactive synthesis
Ioannis Filippidis, Richard M. Murray, Gerard J. Holzmann
https://arxiv.org/abs/1602.01173

### Reference

[1] open-PROMELA compiler (PYTHON package). Available at https://github.com/johnyf/ openpromela.
[2] PROMELA parser (PYTHON package). Available at https://github.com/johnyf/promela.
[3] SLUGS instrumentation at tag synt 2015. Available at https://github.com/johnyf/slugs.
[4] dd: Decision diagrams (PYTHON package). Available at https://github.com/johnyf/dd.
[5] omega:Symbolicandenumerateddatastructuresandalgorithmsformanipulatingω-regularsets(PYTHON package). Available at https://github.com/johnyf/omega.
[6] Mart ́ın Abadi & Leslie Lamport (1994): Open systems in TLA. In: PODC, pp. 81–90, doi:10.1145/197917.197960.
[7] Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo MK Martin, Mukund Raghothaman, Sanjit A Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak & Abhishek Udupa (2013): Syntax-guided synthesis. In: FMCAD, pp. 1–17, doi:10.1109/FMCAD.2013.6679385.
[8] Rajeev Alur & Salvatore La Torre (2004): Deterministic generators and games for LTL fragments. ACM Trans. Comput. Logic 5(1), pp. 1–25, doi:10.1145/963927.963928.
[9] ARM Ltd. (1999): AMBATM Specification, Rev 2.0 edition. Available at http://www-micro.deis. unibo.it/~magagni/amba99.pdf.
[10] Christel Baier & Joost-Pieter Katoen (2008): Principles of model checking. The MIT Press.
[11] Michael Baldamus & Jochen Schro ̈der-Babo (2001): P2B: A translation utility for linking PROMELA and
symbolic model checking. In: SPIN, pp. 183–191, doi:10.1007/3-540-45139-0 11.
[12] Jiˇr ́ı Barnat, Lubosˇ Brim, Vojteˇch Havel, Jan Havl ́ıcˇek, Jan Kriho, Milan Lencˇo, Petr Rocˇkai, Vladim ́ır Sˇtill & Jiˇr ́ı Weiser (2013): DIVINE 3.0 – An explicit-state model checker for multithreaded C & C++ programs. In: CAV, 8044, pp. 863–868, doi:10.1007/978-3-642-39799-8 60.
[13] Vincent Beaudenon, Emmanuelle Encrenaz & Sami Taktak (2010): Data decision diagrams for promela systems analysis. STTT 12(5), pp. 337–352, doi:10.1007/s10009-010-0135-0.
[14] David M. Beazley: PLY (Python Lex-Yacc) v3.4. Available at http://www.dabeaz.com/ply/ply.html.
[15] Tewodros Beyene, Swarat Chaudhuri, Corneliu Popeea & Andrey Rybalchenko (2014): A constraint-based
approach to solving games on infinite graphs. In: POPL, pp. 221–233, doi:10.1145/2535838.2535860.
[16] Roderick Bloem, Alessandro Cimatti, Karin Greimel, Georg Hofferek, Robert Ko ̈nighofer, Marco Roveri, Viktor Schuppan & Richard Seeber (2010): RATSY–A new requirements analysis tool with synthesis. In: CAV, pp. 425–429, doi:10.1007/978-3-642-14295-6 37.
[17] Roderick Bloem, Stefan Galler, Barbara Jobstmann, Nir Piterman, Amir Pnueli & Martin Weiglhofer (2007): Interactive presentation: Automatic hardware synthesis from specifications: A case study. In: Design, Automation and Test in Europe (DATE), pp. 1188–1193. Available at http://dl.acm.org/ citation.cfm?id=1266366.1266622.
[18] Roderick Bloem, Stefan Galler, Barbara Jobstmann, Nir Piterman, Amir Pnueli & Martin Wei- glhofer (2007): Specify, compile, run: Hardware from PSL. ENTCS 190(4), pp. 3–16, doi:10.1016/j.entcs.2007.09.004.
[19] Roderick Bloem, Swen Jacobs & Ayrat Khalimov (2014): Parameterized synthesis case study: AMBA AHB. In Krishnendu Chatterjee, Ru ̈diger Ehlers & Susmit Jha, editors: SYNT, EPTCS 157, pp. 68–83, doi:10.4204/EPTCS.157.9. Available at http://arxiv.org/abs/1407.6580v1.
[20] Roderick Bloem, Barbara Jobstmann, Nir Piterman, Amir Pnueli & Yaniv Sa’ar (2012): Synthe- sis of reactive(1) designs. Journal of Computer and System Sciences (JCSS) 78(3), pp. 911–938, doi:10.1016/j.jcss.2011.08.007.
[21] AaronBohy,Ve ́roniqueBruye`re,EmmanuelFiliot,NaiyongJin&Jean-Franc ̧oisRaskin(2012):ACACIA+, a tool for LTL synthesis. In: CAV, pp. 652–657, doi:10.1007/978-3-642-31424-7 45.
[22] Manfred Broy (1986): A theory for nondeterminism, parallelism, communication, and concurrency. TCS 45(0), pp. 1–61, doi:10.1016/0304-3975(86)90040-X.
[23] Randal E. Bryant (1986): Graph-based algorithms for Boolean function manipulation. IEEE Trans. Com- put. 35(8), pp. 677–691, doi:10.1109/TC.1986.1676819.
[24] Roberto Cavada, Alessandro Cimatti, Charles Arthur Jochim, Gavin Keighren, Emanuele Olivetti, Marco Pistore, Marco Roveri & Andrei Tchaltsev (2010): NUSMV 2.5 User Manual. Technical Report, Fon- dazione Bruno Kessler, 18 Via Sommarive, 38055 Povo (Trento), Italy.
[25] AshokK.Chandra,DexterC.Kozen&LarryJ.Stockmeyer(1981):Alternation.JACM28(1),pp.114–133, doi:10.1145/322234.322243.
[26] Frank Ciesinski, Christel Baier, Marcus Gro ̈ßer & David Parker (2008): Generating compact MTBDD- representations from Probmela specifications. In: SPIN, pp. 60–76, doi:10.1007/978-3-540-85114-1 7.
[27] Edsger W. Dijkstra (1975): Guarded commands, nondeterminacy and formal derivation of programs. CACM 18(8), pp. 453–457, doi:10.1145/360933.360975.
[28] M.B. Dwyer, G.S. Avrunin & J.C. Corbett (1999): Patterns in property specifications for finite-state verifi- cation. In: ICSE, pp. 411–420, doi:10.1145/302405.302672.
[29] Ru ̈diger Ehlers (2011): Experimental aspects of synthesis. EPTCS 50, doi:10.4204/EPTCS.50.
[30] Ru ̈diger Ehlers (2011): Generalized Rabin(1) synthesis with applications to robust system synthesis. In:
NFM, pp. 101–115, doi:10.1007/978-3-642-20398-5 9.
[31] Ru ̈diger Ehlers (2011): Unbeast: Symbolic bounded synthesis. In: TACAS, pp. 272–275, doi:10.1007/978-
3-642-19835-9 25.
[32] Ru ̈diger Ehlers & Vasumathi Raman (2014): Low-effort specification debugging and analysis. EPTCS 157, pp. 117–133, doi:10.4204/EPTCS.157.12.
[33] Ioannis Filippidis & contributors (2013): List of verification and synthesis tools. Available at https: //github.com/johnyf/tool_lists/blob/master/verification_synthesis.md.
[34] Ioannis Filippidis & Richard M. Murray (2015): Revisiting the AMBA AHB bus case study. Technical Report CaltechCDSTR:2015.004, California Institute of Technology, Pasadena, CA. Available at http: //resolver.caltech.edu/CaltechCDSTR:2015.004.
[35] Ioannis Filippidis, Richard M. Murray & Gerard J. Holzmann (2015): Synthesis from multi-paradigm spec- ifications. Technical Report CaltechCDSTR:2015.003, California Institute of Technology, Pasadena, CA. Available at http://resolver.caltech.edu/CaltechCDSTR:2015.003.
[36] Bernd Finkbeiner & Sven Schewe (2013): Bounded synthesis. International Journal on Software Tools for Technology Transfer (STTT) 15(5-6), pp. 519–539, doi:10.1007/s10009-012-0228-z.
[37] Robert W. Floyd (1967): Nondeterministic algorithms. JACM 14(4), pp. 636–644,
doi:10.1145/321420.321422.
[38] Bjorn N. Freeman-Benson (1990): KALEIDOSCOPE: Mixing objects, constraints, and imperative program-
ming. In: OOPSLA/ECOOP, pp. 77–88, doi:10.1145/97946.97957.
[39] Bjørn N. Freeman-Benson & Alan Borning (1992): Integrating constraints with an object-oriented lan-
guage. In: ECOOP, pp. 268–286, doi:10.1007/BFb0053042.
[40] B.N. Freeman-Benson & A Borning (1992): The design and implementation of KALEIDOSCOPE’90-A
constraint imperative programming language. In: ICCL, pp. 174–180, doi:10.1109/ICCL.1992.185480.
[41] Abdoulaye Gamatie ́ (2010): Designing embedded systems with the Signal programming language: syn-
chronous, reactive specification. Springer, doi:10.1007/978-1-4419-0941-1.
[42] Jeff Gennari, Shaun Hedrick, Fred Long, Justin Pincar & Robert Seacord (2007): Ranged integers for the C programming language. Technical Note CMU/SEI-2007-TN-027, Software Engineering Institute, Carnegie Mellon University. Available at http://resources.sei.cmu.edu/library/asset-view. cfm?AssetID=8265.
[43] Yashdeep Godhal, Krishnendu Chatterjee & Thomas A Henzinger (2013): Synthesis of AMBA AHB from formal specification: a case study. International Journal on Software Tools for Technology Transfer (STTT) 15(5-6), pp. 585–601, doi:10.1007/s10009-011-0207-9.
[44] Nicolas Halbwachs (1993): Synchronous programming of reactive systems. Engineering and Computer Science 215, Springer, doi:10.1007/978-1-4757-2231-4. Available at http://www-verimag.imag.fr/ ~halbwach/newbook.pdf.
[45] Charles Antony Richard Hoare (1985, 2004): Communicating sequential processes. 178, Prentice-Hall. Available at http://www.usingcsp.com/cspbook.pdf.
[46] Gerard J. Holzmann: PROMELA Language Reference (http: // spinroot. com/ spin/ Man/ promela. html ). Available at http://spinroot.com/spin/Man/promela.html.
[47] Gerard J. Holzmann (2003): The SPIN model checker: Primer and reference manual. Addison-Wesley.
[48] Yong Jiang & Zongyan Qiu (2012): S2N: model transformation from SPIN to NUSMV. In: SPIN, pp.
255–260, doi:10.1007/978-3-642-31759-0 20.
[49] BarbaraJobstmann&RoderickBloem(2006):OptimizationsforLTLsynthesis.In:FMCAD,pp.117–124, doi:10.1109/FMCAD.2006.22.
[50] BarbaraJobstmann,StefanGaller,MartinWeiglhofer&RoderickBloem(2007):ANZU:Atoolforproperty synthesis. In: CAV, pp. 258–262, doi:10.1007/978-3-540-73368-3 29.
[51] Barbara Jobstmann, Andreas Griesmayer & Roderick Bloem (2005): Program repair as a game. In: CAV, pp. 226–238, doi:10.1007/11513988 23.
[52] Muriel Jourdan, Fabienne Lagnier, R Maraninchi & Pascal Raymond (1994): A multiparadigm language for reactive systems. In: ICCL, pp. 211–218, doi:10.1109/ICCL.1994.288379.
[53] Robert M. Keller (1976): Formal verification of parallel programs. CACM 19(7), pp. 371–384, doi:10.1145/360248.360251.
[54] Yonit Kesten, Amir Pnueli & Li-on Raviv (1998): Algorithmic verification of linear temporal logic specifi- cations. In: ICALP, 1443, pp. 1–16, doi:10.1007/BFb0055036.
[55] Uri Klein, Nir Piterman & Amir Pnueli (2012): Effective synthesis of asynchronous systems from GR(1) specifications. In: VMCAI, pp. 283–298, doi:10.1007/978-3-642-27940-9 19.
[56] M. Kloetzer & C. Belta (2008): A fully automated framework for control of linear systems from temporal logic specifications. TAC 53(1), pp. 287–297, doi:10.1109/TAC.2007.914952.
[57] H. Kress-Gazit, G.E. Fainekos & G.J. Pappas (2009): Temporal-logic-based reactive mission and motion planning. IEEE Transactions on Robotics (TRO) 25(6), pp. 1370–1381, doi:10.1109/TRO.2009.2030225.
[58] Daniel Kroening & Ofer Strichman (2008): Decision procedures: An algorithmic point of view. Springer.
[59] O. Kupferman & M.Y. Vardi (2005): Safraless decision procedures. In: FOCS, pp. 531–540,
doi:10.1109/SFCS.2005.66.
[60] Orna Kupferman (2012): Recent challenges and ideas in temporal synthesis. In: SOFSEM, pp. 88–98, doi:10.1007/978-3-642-27660-6 8.
[61] Leslie Lamport (1994): The Temporal Logic of Actions. ACM Trans. Program. Lang. Syst. 16(3), pp. 872–923, doi:10.1145/177492.177726.
[62] Leslie Lamport (2002): Specifying systems: The TLA+ language and tools or hardware and software engineers. Addison-Wesley. Available at http://research.microsoft.com/en-us/um/people/ lamport/tla/book.html.
[63] Leslie Lamport & Fred B. Schneider (1985): Constraints: A uniform approach to aliasing and typing. In: POPL, pp. 205–216, doi:10.1145/318593.318640.
[64] K Rustan M Leino (2010): Dafny: An automatic program verifier for functional correctness. In: LPAR, 6355, pp. 348–370, doi:10.1007/978-3-642-17511-4 20.
[65] ASolarLezama(2008):Programsynthesisbysketching.Ph.D.thesis,Citeseer.Availableathttp://www. eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-177.html.
[66] Orna Lichtenstein, Amir Pnueli & Lenore Zuck (1985): The glory of the past. In: Logics of Programs, 193, pp. 196–218, doi:10.1007/3-540-15648-8 16.
[67] Scott C. Livingston, Richard M. Murray & Joel W. Burdick (2012): Backtracking temporal logic synthesis for uncertain environments. In: ICRA, pp. 5163–5170, doi:10.1109/ICRA.2012.6225208.
[68] Gus Lopez, Bjorn Freeman-Benson & Alan Borning (1994): Implementing constraint imperative programming languages: The KALEIDOSCOPE’93 virtual machine. In: OOPSLA, pp. 259–271, doi:10.1145/191080.191118.
[69] Z Manna & Amir Pnueli (1990): Tools and rules for the practicing verifier. Technical Report CS-TR-90- 1321, Stanford University, CA, USA. Available at http://i.stanford.edu/pub/cstr/reports/cs/ tr/90/1321/CS-TR-90-1321.pdf.
[70] Zohar Manna & Amir Pnueli (1989): The anchored version of the temporal framework. In: Linear time, branching time and partial order in Logics and models for concurrency, LNCS 354, Springer, pp. 201–284, doi:10.1007/BFb0013024.
[71] Zohar Manna & Amir Pnueli (1990): A hierarchy of temporal properties. In: PODC, pp. 377–410, doi:10.1145/93385.93442.
[72] Shahar Maoz & Yaniv Sa’ar (2011): ASPECTLTL: An aspect language for LTL specifications. In: Aspect- oriented Software Development (AOSD), ACM, pp. 19–30, doi:10.1145/1960275.1960280.
[73] John McCarthy (1959): A basis for a mathematical theory of computation. In P. Braffort & D. Hirschberg, editors: Computer Programming and Formal Systems, Studies in Logic and the Foundations of Mathemat- ics 26, North-Holland, pp. 33–70, doi:10.1016/S0049-237X(09)70099-0.
[74] KennethLauchlinMcMillan(1992):Symbolicmodelchecking:Anapproachtothestateexplosionproblem. Ph.D. thesis, Carnegie Mellon University, Pittsburgh, PA, USA, doi:10.1007/978-1-4615-3190-6. Available at http://www.kenmcmil.com/pubs/thesis.pdf. UMI Order No. GAX92-24209.
[75] George H Mealy (1955): A method for synthesizing sequential circuits. Bell System Technical Journal 34(5), pp. 1045–1079, doi:10.1002/j.1538-7305.1955.tb03788.x.
[76] Edward F Moore (1956): Gedanken-experiments on sequential machines. Automata studies 34, pp. 129– 153.
[77] A. Morgenstern (2010): Symbolic controller synthesis for LTL specifications. Ph.D. thesis, Com- puter Science. Available at http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:hbz: 386-kluedo-25721.
[78] A. Morgenstern & K. Schneider (2011): A LTL fragment for GR(1)-synthesis. EPTCS 50, pp. 33–45, doi:10.4204/EPTCS.50.3.
[79] David E Muller, Ahmed Saoudi & Paul E Schupp (1986): Alternating automata, the weak monadic theory
of the tree, and its complexity. In: ICALP, pp. 275–283, doi:10.1007/3-540-16761-7 77.
[80] Elie Najm & Frank Olsen (1996): Protocol verification with Reactive PROELA/RSPIN. In: SPIN, pp. 109–
128. Available at http://spinroot.com/spin/Workshops/ws96/Ol.pdf.
[81] Elie Najm & Frank Olsen (1996): Reactive EFSMs — Reactive Promela/RSPIN. In: TACAS, pp. 349–368,
doi:10.1007/3-540-61042-1 54.
[82] Shipra Panda & Fabio Somenzi (1995): Who are the variables in your neighbourhood. In: ICCAD, pp. 74–77, doi:10.1109/ICCAD.1995.479994.
[83] Nir Piterman, Amir Pnueli & Yaniv Sa’ar (2006): Synthesis of reactive(1) designs. In: VMCAI, pp. 364– 380, doi:10.1007/11609773 24.
[84] A. Pnueli & R. Rosner (1989): On the synthesis of a reactive module. In: POPL, pp. 179–190, doi:10.1145/75277.75293.
[85] Amir Pnueli (1977): The temporal logic of programs. In: FOCS, pp. 46 –57, doi:10.1109/SFCS.1977.32.
[86] Amir Pnueli & Uri Klein (2009): Synthesis of programs from temporal property specifications. In: MEM-
OCODE, pp. 1–7, doi:10.1109/MEMCOD.2009.5185372.
[87] Amir Pnueli & Roni Rosner (1989): On the synthesis of an asynchronous reactive module. In: ICALP, pp.
652–671, doi:10.1007/BFb0035790.
[88] Amir Pnueli, Yaniv Sa’ar & Lenore D Zuck (2010): JTLV: A framework for developing verification algo-
rithms. In: CAV, pp. 171–174, doi:10.1007/978-3-642-14295-6 18.
[89] Roni Rosner (1992): Modular synthesis of reactive systems. Ph.D. thesis, Weizmann Institute of Science, Rehovot, Israel. Available at http://www.researchgate.net/publication/238759536_Modular_ synthesis_of_reactive_systems/file/50463527f8b648c3ba.pdf.
[90] Richard Rudell (1993): Dynamic variable ordering for ordered binary decision diagrams. In: ICCAD, pp. 42–47, doi:10.1109/ICCAD.1993.580029.
[91] MatthiasSchlaipfer,GeorgHofferek&RoderickBloem(2012):Generalizedreactivity(1)synthesiswithout a monolithic strategy. In: HSVT, pp. 20–34, doi:10.1007/978-3-642-34188-5 6.
[92] Klaus Schneider (2004): Verification of reactive systems: formal methods and algorithms. Springer, doi:10.1007/978-3-662-10778-2.
[93] Saqib Sohail, Fabio Somenzi & Kavita Ravi (2008): A hybrid algorithm for LTL games. In: VMCAI, pp. 309–323, doi:10.1007/978-3-540-78163-9 26.
[94] Fabio Somenzi (2012): CUDD: CU Decision Diagram package - release 2.5.0. University of Colorado at Boulder. Available at http://vlsi.colorado.edu/~fabio/CUDD/cuddIntro.html.
[95] Harald Søndergaard & Peter Sestoft (1992): Non-determinism in functional languages. The Computer Journal 35(5), pp. 514–523, doi:10.1093/comjnl/35.5.514.
[96] Wolfgang Thomas (2008): Solution of Church’s Problem: A tutorial. New Perspectives on Games and interaction 5.
[97] Peter Van-Roy & Seif Haridi (2004): Concepts, techniques, and models of computer programming. MIT press.
[98] Moshe Y Vardi (1995): Alternating automata and program verification. In: Computer Science Today, Springer, pp. 471–485, doi:10.1007/BFb0015261.
[99] Moshe Y Vardi (1996): An automata-theoretic approach to linear temporal logic. In: Logics for concur- rency, LNCS 1043, Springer, pp. 238–266, doi:10.1007/3-540-60915-6 6.
[100] Igor Walukiewicz (2004): A Landscape with games in the background. LICS 0, pp. 356–366, doi:10.1109/LICS.2004.1319630.
[101] Tichakorn Wongpiromsarn, Ufuk Topcu & Richard M Murray (2013): Synthesis of control protocols for autonomous systems. Unmanned Systems 1(01), pp. 21–39, doi:10.1142/S2301385013500027.


<この項は書きかけです。順次追記します。>
This article is not completed. I will add some words and/or centences in order.
Este artículo no está completo. Agregaré algunas palabras en orden.

## 知人資料
' @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

## 自己記事一覧
Qiitaで逆リンクを表示しなくなったような気がする。時々、スマフォで表示するとあらわることがあり、完全に削除したのではなさそう。2024年４月以降、せっせとリンクリストを作り、統計を取って確率を説明しようとしている。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

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

祝休日・謹賀新年 2025年の目標
https://qiita.com/kaizen_nagoya/items/dfa34827932f99c59bbc

Qiita 1年間をまとめた「振り返りページ」＠2024
https://qiita.com/kaizen_nagoya/items/ed6be239119c99b15828

2024 参加・主催Calendarと投稿記事一覧 Qiita(248)
https://qiita.com/kaizen_nagoya/items/d80b8fbac2496df7827f

主催Calendar2024分析 Qiita(254)
https://qiita.com/kaizen_nagoya/items/15807336d583076f70bc

Calendar 統計
https://qiita.com/kaizen_nagoya/items/e315558dcea8ee3fe43e

LLM 関連 Calendar 2024 
https://qiita.com/kaizen_nagoya/items/c36033cf66862d5496fa

Large Language Model Related Calendar 
https://qiita.com/kaizen_nagoya/items/3beb0bc3fb71e3ae6d66

博士論文 Calendar 2024 を開催します。 
https://qiita.com/kaizen_nagoya/items/51601357efbcaf1057d0

博士論文(0)関連記事一覧
https://qiita.com/kaizen_nagoya/items/8f223a760e607b705e78

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

日本のプログラマが世界で戦える16分野。仮説(53),統計と確率(25) 転職(32)、Ethernet(58)
https://qiita.com/kaizen_nagoya/items/a7e634a996cdd02bc53b

小川メソッド　覚え（書きかけ）
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

水道局10年(1976,4-1986,3)を振り返る
https://qiita.com/kaizen_nagoya/items/707fcf6fae230dd349bf

小川清最終講義、最終講義（再）計画, 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.
Este artículo es una impresión personal basada en mi experiencia personal. No tiene nada que ver con la organización o empresa a la que pertenezco actualmente.
### 文書履歴(document history)
ver. 0.01 初稿 　20250518
### 最後までおよみいただきありがとうございました。
いいね　💚、フォローをお願いします。
#### Thank you very much for reading to the last sentence.
Please press the like icon 💚　and follow me for your happy life.
#### Muchas gracias por leer hasta la última oración.
Por favor, haz clic en el ícono Me gusta 💚 y sígueme para tener una vida feliz.