OMEGA2: A New Version of the Profile and the Tools

In previous work we contributed to the definition of an executable profile of UML, called OMEGA UML, dedicated to the formal specification and validation of real-time systems. The prominent features of OMEGA UML are (1) a small and coherent set of concepts for describing the architecture and the behaviour of a system, (2) means for formalizing the properties of the system, in particular timing properties, and (3) a well-behaved concurrent execution model suited for real-time applications. To meet user demands, the profile has recently been updated to include hierarchical composite structures (part of the standard UML 2. x specification) and new concurrency structures. The new version (OMEGA2) is in line with the original principles: simplicity, well-defined operational semantics and tool support for simulation and verification (IFx version 2). The present paper contains an overview of both the profile and the tool.