AUTOSAR CountdownAdvent Calendar 2022Day 3

ISO/IEC OSIに学ぶ通信(102)

Last updated at 2024-08-25Posted at 2019-08-29

開放系相互接続（Open Systems Interconnection）は、
ISO 7498:1984 Open Systems Interconnection - Basic Reference Model
https://www.iso.org/standard/14252.html

<この項は書きかけです。順次追記します。>

人月の神話を読むと、OSIの課題がわかるかもしれない。

人月の神話
https://qiita.com/kaizen_nagoya/items/e38c97a8a468c7fc5743

ただし、OSIの話は、ソフトウェアの話よりは、ハードウェアの話を中心にした方がいいかもしれない。

OSIに沿った安いハードウェア、CPU、ネットワークICを、誰かが作って売り出せば、生き残ったかもしれないから。

大きさと複雑さがあっても、それ論理回路で設計して、安く売り出すかどうかが鍵かもしれない。

論理的な、組織的な議論だけに振り回されない方がよいかもというのがOSIに学ぶ点かもしれない。

LOTOS

研修生で訪問していた電総研（現在の産総研）の言語システム研究室で、
Lotosの研究をされていた方がおみえになった。

ISO 8807:1989　INFORMATION PROCESSING SYSTEMS -- OPEN SYSTEMS INTERCONNECTION -- LOTOS -- A FORMAL DESCRIPTION TECHNIQUE BASED ON THE TEMPORAL ORDERING OF OBSERVATIONAL BEHAVIOUR
https://www.iso.org/standard/16258.html

OBJ to Lotosという研究発表の座長をしたことがあり、内容を真剣に読んだ。

また一部の規格審議がISO/IEC JTC1 SC７で審議することになり、当時国内幹事をしていたため拝読したことあり。

SPIN

博士課程の学生で在籍した静岡大学の研究室グループでは、SPINの翻訳をされていた。

コンピュータプロトコルの設計法―正しいプロトコルの設計と検証へ導く総合解説書

 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.20

SDL（the Specification and Description Language), Lotos(The language of temporal ordering specification), Estelle

の紹介あり。

自分では手をつけることもなく過ごした。
その間に、やれる人はやっていた。

ModelChecking技術の専門性の排除とその効用
An EarlyBird as the 2nd eye
富士ゼロックス株式会社オフィスプロダクト事業本部コントローラソフトウェア開発部
野村秀樹/服部彰宏/村石理恵/山本訓稔 2008 年 1月30日
http://www.jasst.jp/archives/jasst08e/pdf/B4-2.pdf

実際に知ったのはIPAの行事。

プロセス改善セミナー事例紹介 IPA
https://www.ipa.go.jp/files/000005103.pdf

あわてて名古屋で講演をお願いした。

UMLとモデル検証に関する講演会
https://www.toppers.jp/TOPPERS-USERS/200906/msg00001.html

ITU

国際電気通信連合
https://www.itu.int/en/ITU-T/

以前は、言語系の標準が無料でダウンロードできた。
ISO/IEC JTC1と連携して審議していた規格もあった。
現在、調査中。

Draft revised Rec. Z.100 Specification and Description Language - Overview of SDL-2010 (for Consent)
https://www.itu.int/md/T17-SG17-190827-TD-PLEN-2171

ITU-T X.210 (11/1993) ISO/IEC 10731:1994 Information technology – Open Systems Interconnection – Basic Reference Model: Conventions for the definition of OSI services
https://www.itu.int/ITU-T/recommendations/rec.aspx?rec=2828&lang=en

ITU-T X.904 (12/1997) ISO/IEC 10746-4:1998 Information technology – Open Distributed Processing – Reference Model: Architectural Semantics

ITU-T Z.100 App. II (03/1993) SDL bibliography
https://www.itu.int/ITU-T/recommendations/rec.aspx?rec=3161&lang=en

OSI

今、OSIに学ぶことは、アプリケーション層、プレゼンテーション層、セッション層を分けることにより、セキュリティを強化できるかどうかだろうか。

OSI参照モデル

大きすぎ、複雑すぎて失敗したというOSIでも、一番基礎の参照モデルはその後も参照されている。
１００作ったうちの残った１つがOSI参照モデルと言えるだろうか。

OSI参照モデルについて
https://qiita.com/play-life/items/b7571d7ca51a8e13e479

OSI参照モデル
https://qiita.com/twinkle13531/items/6821d6a11be5a3c17837

OSI参照モデルまとめ
https://qiita.com/upopo/items/798b01814851b8f2b39f

プロトコルとOSI参照モデル
https://qiita.com/hgaiji/items/dbb845f5b631e5cf3bc9

「OSI参照モデル」と「RFC1122」(「OSI参照モデル」に戸惑わないために)
https://qiita.com/Black_Kite/items/bc3c5789ccba807b0755

OSI参照モデルまとめ
https://qiita.com/tatsuya4150/items/474b60beed0c04d5d999

[初心者向け]プロトコルとOSI基本参照モデル
https://qiita.com/tochisuke221/items/9a516746a4db3bafc08e

OSI基本参照モデルについて
https://qiita.com/saeco_cco/items/ec3f5f43d047173babd4

ネットワーク　OSI参照モデルの表
https://qiita.com/keitean/items/2010884715a04738da8d

OSI参照モデルとTCP/IP
https://qiita.com/mk185/items/a25a6c08702162ae04f5

OSI参照モデル
https://qiita.com/obukoh/items/fa84aca41ea1c7aee7b4

OSI参照モデル
https://qiita.com/kuromame1020614/items/461b2fba3ca231ceb5c5

OSI参照モデル
https://qiita.com/naoyakenkyo/items/50e9817792fb5c8133d7

OSI参照モデルについてまとめてみた
https://qiita.com/masaya8028/items/f4d405a58fdf839faf72

参考資料(reference)

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:nbnhbz: 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.

自己参考資料(self　reference)

ISO OSI 7層の実例：自動車用診断通信(diagnostics communication)、Ethernet(53)
https://qiita.com/kaizen_nagoya/items/f52ad61f557f000de2d5

ISO/IEC OSIに学ぶ通信(102)
https://qiita.com/kaizen_nagoya/items/89562c52f37d6bf0a80d

OSI参照モデルの資料を作り始める（作業中）
https://qiita.com/kaizen_nagoya/items/26e1451ef4981c46b3be

「コンピュータプロトコルの設計法」に学ぶ
https://qiita.com/kaizen_nagoya/items/a55ff39bba4ac3cb9069

IT業界における国際規格等の利用。仮説・検証（22）
https://qiita.com/kaizen_nagoya/items/0e2ab72fbddc391d4f41

AUTOSAR

overlapped definition in AUTOSAR short name. over 50.:英語(49)
https://qiita.com/kaizen_nagoya/items/9a171ee6a74163d128e9

自己記事一覧

Qiitaで逆リンクを表示しなくなったような気がする。時々、スマフォで表示するとあらわっることがあり、完全に削除したのではなさそう。

４月以降、せっせとリンクリストを作り、統計を取って確率を説明しようとしている。
2025年２月末を目標にしている。

物理記事　上位100
https://qiita.com/kaizen_nagoya/items/66e90fe31fbe3facc6ff

量子(0) 計算機, 量子力学
https://qiita.com/kaizen_nagoya/items/1cd954cb0eed92879fd4

数学関連記事１００
https://qiita.com/kaizen_nagoya/items/d8dadb49a6397e854c6d

統計(0)一覧
https://qiita.com/kaizen_nagoya/items/80d3b221807e53e88aba

図(0) state, sequence and timing. UML and お絵描き
https://qiita.com/kaizen_nagoya/items/60440a882146aeee9e8f

品質一覧
https://qiita.com/kaizen_nagoya/items/2b99b8e9db6d94b2e971

言語・文学記事　１００
https://qiita.com/kaizen_nagoya/items/42d58d5ef7fb53c407d6

医工連携関連記事一覧
https://qiita.com/kaizen_nagoya/items/6ab51c12ba51bc260a82

自動車　記事　１００
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/f77520d378d33451d6fe

仮説（0）一覧（目標100現在40）
https://qiita.com/kaizen_nagoya/items/f000506fe1837b3590df

音楽　一覧(0)
https://qiita.com/kaizen_nagoya/items/b6e5f42bbfe3bbe40f5d

「@kazuo_reve 新人の方によく展開している有益な情報」確認一覧
https://qiita.com/kaizen_nagoya/items/b9380888d1e5a042646b

Qiita(0)Qiita関連記事一覧（自分）
https://qiita.com/kaizen_nagoya/items/58db5fbf036b28e9dfa6

鉄道（０）鉄道のシステム考察はてっちゃんがてつだってくれる
https://qiita.com/kaizen_nagoya/items/26bda595f341a27901a0

安全（0）安全工学シンポジウムに向けて: 21
https://qiita.com/kaizen_nagoya/items/c5d78f3def8195cb2409

一覧の一覧( The directory of directories of mine.) Qiita(100)
https://qiita.com/kaizen_nagoya/items/7eb0e006543886138f39

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

OSEK OS設計の基礎　OSEK(100)
https://qiita.com/kaizen_nagoya/items/7528a22a14242d2d58a3

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

coding (101) 一覧を作成し始めた。omake:最近のQiitaで表示しない5つの事象
https://qiita.com/kaizen_nagoya/items/20667f09f19598aedb68

プログラマによる、プログラマのための、統計(0)と確率のプログラミングとその後
https://qiita.com/kaizen_nagoya/items/6e9897eb641268766909

なぜdockerで機械学習するか書籍・ソース一覧作成中 (目標100)
https://qiita.com/kaizen_nagoya/items/ddd12477544bf5ba85e2

言語処理100本ノックをdockerで。python覚えるのに最適。:10+12
https://qiita.com/kaizen_nagoya/items/7e7eb7c543e0c18438c4

プログラムちょい替え（0）一覧:4件
https://qiita.com/kaizen_nagoya/items/296d87ef4bfd516bc394

Python(0)記事をまとめたい。
https://qiita.com/kaizen_nagoya/items/088c57d70ab6904ebb53

官公庁・学校・公的団体（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

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 初稿　20190829

最後までおよみいただきありがとうございました。

いいね　💚、フォローをお願いします。

Thank you very much for reading to the last sentence.

Please press the like icon 💚　and follow me for your happy life.

You get articles that match your needs
You can efficiently read back useful information
You can use dark theme

What you can do with signing up

ISO/IEC OSIに学ぶ通信(102)

LOTOS

SPIN

1

2

ITU

OSI

OSI参照モデル

参考資料(reference)

Reference

自己参考資料(self　reference)

AUTOSAR

関連資料

Engineering Festa 2024前に必読記事一覧

自己記事一覧

文書履歴(document history)

最後までおよみいただきありがとうございました。

Thank you very much for reading to the last sentence.

ISO/IEC OSIに学ぶ 通信(102)

LOTOS

SPIN

1

2

ITU

OSI

OSI参照モデル

参考資料(reference)

Reference

自己参考資料(self reference)

AUTOSAR

関連資料

Engineering Festa 2024前に必読記事一覧

自己記事一覧

文書履歴(document history)

最後までおよみいただきありがとうございました。

Thank you very much for reading to the last sentence.

ISO/IEC OSIに学ぶ通信(102)

自己参考資料(self　reference)