A general framework for formalizing UML with formal languages
- 29 August 2005
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 433-442
- https://doi.org/10.1109/icse.2001.919116
Abstract
Informal and graphical modeling techniques enable developers to construct abstract representations of systems. Object-oriented modeling techniques further facilitate the development process. The Unified Modeling Language (UML), an object-oriented modeling approach, could be broad enough in scope to represent a variety of domains and gain widespread use. Currently, UML comprises several different notations with no formal semantics attached to the individual diagrams. Therefore, it is not possible to apply rigorous automated analysis or to execute a UML model in order to test its behavior: short of writing code and performing exhaustive testing. We introduce a general framework for formalizing a subset of UML diagrams in terms of different formal languages based on a homomorphic mapping between meta models describing UML and the formal language. This framework enables the construction of a consistent set of rules for transforming UML models into specifications in the formal language. The resulting specifications derived from UML diagrams enable either execution through simulation or analysis through model checking, using existing tools. This paper describes the use of this framework for formalisms UML to model and analyze embedded systems. A prototype system for generating the formal specifications and results from an industrial case study are also described.Keywords
This publication has 12 references indexed in Scilit:
- UML-based analysis of embedded systems using a mapping to VHDLPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Integrating architecture description languages with a standard design methodPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Towards a formalization of UML class structures in ZPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Towards a Formal Operational Semantics of UML Statechart DiagramsPublished by Springer Nature ,1999
- The model checker SPINIEEE Transactions on Software Engineering, 1997
- A formal semantics for object model diagramsIEEE Transactions on Software Engineering, 1995
- Institutions: abstract model theory for specification and programmingJournal of the ACM, 1992
- Statecharts: a visual formalism for complex systemsScience of Computer Programming, 1987
- Communicating sequential processesCommunications of the ACM, 1978
- Guarded commands, nondeterminacy and formal derivation of programsCommunications of the ACM, 1975