Retour au site du LAAS-CNRS

Abstract

The realization of critical systems goes through multiple phases of specification, design, integration, validation, and testing. It starts from high-level sketches down to the final product. Model-Based Design has been acknowledged as a good conveyor to capture these steps. Yet, there is no universal solution to represent all activities. Two candidates are the OMG-based SysML to perform high-level modeling tasks, and the SAE AADL to perform lower-level ones, down to the implementation. The paper shares an experience on the seamless use of SysML and the AADL to model, validate/verify and implement a flight management system.

Résumé

Cet article partage une expérience de modélisation de systèmes temps réel s'appuyant sur le langage AVA- TAR dérivé de SysML, l'outil en mode libre TTool et la méthode associée. AVATAR enrichit SysML par son lan- gage TEPE d'expression de propriétés. Sa sémantique formelle, par traduction vers les automates temporisés, autorise les preuves de sûreté et celle obtenue par traduction vers le pi-calcul rend possible les preuves de sécurité. Exé- cutable sur Linux, MacOS et Windows, l'outil en mode libre TTool mise quant à lui sur l'accessibilité aux non spé- cialistes pour offrir un éditeur de diagrammes, un simulateur de modèles, une interface aux outils de vérification formelle UPPAAL et ProVerif, et un générateur de code C Posix. L'article illustre l'approche AVATAR sur une étude de cas pédagogique et recense les projets académiques et industriels qui font appel à TTool.

Abstract

Using UML or SysML models in a verification-centric method requires a property expression language, a formal se- mantics, and a tool. The paper introduces TEPE, a graphi- cal TEmporal Property Expression language based on SysML parametric diagrams. TEPE enriches the expressiveness of other common property languages in particular with the no- tion of physical time and unordered signal reception. TEPE is further instantiated in the AVATAR real-time UML profile. TTool, an open-source toolkit, implements a press-button ap- proach for the formal verification of AVATAR-TEPE proper- ties with UPPAAL. An elevator system serves as example.

Abstract

TURTLE is a real-time UML profile introduced a few years ago to address the analysis, design and deployment of time-constrained systems. The profile has a formal semantics. Further, it is supported by an open source toolkit: TTool. The latter enables formal verification of TURTLE models without specific knowledge of mathematical notations or formal languages. This paper proposes to extend TURTLE to cover the requirement capture phase, to check a model against formally expressed temporal requirements, and to achieve temporal requirement traceability. TURTLE is extended with SysML requirement diagrams. Non-formal and formal requirements are both handled. Timing Requirement Description Diagrams are introduced to formally express temporal requirements. TRDDs are based on UML Timing Diagrams. A Hybrid Power Management Unit of a Hybrid Vehicle serves as example.

Mots-Clés / Keywords

Abstract

The paper discusses an experience in using a realtime UML/SysML profile and a formal verification toolkit to check a secure group communication system against temporal requirements. A generic framework is proposed and specialized for hierarchical groups.