Relatore : Fabrice KORDON

Co-relazione : HUGUES Jérome

Mise en oeuvre de notations standardisées, formelles et semi-formelles dans un processus de développement de systèmes embarqués temps-réel répartis

Dans un processus 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 est cruciale pour les systèmes temps-réel répartis et embarqués (TR2E), pour s'assurer 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. Il est nécessaire d'adopter une démarche d'Ingénierie Dirigée par les Vérifications et les Validations (IDV2) pour s'assurer que le système est correctement construit, et qu'il satisfait un ensemble de propriétés spécifiées en amont dans le processus de développement. 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 TR2E. Le langage AADL (Architecture Analysis and Design Language) est utilisé comme notation pivot. Le processus proposé prend en compte les aspects comportementaux de l'application et les aspects architecturaux de l'exécutif. Il repose sur des notations standardisées, pour faire face aux problèmes d'interopérabilités des outils mis en oeuvre. 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 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.

Pubblicazioni 2006-2010

• 2010
  • X. Renault, J. Hugues : “Définition d’une famille de patrons de transformation pour l’analyse de modèles AADL”, Génie logiciel : le magazine de l'ingénierie du logiciel et des systèmes, vol. 93, pp. 12-16, (Génie industriel multimédia) (2010)
• 2009
  • X. Renault : “Mise en oeuvre de notations standardisées, formelles et semi-formelles dans un processus de développement de systèmes embarqués temps-réel répartis”, these, difesa 12/03/2009, relatore Kordon, Fabrice, co-relazione : Hugues, Jérome (2009)
  • X. Renault, F. Kordon, J. Hugues : “Adapting models to model checkers, a case study: Analysing AADL using Time or Colored Petri Nets”, Proceedings of the 20^th International Workshop on Rapid System Prototyping, Paris, France, pp. 26-33, (IEEE) (2009)
  • X. Renault, F. Kordon, J. Hugues : “From AADL architectural models to Petri Nets: Checking model viability”, 12^th IEEE International Symposium on Object-oriented Real-time distributed Computing (ISORC'09), Tokyo, Japan, pp. 313-320, (IEEE Computer Society) (2009)
• 2008
  • F. Kordon, J. Hugues, X. Renault : “From Model Driven Engineering to Verification Driven Engineering”, 6^th IFIP Workshop on Software Technologies for Future Embedded & Ubiquitous Systems (SEUS 2008), vol. 5287, Lecture Notes in Computer Science, Capri, Italy, pp. 381-393, (Springer-Verlag) (2008)
  • X. Renault, J. Hugues, F. Kordon : “Formal Modeling of a Generic Middleware to Ensure Invariant Properties”, 10^th Formal Methods for Open Object-based Distributed Systems (FMOODS'08), vol. 5051, Lecture Notes in Computer Science, Oslo, Norway, pp. 185-200, (Springer-Verlag) (2008)
• 2007
  • F. Bonnefoi, L. Hillah, F. Kordon, X. Renault : “Design, Modeling and Analysis of ITS using UML and Petri Nets”, 10^th International IEEE Conference on Intelligent Transportation Systems, Seattle, WA, United States, pp. 314-319, (IEEE) (2007)
• 2006
  • A. Hamez, L. Hillah, F. Kordon, A. Linard, E. Paviot‑Adet, X. Renault, Y. Thierry‑Mieg : “New Features in CPN-AMI 3 : Focusing on the Analysis of Complex Distributed Systems”, 6^th International Conference on Application of Concurrency to System Design (ACSD '06), Turku, Finland, pp. 273-275, (IEEE Computer Society) (2006)