Formal methods provide tools to verify the consistency and correctness of a specification with respect to the desired properties of the system. This verification is important as the development of an AAL (Ambient Assisted Living) system involves different technologies (medical services, surveillance cameras, intelligent devices, etc.) requiring a strong consistency checking between models. We illustrate in this paper how we prove some of the properties of the system before the development even starts. To model the AAL system, we use the SysML language. In terms of tools, we used Rational Rhapsody in combination with the OMEGA2 profile which is an executable Uml/SysML profile used for the formal specification and validation of critical real-time systems. This profile is supported by the IFx toolset which provides mechanisms for the model simulation and properties verification of the AAL system.

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.

We describe an approach to support UML-based development of embedded systems by formal techniques. A subset of UML is extended with timing annotations and given a formal semantics. UML models are translated, via XMI, to the input format of formal tools, to allow timed and non-timed model checking and interactive theorem proving. Moreover, the Play-Engine tool is used to execute and analyze requirements by means of live sequence charts. We apply the approach to a part of an industrial case study, the MARS system, and report about the experiences, results and conclusions.