A Translation of UML Components into Formal Specifications
UML demonstrated that it is a well-suited approach to analyse and design complex systems such as industrial ones. To improve software reliability and reusability the use of formal specification is necessary but it may be difficult. There is a general lack in the formal specification of the UML concepts. This decreases the ability to develop tools and guidelines to help the specifier. Software tools are needed to assist the formal specification process, but also to prove or to verify some parts. In this paper we propose a method to formally specify concurrent and communicating components with data in UML. The principle is, first to complete the design with axioms, second to translate the diagrams into algebraic specifications of data types thanks to our translation tool. We describe the translation principles which are based on previous work around symbolic transition systems and algebraic specifications. Finally, we sketch the implementation of our translation tool using XMI files and the XML4J parser.
KeywordsUnify Modelling Language Unify Modelling Language Model State Predicate Abstract Data Type Prototype Verification System
Unable to display preview. Download preview PDF.
- 1.James Rumbaugh, Ivar Jacobson, and Grady Booch. The Unified Modeling Language Reference Manual. Addison-Wesley, 1999.Google Scholar
- 2.Robert France, Andy Evans, and Kevin Lano. The UML as a formal modeling notation. In Haim Kilov, Bernhard Rumpe, and Ian Simmonds, editors, Proceedings OOPSLA′97 Workshop on Object-oriented Behavioral Semantics, pages 75–81. Technische Universität München, TUM-I9737, 1997.Google Scholar
- 3.Andy Evans. Making UML precise. In Luis Andrade, Ana Moreira, Akash Deshpande, and Stuart Kent, editors, Proceedings of the OOPSLA′98 Workshop on Formalizing UML. Why? How?, 1998.Google Scholar
- 4.Pascal Poizat, Christine Choppy, and Jean-Claude Royer. Concurrency and Data Types: a Specification Method. An Example with LOTOS. In J. Fiadero, editor, Recent Trends in Algebraic Development Techniques, Selected Papers of the 13th Workshop on Algebraic Development Techniques, WADT′98, volume 1589 of Lecture Notes in Computer Science, pages 276–291. Springer-Verlag, 1999.Google Scholar
- 5.Jean-Claude Royer. Formal Specification and Temporal Proof Techniques for Mixed Systems. In Proceedings of the 15th IPDPS 2001 Symposium, FMPPTA, San Francisco, USA, 2001. IEEE Computer Society.Google Scholar
- 6.Christine Choppy, Pascal Poizat, and Jean-Claude Royer. Specification of mixed systems in KORRIGAN with the support of a UML-inspired graphical notation. In Heinrich Huss-mann, editor, Fundamental Approaches to Software Engineering. 4th International Conference, FASE 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2–6. 2001 Proceedings, volume 2029 of LNCS, pages 124–139. Springer, 2001.Google Scholar
- 7.Stephan Garland and John Guttag. An overview of LP, the Larch Prover. In Proc. of the 3rd International Conference on Rewriting Techniques and Applications, volume 355 of Lecture Notes in Computer Science. Springer-Verlag, 1989.Google Scholar
- 8.S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In Deepak Kapur, editor, 11th International Conference on Automated Deduction (CADE), volume 607 of Lecture Notes in Artificial Intelligence, pages 748–752. Springer-Verlag, 1992.Google Scholar
- 9.Pascal André, Annya Romanczuk, Jean-Claude Royer, and Aline Vasconcelos. An Algebraic View of UML Class Diagrams. In H. Sahraoui C. Dony, editor, Acte de la conférence LMO′2000, pages 261–276, 2000. ISBN 2-6462-0093-7.Google Scholar
- 10.Pascal André, Annya Romanczuk, Jean-Claude Royer, and Aline Vasconcelos. Checking the Consistency of UML Class Diagrams Using Larch Prover. In T. Clark, editor, Proceedings of the third Rigorous Object-Oriented Methods Workshop, BCS eWics, ISBN: 1-902505-38-7, 2000. http://www.ewic.org.uk/ewic/workshop/view.cfm/ROOM2000.
- 11.Michel Allemand and Jean-Claude Royer. Mixed Formal Specification with PVS. In Proceedings of the 15th IPDPS 2002 Symposium, FMPPTA. IEEE Computer Society, 2002.Google Scholar
- 12.Jean-Claude Royer. Temporal Logic Verifications for UML: the Vending Machine Example. In Proceedings of the fourth Rigorous Object-Oriented Methods Workshop, 2002.Google Scholar
- 13.Kevin Lano and Juan Bicarregui. Semantics and transformations for UML models. In Pierre-Alain Muller and Jean Bézivin, editors, Proceedings of UML′98 International Workshop, Mulhouse, France, June 3–4, 1998, pages 97–106. ESSAIM, Mulhouse, France, 1998.Google Scholar
- 15.E. Astesiano, B.Krieg-Bruckner, and H.-J. Kreowski Eds., editors. Algebraic Foundations of System Specification. IFIP State-of-the-Art Reports. Springer Verlag, 1999. ISBN 3-540-63772-9.Google Scholar
- 16.Martin Wirsing. Algebraic Specification, volume B of Handbook of Theoretical Computer Science, chapter 13, pages 675–788. Elsevier, 1990. J. Van Leeuwen, Editor.Google Scholar
- 17.André Arnold. Finite Transition Systems. International Series in Computer Science. Prentice-Hall, 1994. ISBN 0-13-092990-5.Google Scholar
- 18.Gianna Reggio, Egidio Astesiano, Christine Choppy, and Heinrich Hussmann. Analysing UML active classes and associated state machines — A lightweight formal approach. In Tom Maibaum, editor, Proc. Fundamental Approaches to Software Engineering (FASE 2000), Berlin, Germany, volume 1783 of LNCS. Springer, 2000.Google Scholar
- 19.A. Hamie, J. Howse, and S. Kent. Interpreting the Object Constraint Language. In Proceedings of Asia Pacific Conference in Software Engineering. IEEE Press, January 1998.Google Scholar
- 20.Jean-Claude Royer. An Operational Approach to the Semantics of Classes: Application to Type Checking. Programming and Computer Software, 27(3), 2002. ISSN 0361–7688.Google Scholar
- 21.Bogumila Hnatkowska and Huzar Zbigniew. Extending the UML with a Multicast Synchronisation. In T. Clark, editor, ROOM′2000: third workshop on Rigorous Object-Oriented Methods, BCS eWics, ISBN: 1-902505-38-7, 2000. http: //www.ewic.org.uk/ewic/workshop/view.cfm/ROOM2000.
- 23.Michael J. McLaughlin and Alan Moore. Real-time extensions to UML. Dr. Dobb’s Journal of Software Tools, 23(12):82, 84, 86–93, December 1998.Google Scholar
- 26.IBM. XML4J. Technical report, 1998. http://www.alphaworks.ibm.com/tech/xml4j.
- 27.José Meseguer. Solving the inheritance anomaly in concurrent object-oriented programming. In Oscar Nierstrasz, editor, Proceedings ECOOP′93, LNCS 707, pages 220–246, Kaiserslautern, Germany, July 1993. Springer-Verlag.Google Scholar
- 28.A. M. D. Moreira and R. G. Clark. Combining Object-Oriented Analysis and Formal Description Techniques. In M. Tokoro and R. Pareschi, editors, Proceedings of ECOOP′94, Bologna, Italy, Lecture Notes in Computer Science 821, pages 344–364. Springer-Verlag, Berlin, 1994.Google Scholar
- 30.A. Hamie, J. Howse, and S. Kent. Modular Semantics for Object-Oriented Models. In Proceedings of Northern Formal Methods Workshop, eWics Series. Springer Verlag, August 1998.Google Scholar
- 31.Bran Selic and Jim Rumbaugh. Using UML for Modeling Complex Real-Time Systems. Technical report, Rational Software Corp., 1998.Google Scholar