Architecture Languages

Outillage pour la modélisation, la vérification et la génération d'applications temporisées et embarquées

Cet article présente un travail en cours pour mettre en place une chaîne d'outils dédiée à la conception, la vérification et l'exécution de systèmes embarqués temps réel. Ce travail se base sur la méthode MCSE et les modèles qu'elle …

Real-Time Model Checking Support for AADL

We describe a model-checking toolchain for the behavioral verification of AADL models that takes into account the realtime semantics of the language and that is compatible with the AADL Behavioral Annex. We give a high-level view of …

Real-time Extensions for the Fiacre modeling language

We present our ongoing research on the extension of the Fiacre language with real-time constructs and real-time verification patterns. Fiacre is a formal language with support for expressing concurrency and timing constraints; its …

Formal Verification of AADL models with Fiacre and Tina

This paper details works undertaken in the scope of the Spices project concerning the behavioral verification of AADL models. We give a high-level view of the tools involved and describe the successive transformations performed by …

Formal Verification of AADL Specifications in the Topcased Environment

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 …