静岡大学の出身研究室で訳していた本の紹介。
Promelaという、元々は Protocol Meta Languageとして、通信規約を記述する言語。
その後、Process Meta Languageとして幅広く利用できることを示した。
Promelaの処理系が、Simple Promela Interpreter(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の紹介あり。
#参考資料
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.
最後までおよみいただきありがとうございました。
いいね 💚、フォローをお願いします。
Thank you very much for reading to the last sentence.
Please press the like icon 💚 and follow me for your happy life.