Model-based techniques for the future integration for formal verification of critical real-time software systems

Robati, Tiyam (2016). Model-based techniques for the future integration for formal verification of critical real-time software systems. Thèse de doctorat électronique, Montréal, École de technologie supérieure.

Prévisualisation	PDF Télécharger (1MB) | Prévisualisation
Prévisualisation	PDF Télécharger (456kB) | Prévisualisation

Résumé

Integrated modular avionics architectures combined with the emerging SAE TTEthernet standard provides a strong infrastructure for the deployment of mixed-critical avionic applications that meet stringent safety, reliability and performance requirements. Integrating these systems is a complex and challenging engineering task. Of paramount importance is the development of a model-based approach that can endow system engineers with a methodology and supporting tools to cope with this complexity. In this thesis, we present an extension of AADL, the standard language used for architecture and analysis modeling, in order to enable the modeling of integrated multi-critical avionic applications deployed on TTEthernet-based IMA architectures. To do this, we first present a metamodel for the TTEthernet domain followed by an extension of the core AADL metamodel with concepts and constraints relevant for this domain. In doing so, we define the concrete textual syntax for this extension, and we outline the implementation of this extension using the Open Source AADL Tool Environment (OSATE). To verify the AADL model for TTEthernet, we build on our extension of AADL and leverage model transformations to assess the system models produced with this methodology. In this process, we transform the system models to a target model that is compatible with DEVS formalism in its dedicated simulation environment.

We illustrate the proposed approach using a case study provided by Bombardier, our industrial partner in this project, and we show the benefits of our AADL extension and verification approach to the contention-freedom property of the TTEthernet schedule.

Titre traduit

Techniques basées sur un modèle pour l'intégration et la vérification formelle de systèmes logiciels critiques en temps réel

Résumé traduit

Les architectures avioniques modulaires intégrées combinées avec la norme SAE TTEthernet constituent une infrastructure solide pour le déploiement des applications avioniques a criticités mixtes ayant des exigences strictes en termes de sécurité, fiabilité et de performance. L’intégration de tels systèmes est une tâche d’ingénierie complexe et difficile. Par conséquent, l’approche basée sur les modèles qui offre aux ingénieurs systèmes une méthodologie et les outils de support pour maitriser cette complexité, est d’une grande importance. Dans cette thèse, nous présentons une extension pour le langage de modélisation AADL pour supporter la modélisation des applications avioniques à criticités mixtes déployées sur des architectures IMA basées sur TTEthernet. En particulier, nous présentons un méta-modèle qui étend le métamodèle de base de AADL avec les concepts et les contraintes de ce domaine. Nous définissons une syntaxe textuelle concrète pour cette extension ainsi que l’implémentation de cette extension en utilisant l’outil OSATE. Par la suite, on construit par-dessus notre extension du langage AADL et nous utilisons les transformations de modèles pour supporter la vérification des modèles de systèmes produits avec cette méthodologie. En particulier, nous proposons une transformation des modèles de systèmes en modèles convenables à la simulation avec DEVs. Finalement, nous illustrons l’approche proposée via une étude de cas fournies par Bombardier, notre partenaire industriel dans le projet. Nous utilisons cette étude de cas pour démontrer notre extension et procéder à la vérification de la contrainte contention-freedom d’un ordonnancement TTEthernet.

Type de document:	Mémoire ou thèse (Thèse de doctorat électronique)
Renseignements supplémentaires:	"Thesis presented to École de technologie supérieure in partial fulfillment of the requirements for the degree of doctor of philosophy". Bibliographie : pages 79-85.
Mots-clés libres:	Avionique numérisée. Ingénierie dirigée par les modèles. Logiciels Vérification. AADL (Informatique) Ethernet (Système de réseau local) Temps réel (Informatique) Traitement réparti. critique, système, TTEthernet, IMA, ARINC 653, AFDX, DEVS
Directeur de mémoire/thèse:	Directeur de mémoire/thèse Gherbi, Abdelouahed
Programme:	Doctorat en génie > Génie
Date de dépôt:	10 févr. 2017 19:50
Dernière modification:	10 févr. 2017 19:50
URI:	https://espace.etsmtl.ca/id/eprint/1809

Gestion Actions (Identification requise)

Dernière vérification avant le dépôt