Dans une démarche classique d'ingénierie dirigée par les modèles (IDM), l'ingénieur modélise son système à l'aide d'une notation semi-formelle, le valide puis l'implante. L'étape de validation, basée sur ces modèles, est particulièrement cruciale pour les systèmes temps-réel répartis et embarqués (TR2E), afin de s'assurer de leur respect d'invariants de sécurité, ou de leur bon fonctionnement logique ou temporel. Cependant, une démarche IDM n'est pas suffisante car elle n'indique pas comment utiliser les modèles pour faire des analyses. Quels modèles (ou vues) utiliser ? Pour analyser quel type de propriétés ? Ainsi, il est nécessaire d'adopter une démarche d'Ingénierie dirigée par les Vérifications et les Validations (IDV2) : les modèles créés sont ceux qui sont utiles pour s'assurer que le système est correctement construit (vérification), et qu'il satisfait un ensemble de propriétés spécifiées en amont dans le processus de développement (validation). Cette thèse propose un processus de développement, de validation et de vérification basé sur des notations formelles, et dédié aux applications temps-réel réparties embarquées. Nous nous appuyons sur une notation pivot standard pour appliquer cette démarche IDV2 : le langage AADL (Architecture Analysis and Design Language) permet à l'ingénieur de spécifier son application TR2E depuis son architecture matérielle jusqu'à son déploiement logiciel. Il repose sur l'existence d'un exécutif ayant certaines propriétés et proposant différents services. Ce processus prend en compte les aspects comportementaux de l'application ainsi que les aspects architecturaux de l'exécutif. Il repose sur des notations standardisées, permettant de faire face aux problèmes d'interopérabilités des outils mis en oeuvre. Pour l'applicatif, des propriétés comme l'absence d'interblocage, l'utilisation et le dimensionnement de ressources ou encore l'ordonnancement du système sont validées. Pour l'exécutif, le fait que l'architecture de celui-ci et les services proposés sont en adéquation avec les propriétés évoquées lors de sa configuration est vérifié. Notre démarche permet d'obtenir des retours aussi bien à propos de l'applicatif que de l'exécutif, et permet de corriger ou modifier les modèles dans un processus de développement itératif. Au cours de notre démarche, nous exploitons et transformons les spécifications AADL vers différentes notations standardisées : les réseaux de Petri pour la validation de l'applicatif, la notation Z pour la vérification de l'exécutif utilisé, PolyORB.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00577646 |
| Date | 03 December 2009 |
| Creators | Renault, Xavier |
| Publisher | Université Pierre et Marie Curie - Paris VI |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0018 seconds