Les méthodes d’ingénierie formelles sont théoriquement capables d’atteindre un niveau de qualité « zéro bug ». Certaines sont utilisées avec succès en industrie, notamment dans le développement de systèmes de métro automatique. Le projet DEPLOY réalise de telles mise en oeuvre dans plusieurs domaine industriel. Dans ce cadre, le CETIC s’attache à la collecte d’observations afin de les diffuser à destination de toute entreprise intéressée par ces méthodes.
La mission du projet DEPLOY consiste à réaliser des avancées majeures en matière de méthodes d’ingénierie utilisées pour développer des systèmes critiques en déployant des méthodes formelles, et les outils les supportant.
Ce projet DEPLOY est entièrement dirigé selon les besoins industriels et est basé sur le déploiement industriel dans quatre secteurs majeurs de l’industrie européenne : l’automobile, les transports, l’espace et le secteur IT.
Le projet sera un succès si les méthodes formelles proposées et leurs outils associés sont effectivement transférés durablement au sein de ces industries.
Les partenaires industriels sont eux-mêmes intéressés par ces observations, de manière à pouvoir poser une décision éclairée quant à l’utilisation des méthodes formelles, et pour pouvoir éventuellement convaincre la hiérarchie.
L’objectif du projet est de produire des documents permettant à toute compagnie intéressée par l’utilisation de méthodes formelles de prendre une décision éclairée sur l’opportunité d’utiliser ces méthodes, ainsi que la meilleure manière de les déployer.
Ces documents regroupent un faisceau d’indicateurs montrant les avantages, limitations et difficultés liées à ces méthodes formelles sur base des expériences industrielles en cours.
Pour attirer l’attention d’une audience industrielle, les résultats clefs de DEPLOY sont structurés dans une foire aux questions (FAQ) permettant de répondre à toutes les questions importantes que se poserait un industriel désirant déployer des méthodes formelles.
Cette FAQ est organisée par rôle (manager, responsable qualité, ingénieur de développement, etc) et couvre les interrogations spécifiques à chacun de ces rôles.
La FAQ couvre les thèmes suivants :
impact sur l’organisation en matière de ressource et de formation,
impact sur la qualité des produits développés en utilisant des méthodes formelles,
possibilité d’exploiter des modèles formels à diverses étapes du processus de développement,
possibilité de réutiliser des modèles formels et des preuves d’un développement à l’autre,
possibilité de fractionner l’apprentissage d’une méthode formelle au sein d’une organisation, et éventuellement de sélectionner un sous-ensemble d’employés pour acquérir une expertise en méthodes formelles.
possibilité de procéder à une migration par étapes à un processus utilisant des méthodes formelles.
forces et faiblesses des outils ainsi que la qualité du support et des fournisseurs de l’outil.
facteurs externes (compétiteurs, organismes régulateurs, etc) qui poussent ou réfrènent l’adoption des méthodes formelles.
Pour chaque thème, les points de vue suivants sont examinés, de manière à couvrir le thème exhaustivement :
Managers de haut niveau : les managers des départements de production ou de R&D doivent prendre des décisions stratégiques pour l’entreprise et quantifier l’impact financier de l’utilisation de nouvelles méthodes et techniques. De plus ce rôle inclut les managers de produits et de lignes de produits, qui ont un impact sur l’aspect commercial des produits.
Chefs de la qualité et de projets : gèrent directement les ingénieurs, analystes et responsables qualité. Ils doivent s’assurer de la faisabilité des projets et ils gèrent directement le personnel travaillant sur les projets de développement de systèmes. Ils ne peuvent normalement pas effectuer de travail technique, mais ont souvent besoin d’avoir une bonne compréhension des méthodes et outils utilisés par leurs équipes, de manière à pouvoir estimer la faisabilité d’un projet et de décider des allocations de personnel sur les projets, des formations, et de l’adaptation des procédures d’assurance qualité.
Ingénieurs et analystes : ce sont les gens qui travaillent directement sur les projets de développement de systèmes. Ils vont appliquer les méthodes d’ingénierie sélectionnées et les outils associés.
Praticiens de la qualité : ils effectuent des tâches de l’assurance qualité telles que la revue de documents, la vérification de traçabilité, l’intégration et le test système. En général, les praticiens de la qualité n’ont pas besoin d’appliquer les méthodes formelles, mais ils doivent les comprendre parce que les produits qu’ils vérifient utilisent des notations formelles.
Les quatre rôles définis ci-dessus couvrent un large panel avec des besoins divers. Identifier les questions d’intérêt pour ces quatre rôles sur les thèmes présentés ci-dessus nous permet de manière sûre de couvrir tous les aspects importants lies à l’impact du déploiement des méthodes formelles dans la société.
La manière naturelle de structurer cette information est une FAQ divisée en pages Web. Cette technologie fournit les mécanismes appropriés pour structurer l’information selon les différentes dimensions : thèmes, rôles et secteurs industriels. Un exemple de question/réponse est présenté ci-dessous. En plus du schéma question/réponse, le thème et le rôle associés à la question sont aussi mentionnés.
En plus de l’approche orientée question, il est intéressant de présenter des histoires complètes reprenant des succès ou des échecs significatifs, en examinant en détail les différents aspects intervenant dans ces histoires. Cela permet de montrer en détail les bénéfices que le monde industriel peut tirer de ces méthodes formelles. Les échecs sont eux aussi repris dans cette section, de manière à pouvoir éviter de reproduire des situations similaires. Nous avons identifié les success stories suivantes :
Utilisation de modèles de spécification pour préparer une formalisation (Bosch)
Augmentation de la capacité à modéliser et prouver des systèmes spatiaux complexes (SSF)
Utilisation de techniques de model-checking pour remplacer une vérification manuelle coûteuse en temps (Siemens)
Utilisation d’une notation spécifique au domaine pour cacher une méthode formelle et favoriser son adoption (SAP)
Génération automatique de jeux de test (SAP)
Risques et bénéfices lies à l’utilisation d’outils formels open source (Systerel)
Transfert technologique et formation nécessaire pour atteindre l’autonomie dans l’application des méthodes formelles (ETHZ)
Les « success stories » rapportées ne sont pas restreintes aux contributions internes du projet. Elles sont consolidées avec des expériences similaires rapportées par la littérature par des groupes d’intérêt et par des événements de dissémination.
La FAQ développée sera publiée on-line sous la forme d’un wiki interactif durant l’année 2011. L’URL du wiki public sera annoncée dans une future newsletter et sur le site du projet DEPLOY. Quelques rapports publics sont d’ores et déjà disponibles sur : http://www.deploy-project.eu/pdf/d7-revised-final.pdf
EDIT - le site est : http://www.fm4industry.org
Les méthodes formelles sont relativement peu utilisées en Wallonie, les industriels préférant en général utiliser des techniques d’ingénierie traditionnelles basées sur des phases d’analyse amont peu formalisée (documents textuels, UML) et avec des coûts avals importants au niveau des phases de tests. Ce choix est tout à fait justifié pour la plupart des systèmes où l’impact de bogues est peu important (indisponibilité du système, perte mineure d’information…) mais montrent leurs limites pour des projets ayant des dimensions critiques au niveau de la sécurité de fonctionnement (mise en danger de personnes, par exemple dans des systèmes de transport) ou de la sécurité des données (ex. cartes ou transactions bancaires).
Grâce à DEPLOY, le CETIC renforce activement son expertise sur les techniques et outils formels. Le CETIC acquiert aussi une expérience précieuse sur les méthodes d’introduction en milieu industriel afin de déterminer le périmètre adéquat, mettre en œuvre les changements et s’assurer d’un retour optimal. Pour citer quelques expériences, le CETIC a déjà :
Exploré des techniques de robustification logicielles permettant de rendre des systèmes critiques robustes par rapport à des pannes du matériel sous-jacent et d’économiser les coûteux matériels de redondances matérielles, une expérience qui s’est avérée concluante.
Développé un prototype complet de chaîne de test basé sur des modèles formels dans un contexte bancaire. Les outils se sont avérés encore trop peu puissants pour un usage industriel.
Assuré des formations en milieu industriel relativement à l’introduction à ce type de méthodes.
Si vous êtes intéressé par ce type d’approche, n’hésitez pas à nous contacter (christophe.ponsard@cetic.be). Le CETIC peut vous apporter son aide pour mettre en œuvre les méthodes formelles, que ce soit sur un projet particulier, ou pour les implanter durablement au sein d’un processus de production. En outre, le projet DEPLOY dispose de mécanismes permettant aux entreprises de disposer de conseils d’experts internationaux en la matière !
Christophe PONSARD, Jean-Christophe DEPREZ et Renaud DE LANDTSHEER
| Thème | Exploitation des méthodes formelles à diverses étapes du processus de développement |
| Rôles | Ingénieurs et Analystes, Praticiens de la Qualité |
| Question | Est-il possible de tirer avantage d’une méthode formelle au-delà de la simple utilisation pour garantir certaines propriétés d’un système, par exemple pour automatiser certains développements et tâches |
| Réponse | Siemens Transport est entrain d’étudier la manière dont les ingénieurs peuvent générer des analyses de type FMEA/AMDEC ainsi qu’une partie de la documentation du système à partir de modèles Event-B. Une intégration de la chaîne d’outils Event-B avec une chaîne d’outil formels en place est aussi à l’étude. SAP a montré comment les ingénieurs pouvaient aider les praticiens de la qualité en générant des cas de tests d’intégration pour tester des processus business. Des modèles formels ont été développés pour prouver certaines propriétés des processus business et générer des jeux de tests d’intégration. Certains des jeux de tests générés n’avaient pas été identifiés pas les praticiens de la qualité. |