Synthèse de la discussion

Safemodel est un projet/thème dont l'objectif général vise à promouvoir des méthodes de conceptions capables d'appréhender la complexité des systèmes logiciels critiques afin d'augmenter/prouver leur fiabilité tout en facilitant le travail des concepteurs et des autorités d'homologation. Il a émergé de projets comme TUCS et SAFECODE qui visaient à établir des processus de développement de logiciels pouvant être certifiés :

• TUCS du réseau RT3: Elaboration d'un processus de développement «UML outillé» couvrant les phases de spécification - vérification - implantation - certification.
• SAFECODE projet ANR : élaboration d'un processus de conception permettant l'expression des exigences de sûreté de fonctionnement (SdF) et leur traçabilité tout au long du développement orienté vers une implantation par composants.

Le domaine fait appel à quelques concepts importants:

• Vérification : le système a été modélisé/réalisé correctement conformément aux exigences.
• Validation : le bon système a été développé selon un processus de développement approprié.
• Certification : le système est reconnu par un organisme indépendant externe conforme aux exigences spécifiées.
• Qualification : le système a été développé à l'aide d'outils «certifiés».
• Homologation : le système est certifié conforme à une norme, ou une réglementation.

Lorsqu'il s'agit de certification, un examen des normes et recommandations s'impose ; cependant, selon le contexte des applications à développer, les attitudes sont différentes.

• Dans le cadre du monde ferroviaire, il n'est pas recommandé de faire appel à des processus de développement faisant appel à des technologies orientés Objet et Modèle.
• Dans le cadre de l'aéronautique, les processus de développement orientés Modèle se pratiquent depuis le Concorde! Les développements utilisent un grand nombre de DSL spécifiques associés à leurs générateurs de code. L'expérience a montré que les tests unitaires n'ont jamais montré de bogues dans un code généré. Les principaux problèmes portent sur la modélisation et le raffinement des exigences.

Les questions que les participants se sont posées peuvent se formuler comme suit :

• Qu’est-ce qu’un processus IDM vérifié, validé, certifiable ?
• Qu’est-ce qu’un modèle vérifié, validé, certifiable ?
• Doit-on absolument vérifier/valider une transformation ?
• Que signifie une préoccupation de type «SafeModel» selon le contexte d'application (automobile, aéronautique, ferroviaire, énergie, monétique, ...) ?


Akram Idani, Yves Ledru et Pierre-Yves Schobbens – Laboratoire d'Informatique de Grenoble, Université de Namur – PDF

Les auteurs proposent de s'appuyer sur le formalisme et les outils de la méthode B pour construire des systèmes corrects par construction dans une approche d'ingénierie dirigée par les modèles. Etant donné que les outils de description des langages de modélisation (MOF et OCL) sont issus d'UML, les auteurs proposent de partir des travaux réalisés autour du passage d'UML à B. Il s'agit d'une approche par plongement profond (deep embedding) qui consiste à interpréter tous les concepts de l'IDM sous la forme de données en B et de fonctions exploitant ces données (de la même manière qu'un interpréte exploite une représentation sous la forme de données des programmes).


Julien Mallet et Siegfried Rouvrais – 
Télécom Bretagne, Institut Télécom – PDF

L'article propose une approche intéressante pour adapter le processus IDM au cas des logiciels critiques. Il part du fait qu'un logiciel est obtenu par un processus d'ingénierie dirigée par les modèles réalisant une succession de transformations de modèles. Dans ce cadre, il est nécessaire de vérifier que les propriétés fonctionnelles mais aussi non fonctionnelles sont respectées par les modèles obtenus.

Les auteurs tentent de mettre en place une méthode permettant, au plus tôt dans le processus de raffinement, de tenir compte de ces exigences. Dans le raffinement deux phases sont prévues, une pour la détermination d'un style d'architecture et une pour le respect de toutes les propriétés attendues. Dans la seconde phase les transformations sont guidées par des propriétés décrites en une logique du premier ordre étendue. Les propriétés prises en compte sont : la sécurité-innocuité, la confidentialité et le découplage temporel. L'utilisation de cette logique dans le processus de raffinement tente d'être décrite.


Mourad Kmimech, Mohamed Tahar Bhiri, Mohamed Graiet et Philipe Aniorté
 – IUT de Bayonne, Faculté des Sciences de Sfax, ISMIM-Monastir, LIUPPA – PDF

Les auteurs s’intéressent à la formalisation du modèle de composant UML 2.0 avec Acme afin de vérifier l’assemblage de composants. Ils partent du constat que les règles de cohérence d’assemblage de composants en UML2.0 exprimé avec OCL et les travaux existants pour la cohérence des diagrammes de structures composites ne sont pas supportés par les ateliers. Ils proposent donc d’utiliser le langage de description d’architecture Acme et son langage de prédicat Armani. Le typage et le langage de contrainte d’Acme leur permettent de définir un méta-modèle des composants UML2.0 et d’exprimer les règles de cohérences pour la vérification des propriétés structurelles. Un petit exemple montre l’assemblage de deux composants.

Suivant le secteur (ferroviaire, aérien, automobile, sous-traitants équipementiers, avec des variations nationales), les contraintes réglementaires, les cultures et les processus varient considérablement.

L'intégration naturelle des technologies IDM dans les contextes de développements critiques exige leur adéquation avec les contextes réglementaires/normatifs associés. En effet, ces technologies ne sauraient être acceptées par les industriels qu'à la condition qu'elles ne fassent pas obstacle à l'étape fondamentale et ultime que constitue l'autorisation de mise en service du système (généralement donnée par des autorités indépendantes).

Les propositions IDM doivent donc simultanément proposer des outils / méthodes pour une plus grande efficacité du processus de développement (leur objectif premier) mais également (ne pas oublier d') exhiber les artefacts propres à convaincre les autorités que ces nouvelles démarches sont au moins aussi fiables que les précédentes.

Selon les domaines concernés, ces artefacts peuvent varier mais on notera des constantes : la maîtrise totale du processus de développement doit être explicitée à tout instant :

• les divers outils-supports utilisés doivent avoir été eux-mêmes développés selon un cadre aussi rigoureux que le système critique en cours de développement ;
• la traçabilité entre les différents documents de spécification et de réalisation doit être préservée et facilement explicitée.

Le processus de développement et la définition de points de contrôle des différentes phases sont au centre de toutes les approches de validation des logiciels critiques. A l'heure actuelle, les recherches en IDM sont principalement centrées sur des modalités de transformation entre des modèles déjà assez élaborés, sans attention suffisante à leur cohérence propre. Si on veut amener cette approche dans le champ des logiciels critiques, des recherches dans trois domaines doivent être amplifiées :

• élicitation et traçabilité des exigences tout au long du cycle de vie ;
• prise en compte des contraintes de sécurité et de sûreté à travers les contrôles statiques et dynamiques sur les modèles ;
• exploitation, comme pour les composants matériels, des tests et contrôles embarqués dans les composants exécutables (approches de type Behavioral Driven Design et Built-in Test).

Le secteur des logiciels critiques a une très grande habitude d'utiliser des modèles et des transformations de modèles mais en restant au niveau des instances (pas de meta-modèles) et avec une terminologie souvent différente. De même, les normes qui contrôlent la validation des codes critiques imposent des processus de développement très structurés et contrôlés.

Si l'IDM veut s'imposer dans ce domaine, elle doit prendre en compte ces contraintes. Même en dehors du secteur critique, les développements IDM ont la contrainte d'avoir des modèles corrects. La validation et la vérification des modèles et des transformations associées sont des domaines d'étude pour lesquels on commence à avoir des résultats sur certains aspects, comme le test sur les transformations de modèles, la vérification/validation de modèles écrits en UML/OCL.

UML est très foisonnant et présente des imprécisions sémantiques qui conduisent à de vraies difficultés en matière de validation. Les approches DSL séduisent largement le milieu mais imposent des coûts d'investissement initiaux qui font reculer beaucoup d'industriels.

En fait il semble bien qu'il est nécessaire d'aborder les deux niveaux :

• une approche générale sur une vue d'ensemble du processus avec support de la traçabilité ;
• le recours à tout type de modèles (pas seulement modelware, tout type de modèle formel ou mathématique peut convenir) les mieux adaptés pour l'amélioration de chaque étape.

L'essence de l'IDM est d'introduire la modélisation le plus en amont possible dans le cycle de développement. L'utilisation de DSL supportant des langages naturels contraints manipulables directement par des experts du métier semble une voie intéressante pour améliorer l'élicitation des exigences.

Pour les logiciels critiques, il semble bien que la traçabilité des exigences tout au long du développement et de la validation soit la colonne vertébrale du processus de développement. La traçabilité (idéalement bidirectionnelle !) est indispensable, elle est l'indicateur principal de la maîtrise de la complexité du système.

Il semble important que les propositions IDM intègrent une traçabilité plus explicite avec les normes en vigueur pour convaincre les utilisateurs industriels. Il découlerait probablement de cette orientation que les normes elles-mêmes deviennent à terme objets de modélisations et de raisonnements (mise en évidence de points communs entre les différents domaines concernés, en corollaire, des points spécifiques,...)

Une étude sur les techniques de traçabilité a été réalisée dans le cadre du projet ModelPlex (http://www.modelplex.org).

E. Brottier, F. Fleurey, J. Steel, B. Baudry, Y. Le Traon. Metamodel-based Test Generation for Model Transformations: an Algorithm and a Tool, in: Proceedings of ISSRE'06, Raleigh, NC, USA, November 2006.

Audrey Occello, Anne-Marie Dery-Pinna and Michel Riveill. Validation and Verification of an UML/OCL Model with USE and B: Case Study and Lessons Learnt. MoDeVVA 2008 Model Driven Engineering, Verification, and Validation: Integrating Verification and Validation in MDE Lillehammer, Norway, 9-11 April 2008.

Dhaussy P, Auvray J, De Belloy S, Boniol F et Landel E. Un langage de contexte de preuve pour la validation formelle de modèles logiciels. conférences LMO’08 et CAL’08. Montréal, CA. Mars 2008.

MODELPLEX(MODELling solution for comPLEX software systems) Workpackage 3: Model Engineering, Deliverable D3.2.a: Traceability techniques, 02/2008.