Early Analysis of Ambient Systems SysML Properties using OMEGA2-IFx

International audience 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...

Full description

Bibliographic Details
Main Authors: Ahmad, Manzoor, Dragomir, Iulia, Bruel, Jean-Michel, Ober, Iulian, Belloir, Nicolas
Other Authors: Laboratoire Informatique de l'Université de Pau et des Pays de l'Adour (LIUPPA), Université de Pau et des Pays de l'Adour (UPPA), Modèles, Architectures, Composants, Agilité et prOcessus (IRIT-MACAO), Institut de recherche en informatique de Toulouse (IRIT), Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université de Toulouse (UT)-Toulouse Mind & Brain Institut (TMBI), Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT)
Format: Conference Object
Language:English
Published: HAL CCSD 2013
Subjects:
Requirements
Formal Verification
Observers
Relax
Simulation
[INFO]Computer Science [cs]
Iceland
Online Access:https://hal.science/hal-01085410
https://hal.science/hal-01085410/document
https://hal.science/hal-01085410/file/belloirSIMULTECH2013.pdf
Description
Summary:International audience 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.

Similar Items