Retour au site du LAAS-CNRS

Résumé

OpenEmbeDD est une plate-forme générique, reposant sur les technologies d'Ingénierie Dirigée par les Modèles (IDM), et intégrant des outils d'aide à la conception d'applications temps réel embarqué (TR/E). Les technologies d'IDM utilisées dans OpenEmbeDD sont basées sur l'environnement Eclipse. Elles fournissent une solution simple et efficace pour l'intégration d'outils TR/E sur la plateforme (par la réalisation d'un modeleur) et l'interopération de ses outils (par transformation de modèle). OpenEmbeDD peut être instanciée à un domaine d'application précis en sélectionnant, parmi l'ensemble des outils disponibles, ceux qui répondent à un cas d'utilisation particulier. La plate-forme OpenEmbeDD s'installe en quelques clics. Elle fournit alors une solution d'IDM complète pour mettre en oeuvre rapidement un modeleur et l'intégrer facilement à une suite d'outils. Pour cela, OpenEmbeDD repose sur le format EMF/Ecore afin de faciliter la manipulation de modèles, intègre le générateur d'éditeurs graphiques Topcased, le langage de transformation ATL, l'environnement de méta-modélisation Kermeta, l'éditeur de profils Papyrus. Sa conformité aux standards industriels les plus répandus est un avantage important. OpenEmbeDD intègre un modeleur UML complet accompagné de la mise en oeuvre de référence du profil temps-réel MARTE. OpenEmbeDD inclus également d'autres standards comme AADL, SysML ou SDL. La plate-forme OpenEmbeDD permet donc de complémenter la modélisation d'applications utilisant des profils UML standards avec toute la souplesse et la spécificité d'outils métier d'aide à la conception pour le TR/E, et ce à moindre coût de développement.

Abstract

Model Checking is a formal technique for the verification of finite systems. However, it is well known that this technique suffers from the state explosion problem. We describe work in progress to implement in the TINA toolbox an enumerative variant of a state based observation graph algorithm defined by Klai and Poitrenaud.

Mots-Clés / Keywords

Model checking; Système temps réel ; Langage dédié à un domaine;

Abstract

More and more, models, through Domain Specific Languages (DSL), tend to be the solution to define complex systems. Expressing properties specific to these metamodels, and checking them, appear as an urgent need. Until now, the only complete industrial solutions that are available consider structural properties such as the ones that could be expressed in OCL. There are although some attempts on behavioural properties for DSL. This paper addresses a method to specify and then check temporal properties over models. The case study is SimplePDL, a process metamodel. We propose a way to use a temporal extension of OCL, TOCL, to express properties. We specify a models transformation to Petri Nets and LTL formulae for both the process model and its associated temporal properties. We check these properties using a model checker and enrich the model with the analysis results. This work is a first step towards a generic framework to specify and effectively check temporal properties over arbitrary models.

Mots-Clés / Keywords

Metamodelling; Properties validation; Verification; Temporal OCL; Process Model; Petri nets; LTL; Models Semantics; Model Transformation;

Abstract

Ladder Diagram (LD) is the most used programming language for Programmable Logical Controllers (PLCs). A PLC is a special purpose industrial computer used to automate industrial processes. Bugs in LD programs are very costly and sometimes are even a threat to human safety. We propose a model driven approach for formal verification of LD programs through model-checking. We provide a metamodel for a subset of the LD language. We define a time Petri net (TPN) semantics for LD programs through an ATL model transformation. Finally, we automatically generate behavioral properties over the LD models as LTL formulae which are then checked over the generated TPN using the model-checkers available in the Tina toolkit. We focus on race condition detection. This work is supported by the topcased project, part of the french cluster Aerospace Valley (granted by the french DGE), cf. http://www.topcased.org