On testing and conformance relations for UML statechart diagrams behaviours

ABSTRACT

In this paper we study the formal relationship between testing preorder/equivalences for a behavioural subset of UML Statechart Diagrams and a conformance relation for implementations with respect to specifications given using such diagrams. We study the impact of stuttering on the above mentioned relationship. In the context of UMLSDs, stuttering occurs when no transition of the UMLSD is enabled by the current event in the current (global) state of the underlying state-machine. We consider both the case in which the semantics underlying the testing relations does not model stuttering explicitly - we call it the non-stuttering semantics - and the case in which it does it - i.e. the stuttering semantics. We show that in the first case the conformance relation is stronger than the reverse of the MUST preorder and, consequently, stronger than the MAY preorder. Much more interesting results can be proven in the second case, possibly under proper conditions on the sets of events under consideration. In fact the conformance relation is shown to coincide with the MAY preorder, and thus be implied by the reverse MUST preorder. Finally, we show important substitutivity properties which hold in the case of stuttering semantics.

REFERENCES

• 1: Barry S. Bosik , M. Ümit Uyar, Finite state machine based formal methods in protocol conformance testing: from theory to implementation, Computer Networks and ISDN Systems, v.22 n.1, p.7-33, Aug. 1991 [doi>10.1016/0169-7552(91)90079-R]
• 2: R De Nicola, Extensional equivalence for transition systems, Acta Informatica, v.24 n.2, p.211-237, April 1987
• 3: S. Gnesi, D. Latella, and M. Massink. Modular semantics for a UML Statechart Diagrams kernel and its extension to Multicharts and Branching Time Model Checking. The Journal of Logic and Algebraic Programming. Elsevier Science. (To appear).
• 4: S. Gnesi, D. Latella, and M. Massink. Towards formal conformance testing of uml statechart diagrams behaviors. (submitted).
• 5: S. Gnesi, D. Latella, and M. Massink. Formal conformance testing UML Statechart Diagrams Behaviours: From theory to automatic test generation. Technical Report CNUCE-B04-2001-16, Consiglio Nazionale delle Ricerche, Istituto CNUCE, 2001. (Full version).
• 6: Matthew Hennessy, Algebraic theory of processes, MIT Press, Cambridge, MA, 1988
• 7: D. Latella, I. Majzik, and M. Massink. Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker. Formal Aspects of Computing. The International Journal of Formal Methods. Springer, 11(6):637-664, 1999.
• 8: Diego Latella , Istvan Majzik , Mieke Massink, Towards a Formal Operational Semantics of UML Statechart Diagrams, Proceedings of the IFIP TC6/WG6.1 Third International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS), p.465, February 15-18, 1999
• 9: D. Latella and M. Massink. A formal testing framework for UML Statechart Diagrams Behaviours: From theory to automatic verification. Technical Report CNUCE-B4-2001-007, Consiglio Nazionale delle Ricerche, Istituto CNUCE, 2001. (Full version).
• 10: Diego Latella , Mieke Massink, A Formal Testing Framework for UML Statechart Diagrams Behaviours: From Theory to Automatic Verification, The 6th IEEE International Symposium on High-Assurance Systems Engineering: Special Topic: Impact of Networking, p.11-22, October 24-26, 2001
• 11: D. Latella and M. Massink. Relating testing and conformance relations for UML Statechart Diagrams Behaviours. Technical Report CNUCE-B4-2002-001, Consiglio Nazionale delle Ricerche, Istituto CNUCE, 2002. (Full version).
• 12: D. Lee and M. Yannakakis. Principles and Methods of Testing Finite State Machines - A Survey. Proceedings of the IEEE, 84(8):1090-1123, 1996.
• 13: M. Massink. Functional Techniques in Concurrency. PhD thesis, University of Nijmegen, Feb. 1996. ISBN 90-9008940-3.
• 14: Object Management Group, Inc. OMG Unified Modeling Language Specification - version 1.3, 1999.
• 15: Rational Software and Microsoft and Hewlett-Packard and Oracle and Sterling Software and MCI Systemhouse and Unisys and ICON Computing and IntelliCorp and i-Logix and IBM and ObjecTime and Platinum Technology and Ptech and Taskon and Reich Technologies and Softeam. UML Semantics, version 1.1, 1997. UML semantics with metamodel.
• 16: J. Tretmans. A Formal Approach to Conformance Testing. PhD thesis, University of Twente, 1992.
• 17: J. Tretmans. Test generation with inputs, outputs and repetitive quiescence. Software - Concepts and Tools, 17(3):103-120, 1996.
• 18: Jan Tretmans, Testing Concurrent Systems: A Formal Approach, Proceedings of the 10th International Conference on Concurrency Theory, p.46-65, August 24-27, 1999

INDEX TERMS

Primary Classification:
  H. Information Systems
  H.2 DATABASE MANAGEMENT
      H.2.5 Heterogeneous Databases

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

Keywords:
UML statechart diagrams, conformance testing, formal semantics, formal testing theory, testing theory