Verifying Protocol Conformance Using Software Model Checking for the Model-Driven Development of Embedded Systems
Issue No. 09 - Sept. (2013 vol. 39)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2013.14
Yann Moffett , CF 18 Avionics System Engineering, Ottawa
Juergen Dingel , Queens University, Kingston
Alain Beaulieu , Royal Military College, Kingston
To facilitate modular development, the use of state machines has been proposed to specify the protocol (i.e., the sequence of messages) that each port of a component can engage in. The protocol conformance checking problem consists of determining whether the actual behavior of a component conforms to the protocol specifications on its ports. In this paper, we consider this problem in the context of the model-driven development (MDD) of embedded systems based on UML 2, in which UML 2 state machines are used to specify component behavior. We provide a definition of conformance which slightly extends those found in the literature and reduce the conformance check to a state space exploration. We describe a tool implementing the approach using the Java PathFinder software model checker and the MDD tool IBM Rational RoseRT, discuss its application to three case studies, and show how the tool repeatedly allowed us to find unexpected conformance errors with encouraging performance. We conclude that the approach is promising for supporting the modular development of embedded components in the context of industrial applications of MDD.
Unified modeling language, Protocols, Ports (Computers), Software, Safety, Context, Java, software model checking, Component-based software engineering, behavioral interface specifications, software modeling, model-driven development, formal specification and verification
A. Beaulieu, J. Dingel and Y. Moffett, "Verifying Protocol Conformance Using Software Model Checking for the Model-Driven Development of Embedded Systems," in IEEE Transactions on Software Engineering, vol. 39, no. , pp. 1307-13256, 2013.