Generating class contracts from UML protocol statemachines

ABSTRACT

We present an approach to generate behavioral class interfaces in the form of class contracts from UML 2.0 protocol state machines. A generated class contract defines a pre- and post-condition for each operation that triggers a transition in the state machine. We consider the following protocol SM elements: state and state invariants, simple transitions, compound transitions, high-level transitions, complete transitions, self transitions also deal with the case of firing priorities. The generated contracts can be used as a behavioral interface, for documentation, run-time checking and test case generation.

References

1. UML Revision Task Force. OMG UML Specification 2.2, 2009. Available at http://www.omg.org/spec/UML/2.2/.
2. Cheon, Y., Automated Random Testing to Detect Specification-Code Inconsistencies. In Proceedings of the 2007 International Conference on Software Engineering Theory and Practice, July 9--12, 2007, Orlando, Florida, U.S.A.
3. Cheon, Y., and Leavens, G. T., The JML and JUnit Way of Unit Testing and its Implementation. Technical Report 04--02, Department of Computer Science, Iowa State University, Ames, IA, February 2004.
4. Leitner, A., Ciupa, I., Manuel, O., Meyer, B., and Fiva. A., Contract driven development = test driven development: writing test cases. In ESEC-FSE 07: Proceedings of the 6th joint meeting of the european software engineering conference and the 14th ACM SIGSOFT symposium on Foundations of software engineering, pages 425434, New York, NY, USA, 2007. ACM Press.
5. Gery, E., Harel, D., and Palatshy, E., Rhapsody: A Complete Lifecycle Model-Based Development System. In Proc. Intl Conf. on Integrated Formal Methods, 2002. pp. 1--10.
6. Ciupa, I., and Leitner, A., Automatic testing based on Design by Contract. In Proceedings of Net.ObjectDays 2005, 6th Annual International Conference on Object-Oriented and Internet-based Technologies, Concepts and Applications for a Networked World (2005) 545--557
7. Snook, C., and Butler, M., UML-B: Formal modelling and design aided by UML. ACM Transactions on Software Engineering and Methodology, 2006. Volume 15, Issue 1 January 2006, Pages: 92--122.
8. Kim, Y., Honh, H., Cho, S., Bae, D., and Cha, S., Test Cases Generation from UML State Diagrams, IEE Proc. Software, vol. 146, no. 4, pp. 187--192, Aug. 1999.
9. Sekerinski, E. and Zurob, R., iState: A statechart translator. In M. Gogolla and C. Kobryn, editors, UML 2001 The Unified Modeling Language, 4th International Conference, Lecture Notes in Computer Science 2185, pages 376390, Toronto, Canada, 2001. Springer-Verlag.
10. Lilius, J. and I. Porres, Formalising UML State Machines for Model Checking, in: R. B. France and B. Rumpe, editors, Proc. 2nd Int. Conf. UML, Lect. Notes Comp. Sci. 1723 (1999), pp. 430445.
11. Knapp, A., Merz, S., and Rauh, C., Model Checking Timed UML State Machines and Collaborations. In Proc. 7th Int. Symp. Formal Techniques in Real-Time and Fault Tolerant Systems, 2002. Volume 2469/2002 Pages, 395--414
12. Briand, L. C., Labiche, Y. and Sun, H. Investigating the Use of Analysis Contracts to Support Fault Isolation in Object Oriented Code. In Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis (ISSTA 02). ACM Press, New York, NY (2002) 70--80
13. Sekerinski, E. 1998. Graphical design of reactive systems. In B98: Recent Advances in the Development and Use of the B Method2nd International B Conference. Montpellier, France, April 1998, D. Bert, Ed. Lecture Notes in Computer Science, Vol. 1393, Springer-Verlag, 182197.
14. Sekerinski, E., Verifying Statecharts with State Invariants, In the Proceedings of the 13th IEEE International Conference on Engineering of Complex Computer Systems, Pages 7--14, 2008
15. Meyer, B., Applying Design by Contract, Computer, Oct. 1992, pp. 40--52.
16. Kansomkeat, S., Rivepiboon, W., Automated-Generating Test Case Using Statechart Diagrams, Proceedings of the Annual Research Conference of the South African Institute of Computer Scientists and Information Technologists on Enablement through Technology, 2003, pp. 296--300
17. Van Der Straeten, R.: Inconsistency Management in Model-driven Engineering. An Approach using Description Logics. PhD thesis, Department of Computer Science, Vrije Universiteit Brussel, Belgium (2005)
18. Benowitz, E., Clark, K., Watney, G., Auto-coding UML statecharts for flight software, In the Proceedings of the 2nd IEEE International Conference on Space Mission Challenges for Information Technology
19. Leavens, G. T., Baker, A. L., and Ruby, C., JML: a Java modeling language. In Formal Underpinnings of Java Workshop, Oct. 1998.
20. Niaz. I. A., Tanaka, J., Mapping Uml Statecharts To Java Code, In Proceedings of IASTED International Conf. on Software Engineering (SE 2004) (2005)
21. Lampinen, J., Interface specification methods for software components, Publications in the Laboratory for Theoretical Computer Science. 2008.
22. Flanagan, C., Leino, K. R. M., Lillibridge, M., Nelson, G., Saxe, J. B., Stata, R., Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, Berlin, Germany, June 17--19, 2002.

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

      • Software defect analysis

        • Software testing and debugging

  • Software notations and tools

    • General programming languages

      • Language types

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Logic

  • Semantics and reasoning

    • Program reasoning

      • Program verification