Verification and implementation of software for dependable controllers
作者： Krzysztof Sacha
DOI: 10.1504/IJCCBS.2010.031717
关键词:
摘要: A method is described for modelling, verification and automatic generation of code PLC controllers. The requirements a controller are modelled using UML state machine diagram, with formal semantics given by finite time machine. model can automatically be converted into timed automaton, embedded the environment (a controlled plant) verified against safety UPPAAL – free checking tool networks automata. translated program in one IEC 61131 languages, e.g., ladder diagram structured text.
pw.edu.pl
researchgate.net 
sci-hub.se 参考文章(14)
Zohar Manna, Amir Pnueli, Temporal Verification of Reactive Systems Springer New York. ,(1995) , 10.1007/978-1-4612-4222-2
Kurt Jensen, Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use ,(2011)
Zohar Manna, Amir Pnueli, Temporal Verification of Reactive Systems: Safety ,(1995)
Robin MILNER, Operational and algebraic semantics of concurrent processes Handbook of theoretical computer science (vol. B). pp. 1201- 1242 ,(1991) , 10.1016/B978-0-444-88074-1.50024-X
Krzysztof Sacha, Translatable finite state time machine SDL'07 Proceedings of the 13th international SDL Forum conference on Design for dependable systems. pp. 117- 132 ,(2007) , 10.1007/978-3-540-74984-4_8
K. Jensen, Coloured Petri nets Discrete Event Systems: A New Challenge for Intelligent Control Systems, IEE Colloquium on. ,(1993)
Pavel Krčál, Leonid Mokrushin, P. S. Thiagarajan, Wang Yi, Timed vs. Time-Triggered Automata CONCUR 2004 - Concurrency Theory. pp. 340- 354 ,(2004) , 10.1007/978-3-540-28644-8_22
Gerd Behrmann, Alexandre David, Kim G. Larsen, A Tutorial on UPPAAL formal methods. pp. 200- 236 ,(2004) , 10.1007/978-3-540-30080-9_7
Krzysztof Sacha, Verification and Implementation of Dependable Controllers international conference on dependability of computer systems. pp. 143- 151 ,(2008) , 10.1109/DEPCOS-RELCOMEX.2008.30
T.A. Henzinger, X. Nicollin, J. Sifakis, S. Yovine, Symbolic model checking for real-time systems Information & Computation. ,vol. 111, pp. 193- 244 ,(1994) , 10.1006/INCO.1994.1045