Formal Modeling and Analysis of the Modbus Protocol
Modbus is a communication protocol that is widely used in SCADA systems and distributed control applications. This paper presents formal specifications of Modbus developed using PVS, a generic theorem prover; and SAL, a toolset for the automatic analysis of state-transition systems. Both formalizations are based on the Modbus Application Protocol, which specifies the format of Modbus request and response messages. This formal modeling effort is the first step in the development of automated methods for systematic and extensive testing of Modbus devices.
Keywords: Modbus, formal methods, modeling, test-case generation
KeywordsModel Checker Function Code Bounded Model Checker Master Device SCADA System
- P. Ammann, P. Black and W. Majurski, Using model checking to generate tests from specifications, Proceedings of the Second IEEE International Conference on Formal Engineering Methods, pp. 46-54, 1998.Google Scholar
- L. de Moura, S. Owre, H. Ruess, J. Rushby, N. Shankar, M. Sorea and A. Tiwari, SAL 2, in Proceedings of the Sixteenth International Conference on Computer Aided Verification (LNCS 3114), R. Alur and D. Peled (Eds. ), Springer, Berlin-Heidelberg, Germany, pp. 496-500, 2004.Google Scholar
- L. de Moura, S. Owre and N. Shankar, The SAL Language Manual, Tech- nical Report SRI-CSL-01-02, SRI International, Menlo Park, California, 2003.Google Scholar
- B. Dutertre, Formal Modeling and Analysis of the Modbus Protocol, Tech- nical Report, SRI International, Menlo Park, California, 2006.Google Scholar
- A. Gargantini and C. Heitmeyer, Using model checking to generate tests from requirements specifications, in Proceedings of the Seventh Euro- pean Software Engineering Conference (LNCS 1687), O. Nierstrasz and M. Lemoine (Eds. ), Springer, Berlin-Heidelberg, Germany, pp. 146-162, 1999.Google Scholar
- D. Geist, M. Farkas, A. Landver, Y. Lichtenstein, S. Ur and Y. Wolf- sthal, Coverage-directed test generation using symbolic techniques, in Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (LNCS 1166), M. Srivas and A. Camilleri (Eds. ), Springer, Berlin-Heidelberg, Germany, pp. 143-158, 1996.CrossRefGoogle Scholar
- G. Hamon, L. de Moura and J. Rushby, Generating efficient test sets with a model checker, Proceedings of the Second International Conference on Software Engineering and Formal Methods, pp. 261-270, 2004.Google Scholar
- Modbus IDA, MODBUS Application Protocol Specification v1. 1a, North Grafton, Massachusetts (www.modbus. org/specs. php), June 4, 2004.
- Modbus IDA, MODBUS Messaging on TCP/IP Implementation Guide v1. 0a, North Grafton, Massachusetts (www.modbus. org/specs. php), June 4, 2004.
- Modbus. org, MODBUS over Serial Line Specification and Implementation Guide v1. 0, North Grafton, Massachusetts (www.modbus. org/specs. php ), February 12, 2002.
- S. Rayadurgam and M Heimdahl, Coverage based test-case generation using model checkers, Proceedings of the Eighth Annual IEEE International Conference and Workshop on the Engineering of Computer Based Systems, pp. 83-91, 2001.Google Scholar
- V. Rusu, L. du Bousquet and T. Jéron, An approach to symbolic test generation, in Proceedings of the Second International Conference on Integrated Formal Methods (LNCS 1945), W. Grieskamp, T. Santen and B. Stoddart (Eds. ), Springer, Berlin-Heidelberg, Germany, pp. 338-357, 2000.Google Scholar