Formal Modeling and Analysis of the Modbus Protocol

  • Bruno Dutertre
Part of the IFIP International Federation for Information Processing book series (IFIPAICT, volume 253)

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


Model Checker Function Code Bounded Model Checker Master Device SCADA System 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. [1]
    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
  2. [2]
    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
  3. [3]
    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
  4. [4]
    B. Dutertre, Formal Modeling and Analysis of the Modbus Protocol, Tech- nical Report, SRI International, Menlo Park, California, 2006.Google Scholar
  5. [5]
    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
  6. [6]
    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
  7. [7]
    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
  8. [8]
    Modbus IDA, MODBUS Application Protocol Specification v1. 1a, North Grafton, Massachusetts (www.modbus. org/specs. php), June 4, 2004.
  9. [9]
    Modbus IDA, MODBUS Messaging on TCP/IP Implementation Guide v1. 0a, North Grafton, Massachusetts (www.modbus. org/specs. php), June 4, 2004.
  10. [10]
    Modbus. org, MODBUS over Serial Line Specification and Implementation Guide v1. 0, North Grafton, Massachusetts (www.modbus. org/specs. php ), February 12, 2002.
  11. [11]
    S. Owre, J. Rushby, N. Shankar and F. von Henke, Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS, IEEE Transactions on Software Engineering, vol. 21(2), pp. 107-125, 1995.CrossRefGoogle Scholar
  12. [12]
    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
  13. [13]
    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

Copyright information

© IFIP International Federation for Information Processing 2008

Authors and Affiliations

  • Bruno Dutertre
    • 1
  1. 1.SRI InternationalMenlo ParkUSA

Personalised recommendations