開放系相互接続（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.9
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
#参考資料(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:nbn
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.
#自己参考資料(self reference)
OSI参照モデルの資料を作り始める（作業中）
「コンピュータプロトコルの設計法」に学ぶ
IT業界における国際規格等の利用。仮説・検証（22）
AUTOSAR
overlapped definition in AUTOSAR short name. over 50.:英語(49)
＜この記事は個人の過去の経験に基づく個人の感想です。現在所属する組織、業務とは関係がありません。＞
最後までおよみいただきありがとうございました。
いいね 💚、フォローをお願いします。
Thank you very much for reading to the last sentence.
Please press the like icon 💚 and follow me for your happy life.