The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.09 - Sept. (2013 vol.39)
pp: 1307-13256
Yann Moffett , CF 18 Avionics System Engineering, Ottawa
Juergen Dingel , Queens University, Kingston
Alain Beaulieu , Royal Military College, Kingston
ABSTRACT
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.
INDEX TERMS
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
CITATION
Yann Moffett, Juergen Dingel, Alain Beaulieu, "Verifying Protocol Conformance Using Software Model Checking for the Model-Driven Development of Embedded Systems", IEEE Transactions on Software Engineering, vol.39, no. 9, pp. 1307-13256, Sept. 2013, doi:10.1109/TSE.2013.14
REFERENCES
[1] G. Hunt and J. Larus, "Singularity: Rethinking the Software Stack," ACM SIGOPS Operating Systems Rev., vol. 41, no. 2, pp. 37-49, 2007.
[2] M. Fähndrich, M. Aiken, C. Hawblitzel, O. Hodson, G. Hunt, J. Larus, and S. Levi, "Language Support for Fast and Reliable Message-Based Communication in Singularity OS," Proc. First ACM SIGOPS/EuroSys European Conf. Computer Systems, pp. 177-190. 2006.
[3] R. Campbell and A. Habermann, "The Specification of Process Synchronization by Path Expressions," Proc. Int'l Symp. Operating Systems, pp. 89-102, 1974.
[4] D. Yellin and R. Strom, "Protocol Specifications and Component Adaptors," ACM Trans. Programming Languages and Systems, vol. 19, no. 2, pp. 292-333, 1997.
[5] G. Leavens, A. Baker, and C. Ruby, "Preliminary Design of JML: A Behavioral Interface Specification Language for Java," SIGSOFT Software Eng. Notes, vol. 31, no. 3, pp. 1-38, 2006.
[6] S. Gay, V. Vasconcelos, and A. Ravara, "Session Types for Inter-Process Communication," http://eprints.kfupm.edu.sa64731/, 2003.
[7] F. Plasil and S. Visnovsky, "Behavior Protocols for Software Components," IEEE Trans. Software Eng., vol. 28, no. 11, pp. 1056-1076, Nov. 2002.
[8] T. Bureš, M. Děcký, P. Hnětynka, J. Kofroň, P. Parízek, F. Plášil, T. Poch, O. Šerý, and P. Tůma, "CoCoME in SOFA," The Common Component Modeling Example, A. Rausch, R. Reussner, R. Mirandola, and F. Plášil, eds., pp. 388-417, Springer-Verlag, 2008.
[9] A. Cansado, D. Caromel, L. Henrio, E. Madelaine, M. Rivera, and E. Salageanu, "A Specification Language for Distributed Components Implemented in GCM/ProActive," The Common Component Modeling Example, A. Rausch, R. Reussner, R. Mirandola, and F. Plášil, eds., pp. 418-448, Springer, 2008.
[10] M. Baldoni, C. Baroglio, A. Martelli, V. Patti, and C. Schifanella, "Verifying Protocol Conformance for Logic-Based Communicating Agents," Proc. Fifth Int'l Conf. Computational Logic in Multi-Agent Systems, pp. 196-212, 2005.
[11] I. Rauf and I. Porres, "Designing Level 3 Behavioral RESTful Web Service Interfaces," SIGAPP Applied Computing Rev., vol. 11, no. 3, pp. 19-31, 2011.
[12] B. Selic, G. Gullekson, and P. Ward, Real-Time Object-Oriented Modeling. Wiley, Apr. 1994.
[13] B. Selic, "Using UML for Modeling Complex Real-Time Systems," Proc. ACM SIGPLAN Workshop Languages, Compilers, and Tools for Embedded Systems, pp. 250-260, 1998.
[14] D. Schmidt, "Model-Driven Engineering," Computer, vol. 39, no. 2, pp. 25-31, Feb. 2006.
[15] B. Selic, "Using UML for Modeling Complex Real-Time Systems," Proc. ACM SIGPLAN Workshop Languages, Compilers, and Tools for Embedded Systems, pp. 250-260, 1998.
[16] E. Gery, D. Harel, and E. Palachi, "Rhapsody: A Complete Life-Cycle Model-Based Development System," Proc. Conf. Integrated Formal Methods, pp. 1-10, 2002.
[17] P. Abdulla, J. Deneux, G. Stalmarck, H. Agren, and O. Akerlund, "Designing Safe, Reliable Systems Using Scade," Proc. First Int'l Conf. Leveraging Applications of Formal Methods, 2004.
[18] T. Weigert et al., "Experiences in Deploying Model-Driven Engineering," Proc. 13th Int'l SDL Forum Conf. Design for Dependable Systems, 2007.
[19] Object Management Group, "UML 2.4 Superstructure Specification," Technical Report, formal/2011-08-05, OMG, 2011.
[20] Object Management Group, "Action Language for Foundational UML (ALF)," Technical Report ptc/2010-10-05, OMG, 2010.
[21] O. Shigo, A. Okawa, and D. Kato, "Constructing Behavioral State Machine Using Interface Protocol Specification," Proc. 13th Asia Pacific Software Eng. Conf., pp. 191-198, 2006.
[22] A. Stengel and T. Bultan, "Analyzing Singularity Channel Contracts," Proc. 18th Int'l Symp. Software Testing and Analysis, 2009.
[23] L. Giordano and A. Martelli, "Verifying Agent Conformance with Protocols: An Automata Based Approach," Proc. Int'l Agents, Logic and Theorem Proving Workshop, pp. 19-31, 2007.
[24] R. Jhala and R. Majumdar, "Software Model Checking," ACM Computing Surveys, vol. 41, no. 4, pp. 1-54, 2009.
[25] W. Visser, K. Havelund, G. Brat, S. Park, and F. Lerda, "Model Checking Programs," Proc. 15th IEEE Int'l Conf. Automated Software Eng., vol. 10, no. 2, pp. 203-232, Apr. 2003.
[26] V. Tran, H. Hashimoto, Y. Tanabe, and M. Hagiya, "Verification of Java Programs under Fairness Assumption," Proc. 25th Conf. Japan Soc. for Software Science and Technology, 2008.
[27] B. Selic, "personal communication," Jan. 2011.
[28] P. Whittaker, M. Goldsmith, K. Macolini, and T. Teitelbaum, "Model Checking UML-RT Protocols," Proc. Workshop Formal Design Techniques for Real-Time UML, Nov. 2000.
[29] Eclipse Foundation "Eclipse Java Emitter Templates (JET)," www.eclipse.org/modelingm2t, 2010.
[30] Y. Moffett, "UML-RT Protocol Conformance Verification Through Exhaustive Exploration—From Theory to Implementation," MSc thesis, Royal Military College of Canada, www.cs.queensu.ca/dingelmoffettMSc.pdf, 2010.
[31] Y. Moffett, A. Beaulieu, and J. Dingel, "Verifying UML-RT Protocol Conformance Using Model Checking," Proc. 14th ACM/IEEE Int'l Conf. Model Driven Eng. Languages and Systems, pp. 410-424, 2011.
[32] A. Cansado, D. Caromel, L. Henrio, E. Madelaine, M. Rivera, and E. Salageanu, "A Specification Language for Distributed Components Implemented in GCM/ProActive," The Common Component Modeling Example, A. Rausch, R. Reussner, R. Mirandola, and F. Plášil, eds., pp. 418-448, Springer, 2008.
[33] P. Pelliccione, P. Inverardi, and H. Muccini, "Charmy: An Extensible Tool for Architectural Analysis," IEEE Trans. Software Eng., vol. 35, no. 3, pp. 325-346, May/June 2009.
[34] R. Allen and D. Garlan, "A Formal Basis for Architectural Connection," ACM Trans. Software Eng. and Methodology, vol. 6, no. 3, pp. 213-249, 1997.
[35] F. Plasil and S. Visnovsky, "Behavior Protocols for Software Components," IEEE Trans. Software Eng., vol. 28, no. 11, pp. 1056-1076, Nov. 2002.
[36] Z. Liu, C. Morisset, and V. Stolz, "RCOS: Theory and Tools for Component-Based Model Driven Development," Proc. Third Int'l Symp. Fundamentals of Software Eng., 2009.
[37] J. Kofron, "Checking Software Component Behavior Using Behavior Protocols and Spin," Proc. ACM Symp. Applied Computing, pp. 1513-1517, 2007.
[38] P. Parizek, F. Plasil, and J. Kofron, "Model Checking of Software Components: Combining Java PathFinder and Behavior Protocol Model Checker," Proc. IEEE/NASA 30th Ann. Software Eng. Workshop, 2006.
[39] G. Engels, J. Küster, R. Heckel, and L. Groenewegen, "A Methodology for Specifying and Analyzing Consistency of Object-Oriented Behavioral Models," Proc. Eighth European Software Eng. Conf. Held Jointly with Ninth ACM SIGSOFT Int'l Symp. Foundations of Software Eng., pp. 186-195. 2001.
[40] G. Engels, J. Küster, R. Heckel, and M. Lohmann, "Model-Based Verification and Validation of Properties," Electronic Notes in Theoretical Computer Science, vol. 82, no. 7, pp. 133-150, 2003.
[41] M. Saaltink, "Using SPIN to Analyse ROOM Models," Technical Report TR-99-5537-02, ORA Canada, 1999.
[42] M. Saaltink and I. Meisels, "Using SPIN to Analyse RoseRT Models," Technical Report TR-99-5537-03, ORA Canada, Oct. 1999.
[43] T. Schäfer, A. Knapp, and S. Merz, "Model Checking UML State Machines and Collaborations," Electronic Notes in Theoretical Computer Science, vol. 55, pp. 1-13, 2004.
[44] H. Giese, M. Tichy, S. Burmester, and S. Flake, "Towards the Compositional Verification of Real-Time UML Designs," Proc. European Software Eng. Conf., pp. 38-47, 2003.
[45] I. Porres and I. Rauf, "From Nondeterministic UML Protocol Statemachines to Class Contracts," Proc. Third Int'l Conf. Software Testing, Verification, and Validation, pp. 107-116, Apr. 2010.
[46] T. Ball, V. Levin, and S. Rajamani, "A Decade of Software Model Checking with Slam," Comm. ACM, vol. 54, no. 7, pp. 68-76, 2011.
[47] L. Giordano and A. Martelli, "Verifying Agent Conformance with Protocols Specified in a Temporal Action Logic," Proc. 10th Congress Artificial Intelligence and Human-Oriented Computing, pp. 145-156, 2007.
6 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool