Synchronous Abstract Machines
作者： Carlo A. Furia , Dino Mandrioli , Angelo Morzenti , Matteo Rossi
DOI: 10.1007/978-3-642-32332-4_7
关键词: Automaton 、 Semantics (computer science) 、 State (computer science) 、 Theoretical computer science 、 Abstract machine 、 Model checking 、 Discrete time and continuous time 、 Transition system 、 Rotation formalisms in three dimensions 、 Computer science
摘要: In this chapter, we analyze state-based formalisms that extend the basic automata models of Chap. 6 with a notion time. The discussion progresses from simplest to richer and extensions can express sophisticated timing properties. First, introduce transition system, which is used provide semantics discussed in rest chapter later ones. Then, show how finite-state represent temporal features systems. We then discuss several classic model automata: Timed Transition Models Statecharts specific mechanisms for modeling discrete time, while timed hybrid include deal continuous shows probabilities be introduced automata; it concludes some design verification techniques tools based on presented earlier.
springer.com
sci-hub.st 参考文章(52)
Eugene Asarin, Challenges in Timed Languages: from applied theory to basic theory (Column: Concurrency). Bulletin of The European Association for Theoretical Computer Science. ,vol. 83, pp. 106- 120 ,(2004)
David Harel, Rivi Sherman, Amir Pnueli, Jeanette P. Schmidt, On the Formal Semantics of Statecharts (Extended Abstract) logic in computer science. pp. 54- 64 ,(1987)
Tom Bienmüller, Werner Damm, Hartmut Wittke, The Statemate Verification Environment computer aided verification. pp. 561- 567 ,(2000) , 10.1007/10722167_45
Rajeev Alur, P. Madhusudan, Decision Problems for Timed Automata : A Survey formal methods. ,vol. 3185, pp. 1- 24 ,(2004) , 10.1007/978-3-540-30080-9_1
Joost-Pieter Katoen, Christel Baier, Principles of Model Checking ,(2008)
Michael Beeck, A Comparison of Statecharts Variants international symposium organized jointly with working group provably correct systems on formal techniques in real time and fault tolerant systems. pp. 128- 148 ,(1994) , 10.1007/3-540-58468-4_163
Zohar Manna, Amir Pnueli, The temporal logic of reactive and concurrent systems ,(1992)
Goran Frehse, PHAVer: algorithmic verification of hybrid systems past hytech international conference on hybrid systems computation and control. pp. 258- 273 ,(2005) , 10.1007/978-3-540-31954-2_17
X. Nicollin, A. Olivero, J. Sifakis, S. Yovine, An Approach to the Description and Analysis of Hybrid Systems Hybrid Systems. pp. 149- 178 ,(1993) , 10.1007/3-540-57318-6_28
M. Archer, C. Heitmeyer, Mechanical verification of timed automata: a case study real time technology and applications symposium. pp. 192- 203 ,(1996) , 10.1109/RTTAS.1996.509536