Formal Modeling and Analysis of the Modbus Protocol
作者： Bruno Dutertre
DOI: 10.1007/978-0-387-75462-8_14
关键词:
摘要: Modbus is a communication protocol widely used in SCADA systems and distributed control applications. This report describes formal models of the protocol. Two formalizations are presented: first was developed using PVS generic theorem prover second SAL, an environment for automatic analysis state-transition model checking tools. Both based on Application Protocol Specification [9], application-layer part standard. specifies format command response messages that application can use to communicate with sensor or actuator devices. The goal modeling effort study automated methods systematic extensive testing
springer.com
sri.com 
sci-hub.st 参考文章(8)
Daniel Geist, Monica Farkas, Avner Landver, Yossi Lichtenstein, Shmuel Ur, Yaron Wolfsthal, Coverage-Directed Test Generation Using Symbolic Techniques formal methods in computer-aided design. pp. 143- 158 ,(1996) , 10.1007/BFB0031805
Vlad Rusu, Lydie du Bousquet, Thierry Jéron, An Approach to Symbolic Test Generation integrated formal methods. pp. 338- 357 ,(2000) , 10.1007/3-540-40911-4_20
P.E. Ammann, P.E. Black, W. Majurski, Using model checking to generate tests from specifications international conference on formal engineering methods. pp. 46- 54 ,(1998) , 10.1109/ICFEM.1998.730569
Angelo Gargantini, Constance Heitmeyer, Using model checking to generate tests from requirements specifications foundations of software engineering. ,vol. 24, pp. 146- 162 ,(1999) , 10.1145/318774.318939
S. Owre, J. Rushby, N. Shankar, F. von Henke, Formal verification for fault-tolerant architectures: prolegomena to the design of PVS IEEE Transactions on Software Engineering. ,vol. 21, pp. 107- 125 ,(1995) , 10.1109/32.345827
J. Rushby, L. de Moura, G. Hamon, Generating efficient test sets with a model checker software engineering and formal methods. pp. 261- 270 ,(2004) , 10.1109/SEFM.2004.21
Leonardo de Moura, Sam Owre, N. Shankar, The SAL Language Manual ,(2003)
S. Rayadurgam, M.P.E. Heimdahl, Coverage based test-case generation using model checkers engineering of computer based systems. pp. 83- 91 ,(2001) , 10.1109/ECBS.2001.922409