Retour au site du LAAS-CNRS

Abstract

We describe a formal verification toolchain for AADL, the SAE Architecture Analysis and Design Language, enriched with its behavioral annex. Our approach is based on tools that are integrated in the Topcased environment. We give a high-level view of the tools involved and illustrate the successive transformations that take place during the verification process.

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.

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

Mots-Clés / Keywords