Modélisation formelle pour l’ingénierie système. La sûreté d’un drone comme illustration des enjeux d’une conception formalisée

24/12/2017
OAI : oai:www.see.asso.fr:1301:2017-5:21290
DOI : http://dx.doi.org/10.23723/1301:2017-5/21290You do not have permission to access embedded form.
contenu protégé  Document accessible sous conditions - vous devez vous connecter ou vous enregistrer pour accéder à ou acquérir ce document.
Prix : 10,00 € TVA 20,0% comprise (8,33 € hors TVA) - Accès libre pour les ayants-droit
 

Résumé

Modélisation formelle pour l’ingénierie système. La sûreté d’un drone comme illustration des enjeux d’une conception formalisée

Métriques

1
0
403.1 Ko
 application/pdf
bitcache://a862c574bdbe00d7f4716bb769e7b070137f97b6

Licence

Creative Commons Aucune (Tous droits réservés)
<resource  xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
                xmlns="http://datacite.org/schema/kernel-4"
                xsi:schemaLocation="http://datacite.org/schema/kernel-4 http://schema.datacite.org/meta/kernel-4/metadata.xsd">
        <identifier identifierType="DOI">10.23723/1301:2017-5/21290</identifier><creators><creator><creatorName>Sophie Coudert</creatorName></creator><creator><creatorName>Dominique Legros</creatorName></creator></creators><titles>
            <title>Modélisation formelle pour l’ingénierie système. La sûreté d’un drone comme illustration des enjeux d’une conception formalisée</title></titles>
        <publisher>SEE</publisher>
        <publicationYear>2017</publicationYear>
        <resourceType resourceTypeGeneral="Text">Text</resourceType><dates>
	    <date dateType="Created">Sun 24 Dec 2017</date>
	    <date dateType="Updated">Mon 29 Jan 2018</date>
            <date dateType="Submitted">Sat 17 Feb 2018</date>
	</dates>
        <alternateIdentifiers>
	    <alternateIdentifier alternateIdentifierType="bitstream">a862c574bdbe00d7f4716bb769e7b070137f97b6</alternateIdentifier>
	</alternateIdentifiers>
        <formats>
	    <format>application/pdf</format>
	</formats>
	<version>35772</version>
        <descriptions>
            <description descriptionType="Abstract"></description>
        </descriptions>
    </resource>
.

URSI DOSSIER 2 76 ZREE N°5/2017 Modélisation formelle pour l’ingénierie système Conception formelle pour la sûreté d’un drone Sophie Coudert1 , Dominique Legros2 Institut Mines-Telecom – Telecom ParisTech1 , ENGIE INEO UTS2 Introduction Les méthodologies basées sur le cycle de vie – ou les méthodes d’analyses semi-formelles telles que SADT, SA- RT, UML – permettent d’appréhender plus facilement et plus complètement l’analyse et la résolution d’un problème. Cependant elles restent focalisées sur le comment de la pro- duction logicielle et le lien avec le niveau applicatif est peu encadré. Les méthodes formelles, quant à elles, répondent à la fois au quoi et au comment en reliant spécifications abstraites et programmes par des règles mathématiques. Ces approches se basent sur la logique [9,10,11] qui offre une approche scientifique du raisonnement et de ses règles en s’appuyant sur des langages formels. Ces langages per- mettent d’écrire des descriptions précises, non ambiguës, support essentiel pour l’analyse et le raisonnement rigoureux. La logique définit mathématiquement l’interprétation du lan- gage et caractérise le raisonnement fondé comme utilisant des règles dont on a prouvé qu’elles ne permettent que des déductions vraies pour cette interprétation. Le raisonnement valide devient alors une question de forme, contrôlable par la machine et parfois automatisable. Utilisant ces atouts, les méthodes formelles sont souvent accompagnées d’un outil- lage puissant pour assister les processus de conception et de vérification. Elles permettent de prouver des propriétés du système, d’identifier des conditions d’assemblage sûr, de ga- rantir le lien entre l’application et l’implémentation, etc. Elles offrent aussi des techniques complémentaires telles que le prototypage ou la simulation rapide. Elles apportent ainsi des garanties fortes bien identifiées et évitent bien des erreurs humaines. Cependant, utiliser ces approches induit un effort de modélisation et demande une certaine expertise. Elles sont restées longtemps réservées au traitement de problèmes particuliers soumis à des objectifs très élevés de fiabilité ou de sécurité (nucléaire, militaire, spatial, etc.). Mais La com- plexité croissante des systèmes modernes demande plus de rigueur dans le processus de conception. Les approches for- melles y contribuent et l’expérience montre que l’investisse- ment en amont du processus induit des économies en aval. Face à la complexité, elles proposent des techniques pour décomposer et structurer les problèmes tout en gardant la maîtrise des propriétés du système. Aujourd’hui, leur champ d’application est en pleine extension et les travaux récents y associent des méthodologies accompagnatrices. Using formal methods in development process forces to be rigorous and requires some new efforts with respect to previous approaches. But it leads to a better command of system complexity so that investing in the use of such techniques at the beginning of a design process allows savings at the end. Recent trends in formal methods and the development of associated methodo- logies make these approaches more and more suitable for industrial use. This paper presents the main ideas un- derlying formal modeling: what it is about, what it brings in term of reliability of systems, what the difficulties are and how recent trends can assist to overcome them. The purpose is illustrated with a pedagogical example. It pro- vides the reader with a brief overview of technical aspects and supports a discussion on methodological aspects. Then state of the art, current issues and perspectives are more broadly discussed before concluding. ABSTRACT L'utilisation de méthodes formelles dans le processus de développement impose des contraintes rigoureuses et nécessite de nouveaux efforts par rapport aux approches antérieures. Mais cela conduit à une meilleure maîtrise de la complexité du système et investir dans l'utilisation de telles techniques au début d'un processus de conception permet des économies à la fin. Les tendances récentes dans les méthodes formelles et le développement de méthodologies associées rendent ces approches de plus en plus adaptées à un usage industriel. Cet article présente les principales idées qui sous-tendent la modélisation formelle : de quoi il s'agit, ce qu'elle ap- porte en termes de fiabilité des systèmes, quelles sont les difficultés et comment les tendances récentes peuvent aider à les surmonter. Le tout est illustré avec un exemple pédagogique. Il fournit au lecteur un bref aperçu des as- pects techniques et vient en support d’une discussion sur les aspects méthodologiques. Ensuite, l'état de l'art, les questions actuelles et les perspectives sont plus largement discutées avant de conclure. RÉSUMÉ REE N°5/2017 Z 77 Modélisation formelle pour l’ingénierie système Cet article montre les enjeux liés à la mise en œuvre des méthodes formelles dans la pratique des bureaux d’étude. Après un aperçu général de la modélisation et des garanties associées en section 1, l’exemple pédagogique d’un drone illustre en section 2 les aspects méthodologiques qui sont ensuite discutés plus largement avant de conclure. Modélisation et garanties mathématiques La modélisation pour une exploitation méthodique doit s’inscrire dans un cadre précis, suivre des principes. C’est ce qui constitue le méta-modèle, présenté dans la première partie de cette section. Les deux suivantes présentent la mo- délisation formelle, ses bases et sa structuration. Modélisation et méta-modèle Le processus de modélisation est souvent confondu avec celui de l’analyse. L’analyse consiste en la décomposition d’un système en éléments plus faciles à appréhender, alors que la modélisation vise à décrire une abstraction de ce sys- tème à travers des représentations conceptuelles simplifiées permettant de le comprendre et de le simuler par exemple. L’action de modéliser n’est pas neutre et façonne la repré- sentation du système observé. Un modèle est avant tout une représentation intellectuelle puis ensuite symbolique d’un monde observé. La démarche de modélisation relève de deux opérations : la conceptualisation et la représentation. La conceptualisation permet de dégager une représen- tation du monde réel sous une forme logique générale, le méta-modèle, qui est l’ensemble des concepts de base pour modéliser (syntaxe, sémantique…) et des règles qui régissent leur utilisation. Le contenu d’un modèle dépend, lui, du phé- nomène observé. On attend du méta-modèle un gain dans l’abstraction du système, grâce à un jeu de concepts géné- riques qui facilite l’identification d'éléments constitutifs du système et la description de ses comportements. Un méta-modèle prend en compte deux problématiques : la compréhension du réel et la robustesse du modèle de représentation. Il doit respecter les objectifs suivants : sla lisibilité des concepts. Ils doivent être intellectuellement et mathématiquement manipulables ; sla fiabilité du formalisme retenu. La conceptualisation va définir un cadre de travail sur lequel va être projeté le sys- tème observé. Il est donc nécessaire que les mécanismes mis en œuvre soient fiables et que la confiance dans les résultats produits soit forte ; s la neutralité de la représentation. La méthodologie et le formalisme proposés ont pour objectif de pouvoir conduire des analyses pendant toute la démarche de modélisation puis d’exploitation du modèle. Si ces activités relèvent du domaine de l’expertise, le cadre descriptif doit faciliter des représentations non biaisées. Les approches formelles sont des approches modélisa- trices dont les méta-modèles s’appuient sur la logique ma- thématique, permettant des démonstrations rigoureuses et contrôlables par ordinateur. Base logique, raisonnement et vérification formels La sûreté du raisonnement formel tient au fait qu’il utilise des règles préalablement prouvées : pour pouvoir utiliser une règle « P ⵫ Q » permettant de déduire une propriété Q d’une propriété P, il faut avoir montré (mathématiquement) que P est vraie à chaque fois que Q l’est, en s’appuyant sur la définition rigoureuse de l’interprétation des propriétés. Par exemple une règle telle que « x = y/2 ⵫ y = 2.x » pourra être prouvée (et donc utilisée) pour une sémantique qui interprète les divers symboles (x,y,2,/,.) dans les réels ou les rationnels, mais pas pour une sémantique dans des entiers. Cette règle est dédiée au raisonnement sur des nombres. Un ensemble de règles dédié au raisonnement sur une classe de propriétés est appelé un système formel. Le ma- thématicien démontre les règles. L’ordinateur les utilise pour superviser ou automatiser les preuves. La logique fournit des systèmes adaptés pour des rai- sonnements généraux [1]. Par exemple la règle « P, P=>Q ⵫ Q » dit que, si d’une part P est vrai, et d’autre part quand P est vrai Q l’est aussi, alors on peut en déduire que Q est vrai. Une application de cette règle pourrait être « Père(a,b) & Père(b,c) , Père(a,b) & Père(b,c) => GrandPère(a,c) & GrandPère(a,c) ». P,Q, =>, &,= et ⵫ sont les symboles du mé- ta-modèle, sur lesquels se basent les règles générales de rai- sonnement. Père, GrandPère, etc. sont symboles propres au système modélisé et respectent une forme imposée par le méta-modèle : ici par exemple on a un prédicat à deux places « Père(_,_) » interprété en sémantique ensembliste par une relation binaire. Dans cet exemple, les propriétés spécifiques au domaine peuvent être des axiomes (écrits dans la spécifi- cation), comme « Père(x,y) & Père(y,z) => GrandPère(x,z) ») ou des théorèmes (espérés, puis démontrés en utilisant les règles à partir des axiomes), comme « GrandPère(a,c) »). Quand la sémantique est définie sous forme de machines à états finis (automate), on dispose d’une technique com- plémentaire pour prouver automatiquement qu’une proprié- té est vérifiée. Cette technique, dite “model-checking” [2], repose fondamentalement sur des algorithmes de parcours d’états. Cette méthode est avantageuse car de nombreux systèmes peuvent être modélisés par des automates repré- sentant l’évolution de leur état dans le temps. URSI DOSSIER 2 78 ZREE N°5/2017 Les méta-modèles formels offrent divers services : cer- tain se prêtent à la description de propriétés fonctionnelles, d’autres aux propriétés temporelles, par exemple. Les mé- ta-modèles contraints (finitude, propriétés restreintes, etc.) offrent plus d’automatisation et d’efficacité des outils. Les méta-modèles souples sont souvent plus expressifs, mais les exploiter requiert plus de contribution humaine. Pour faciliter l’utilisation des méta-modèles fondamentaux (techniques, logiques), les méthodologies outillées y superposent des couches spécialisées pour des domaines particuliers, offrant des interfaces plus intuitives, avec des représentations gra- phiques par exemple. Les environnements de conception associés aident à la mise en œuvre conjointe de l’expertise du domaine et de celle du méta-modèle. Aussi utiliser des formalismes logiques n’entrave plus vraiment le gain que représente la rigueur mathématique dès les spécifications de plus haut niveau. Les difficultés viennent surtout de la complexité des sys- tèmes qui se répercutent sur les modèles : accroissement du nombre d’états, du nombre de formules, du nombre de preuves, etc. Pour faire face, les méthodes formelles ont développé des techniques complémentaires, en particulier en termes d’abstraction et de structuration. Structurer en préservant les garanties La complexité s’accroît encore si l’on aborde des systèmes plus hétérogènes que le strict logiciel, avec la variété des environnements physiques, logiques ou technologiques. Le modélisateur risque alors de perdre la maîtrise de la re- présentation abstraite, submergé par une information trop abondante. Aussi, plutôt que de travailler sur des modèles détaillés, on utilise des modèles partiels, plus simples : des composants du système complet, des aspects ou des ni- veaux de détails. La difficulté est reportée vers le contrôle des relations entre ces parties pour une structuration maîtrisée. On distingue souvent deux axes de structuration : l’axe hori- zontal des composants et l’axe vertical des niveaux de détails. La structure horizontale (figure 1) combine des parties d’un système qui peuvent être développées séparément, avec leur propre cycle de développement. Ainsi les déve- loppeurs se concentrent sur des problèmes bien délimités sans considérer l’ensemble. Malheureusement une combi- naison horizontale sûre est difficile, de mauvaises interac- tions peuvent apparaître et les propriétés prouvées sur les composants peuvent être perdues au niveau du système. Par exemple, une ressource peut être suffisante pour un composant mais pas pour deux fonctionnant simultanément. Figure 1 : Méthodologie avec assistance formelle. REE N°5/2017 Z 79 Modélisation formelle pour l’ingénierie système Les outils formels permettent d’identifier les compositions incertaines mais ne suppriment pas le problème intrinsèque. Néanmoins, cet axe de structuration est incontournable, no- tamment pour l’utilisation de composants préexistants. La difficulté est moindre dans le cas de composants fortement indépendants, de composants sans sous-état partagé ou de propriétés fortement locales. Structurer verticalement (figure 2) consiste à relier des modèles abstraits et des modèles détaillés d’un même sys- tème. En ne conservant au niveau abstrait que les informa- tions pertinentes pour la propriété que l’on veut établir, on obtient des modèles plus simples et on réduit la complexité des processus de validation. Il faut alors s'assurer que les résultats obtenus restent valables sur les modèles concrets. Les approches formelles apportent cette garantie par une ca- ractérisation mathématique des contraintes à respecter pour que les propriétés prouvées soient préservées au niveau concret. On s’appuie pour cela sur une relation maîtrisée entre les niveaux, concernant les modèles et les propriétés, souvent reformulées. Des outils permettent d’assurer le res- pect de ces contraintes. Méthodologiquement, on utilise cette préservation de deux façons. Abstraire consiste à retirer de l’information d’un modèle détaillé, par exemple pour vérifier a posteriori les propriétés d’un système existant. Raffiner consiste à partir d’un modèle abstrait et à ajouter des choix de réalisation, comme lors d’un processus de conception. Les méthodes formelles apportent ainsi des méta-mo- dèles pour la structuration, permettant de relier de façon sûre les composants ou les niveaux de représentation. Pour assu- rer concrètement cette sûreté, on dispose d’outils reposant sur des bases mathématiques prouvées et les recherches visent à optimiser les simplifications pour augmenter la maî- trise de la complexité. Plus généralement, elles visent une structuration adaptée à la preuve, qui peut constituer un bon support pour des méthodologies de mise au point de systèmes sûrs. L’exemple et la discussion qui suivent montrent que leur mise en œuvre mène à un examen rigoureux des problèmes. Exemple de conception avec une méthode formelle Nous illustrons ici la mise en œuvre d’une méthode for- melle par un exemple simplifié. Il s’appuie sur la méthode « Event-B » [3], généralisation pour la modélisation système de la « méthode B » (utilisée pour le logiciel dans le domaine Figure 2 : Structuration horizontale. Figure 3 : Structuration verticale. URSI DOSSIER 2 80 ZREE N°5/2017 du ferroviaire). Après une présentation rapide de la méthode, nous montrons une spécification abstraite de suivi d’un raffi- nement, puis discutons quelques aspects méthodologiques. Event B : un méta-modèle formel pour la modélisation système L’approche « Event-B » permet la modélisation et l’analyse de comportement de systèmes réactifs, c’est-à-dire réagis- sant à des stimuli. On y prouve des propriétés de sûreté, mais surtout, on passe de modèles abstraits à des modèles concrets par un raffinement rigoureux qui permet d’exprimer la sûreté au niveau applicatif et de la garantir au niveau de l’implémentation. Les spécifications décrivent des machines à états. Les états sont caractérisés par des variables. On change d’état par des événements, caractérisés par les conditions dans lesquelles ils peuvent survenir (les gardes) et les modifications qu’ils apportent à l’état (les substitutions). Les systèmes décrits sont discrets et non continus. Une machine se voit associer des invariants : des propriétés de sûreté dont on doit prouver qu’elles sont vraies dans tous les états. Les outils génèrent une liste de preuves mathématiques à apporter pour garantir les invariants d’une machine et automatisent partiellement ces preuves. On a une forte puissance d’expression pour les propriétés de sûreté car le langage logique disponible pour cela est riche (théorie naïve des ensembles). Le point fort de cette méthode est son processus de raf- finement prouvé, pendant lequel on précise parallèlement l’état et les événements. Une porte à franchir peut devenir une porte munie d’une poignée et d’une serrure. L’ouvrir peut alors devenir la déverrouiller, actionner la poignée puis tirer la porte. Les propriétés sont raffinées en fonction des propriétés de sûreté visées : si l’on s’intéresse au simple franchissement de la porte, on la considérera comme ouverte, abstraitement, quand elle a été concrètement tirée. Si c’est la sécurité antivol qui nous intéresse, on préférera sans doute assimiler l’ouver- ture au déverrouillage. Le raffinement prend donc en compte simultanément le système et les propriétés visées. La relation entre les états abstraits et concrets est exprimée par une pro- priété. Les événements abstraits sont interprétés par certains des événements concrets : selon l’objectif l’ouverture de la porte est son mouvement ou son déverrouillage. Techniquement, pour préserver les propriétés abstraites, il faut respecter quelques contraintes. Les nouveaux événe- ments (actionner la poignée par exemple) ne doivent agir que sur les nouvelles parties de l’état (la poignée qui n’exis- tait pas au niveau abstrait). Les événements hérités de l’abs- trait (ouvrir la porte) ne peuvent être que plus contraints (par exemple on n’ouvrira que sur autorisation). Ainsi on n’ajoute pas de nouveaux comportements sur la partie héritée de l’abstrait et comme les propriétés abstraites avaient été prou- vées pour tout comportement abstrait, elles restent vraies. Ces contraintes sont fortes mais elles apportent une bonne structuration pour des preuves modulaires (on ne reprouve pas ce qui l’a déjà été) et permettent ainsi une approche per- formante en matière de garanties. L’efficacité repose beau- coup sur l’expertise de celui qui spécifie et la mise en œuvre de la méthode gagne à s’articuler avec un complément mé- thodologique comme l’illustre l’exemple qui suit. Spécification abstraite d’un drone très simple Pour illustrer la transition des exigences système de haut niveau vers la mise en œuvre de systèmes de bas niveau, c’est-à-dire la transition des propriétés à respecter vers une solution technique fiable, nous avons choisi le drone. Si l’in- térêt du drone n’est pas à démontrer [4,5], l’utilisation de celui-ci est cependant limitée par le risque qu’il fait courir à son environnement. Il est donc important d’assurer que le comportement du drone est conforme à un comportement attendu. Pour des raisons de clarté nous nous limitons ici à une fonction simple de réaction face à un obstacle situé sur une trajectoire linéaire, situation illustrée sur la figure 3. Figure 4 : Problème initial. REE N°5/2017 Z 81 Modélisation formelle pour l’ingénierie système Le comportement à prouver concerne le déplacement du drone sur sa trajectoire qu’on caractérise par l’événement « move ». La spécification abstraite consiste donc à définir et caractériser la propriété de sûreté du mouvement ; il appa- raît ici de façon évidente que cette propriété est que l’on doit veiller à ce que la distance à l’obstacle soit toujours (invariant) positive. Nous venons en quelques mots de modéliser le pro- blème (figure 4) avec un fort niveau d’abstraction de la réalité. Techniquement, la machine abstraite de haut niveau ne contient que les données minimales suffisantes pour décrire le comportement attendu. La position du drone est assimilée à sa distance à l’obstacle « DIST », sans se préoccuper des vo- lumes des deux objets. L’accident a lieu si la distance sort du positif. À ce niveau, nous autorisons tout mouvement (décrit par “move”) qui ne cause pas de collision, ainsi, le déplace- ment consiste à passer à une nouvelle position respectant l’invariant. Sur cette spécification, considérant une distance initiale positive, montrer que l’invariant est préservé est trivial, direct et les outils le font d’ailleurs automatiquement. Le côté « simplissime » de cette machine n’est pas uni- quement dû à la simplification « pédagogique » de l’exemple et des notations Event-B. La simplicité est une qualité essen- tielle d’un bon modèle abstrait : s LESDONNÏESSONTCELLESDUPROBLÒME LEiQUOIwLEXIGENCE est décrite sans aucune considération des éléments et des solutions techniques envisagés. DIST, par exemple, repré- sente la distance réelle et non une quelconque donnée mémorisée dans quelque composant du drone. Elles ne parlent que de ce qui intéresse la propriété visée : l’absence d’accident. Pour cela, les autres contraintes sur le déplace- ment du drone ne sont pas utiles ; s CETTEDESCRIPTIONSIMPLEESTTRÒSFACILEÌVALIDERMÐMEPAR un néophyte de Event-B. Pour le technicien de la méthode formelle, les preuves sont simples, voire triviales. Une fois exprimée la propriété, ce qui est le rôle de cette première machine, on va mettre au point un système qui la respecte (de façon prouvée) par raffinements successifs. Le paragraphe suivant illustre le début de ce processus. Une première étape de raffinement Les raffinements vont permettre d’une part de préciser le déplacement réel et d’autre part d’introduire les variables techniques du système. Cette démarche va nous obliger à nous intéresser aux conditions qui définissent ce déplace- ment. Nous quittons alors l’abstraction du phénomène pour intégrer des caractéristiques propres au déplacement d’un drone : le processus de modélisation passe de la machine abstraite à une première machine concrète (figure 5). Le déplacement est déterminé par le vent et les moteurs. Un choix de modélisation fait à ce niveau : les événements « move » qui discrétisent le modèle se produisent à inter- valle régulier, ce qui devra être affiné dans un raffinement ultérieur (non présenté ici). Cela permet d’effectuer les cal- culs sur les valeurs de vitesse, plutôt que sur les distances parcourues (relation résultant de la dérivation partielle de la trajectoire du drone par le délai entre chaque occurrence v = bx/bt). La vitesse « Speed », choisie par le drone, a le statut de variable d’état, tandis que le vent « W », donnée externe est une variable locale aléatoire de l’événement (introduite par le mot-clé « some ») qui représente le vent moyen depuis la dernière occurrence de « move ». Ainsi, par raffinement, le « for some D where D>0 do DIST @ D » de l’événement « move » devrait devenir quelque chose ressemblant à « for some wind W do DIST @ DIST-(Speed+W) ». Une telle caractérisation du mouvement n’exclut pas l’acci- dent, et de fait, elle ne passe pas l’épreuve du raffinement prouvé. Face à une proposition de raffinement, les outils associés à Event-B génèrent des obligations de preuve et, ici, ils exigent que l’on prouve que « DIST_(Speed+W) » consti- tue bien « some D where D>0 » ce qui, étant potentielle- ment faux, n’est pas prouvable mathématiquement. Il faut donc ajouter des contraintes et précisions. L’approche formel- le oblige à exhiber de façon rigoureuse les conditions sous lesquelles le système offre les garanties requises. On considère alors comme condition un vent maximal « MaxWind » tel que la vitesse du moteur peut le contrer Figure 5. Machine abstraite. Figure 6 : Premier raffinement. URSI DOSSIER 2 82 ZREE N°5/2017 (MaxSpeed > MaxWind), et le système ne sera garanti que pour un vent dans cette limite. « Speed » est déterminée par le drone, ce qui est modélisé par un nouvel événement « Speed ». Pour cela le drone s’appuie sur la distance qu’il détecte, d’où l’autre nouvel événement : « detect ». Enfin, il faut que ces événement se produisent cycliquement d’où l’introduction d’une variable de séquencement « step », utilisé dans les gardes (conditions pour qu’un événement puisse se produire). On obtient la machine de la figure 5, où l’opérateur « || » exprime le parallélisme entre deux opérations sur les variables. Les contraintes assurant que la distance reste positive sont essentiellement celles encadrées en continu. Encadrés en pointillé, l’invariant exprime que la vitesse du drone est limitée et la contrainte de l’événement « speed » assure que le drone respecte cette limite. En outre, le drone s’appuie non pas directement sur la distance réelle (il n’est pas om- niscient), mais sur une distance détectée. Afin de pouvoir prouver que « DIST-(Speed+W) >0» il faut que la distance détectée soit bien la bonne, ce qui est vrai par la définition de l’événement « detect ». Ainsi on peut prouver que la nou- velle machine constitue bien un raffinement formel de la machine abstraite : les événements sont bien une réalisation du comportement abstrait et les propriétés sont préservées. Suivent ensuite d’autres raffinements pour arriver au système détaillé. Considérations méthodologiques sur l’exemple Pour apporter tout son potentiel de garantie, le processus de modélisation/raffinement doit s’articuler avec un travail de confrontation méthodique du modèle avec la réalité modé- lisée et éviter ainsi les divergences non maîtrisées. Cette ap- proche formelle offre un bon support pour mettre en œuvre une méthodologie accompagnatrice. L’exemple permet d’en donner un aperçu. Au fur et à mesure du processus apparaissent de nou- veaux éléments (variables, événements, propriétés). Il est important de valider tous les éléments introduits dans le mo- dèle. Des outils peuvent guider cette validation en s’appuyant sur une classification des éléments selon leur lieu d’appari- tion, leur statut (propriété, variable d’état, variable locale, va- riable du réel, variable du système, etc.) et selon le fait qu’ils sont raffinés ou non, car seul ce qui n’est pas raffiné doit être garanti par l’extérieur. La méthodologie peut alors déci- der d’actions complémentaires de validation. Par exemple les bornes imposées au vent sont à mettre dans les condi- tions d’utilisation du système. La précision du capteur de distance pourra être garantie par son fournisseur. La vitesse « MaxSpeed » pourra être prouvée par raffinement quand on introduira la puissance du moteur, et cette puissance mise dans un cahier des charges, etc. Raffiner incrémentalement par des pas de taille raisonnable fait que si les vérifications sont potentiellement nombreuses, chacune d’entre elles est souvent relativement simple et présentable à un non expert, éventuellement reformulée en langage naturel. L’approche permet une bonne décomposition du problème global en sous-problèmes avec un inventaire méthodique et rigoureux des hypothèses à valider par le réel. Il est possible d’inter- rompre le développement formel (ne pas raffiner plus) en un point pour déléguer une garantie à une autre approche (contrat fournisseur, par exemple). Il reste cependant des points délicats à surveiller pour une modélisation pertinente. Par exemple (figure 6), l’uti- lisation de la distance détectée comme représentant exact de la distance réelle suppose implicitement que le drone ne s’est pas déplacé entre la détection et l’utilisation de la valeur détectée. Si c’est une erreur de modélisation, les garanties prouvées ne s’appliquent pas au système réel. Plus proba- blement, on détectera le problème en raffinant, quand on introduira la mesure du temps. On évitera alors l’erreur mais il faudra reprendre le travail de modélisation en amont, par exemple en introduisant une distance tampon dont on prou- vera ensuite en raffinant qu’elle est suffisante. Cette reprise peut être coûteuse. Ne pas prendre en considération ce déplacement peut également être un choix si on le consi- dère comme négligeable au regard des autres grandeurs traitées. On choisit alors délibérément un modèle inexact, par approximation (figure 7) et garantir la pertinence de ce modèle relève alors de la seule responsabilité de celui qui fait ce choix. Ceci illustre qu’il est essentiel de bien vérifier la frontière entre modèle et réel. Pour ces points délicats des solutions-type émergent avec l’expérience et le traite- ment des approximations ou autres subtilités de ce type peut devenir méthodique. Notons enfin que des travaux récents apportent des outils pour la modélisation du continu et son articulation avec les modèles discrets [6]. Bien que la mise en œuvre de telles techniques commence à peine, il existe déjà des approches s’appuyant dessus, dites « hybrides » [7]. Enfin notons que la simplicité des modèles étant essen- tielle à la mise en œuvre, il est très opportun de séparer les problèmes. Par exemple on pourra considérer que le modèle du drone ne vaut que pour les vitesses de vents Figure 7 : Approximation. REE N°5/2017 Z 83 Modélisation formelle pour l’ingénierie système limites autorisés tout en permettant au drone réel d’explorer des zones où il y a risque de dépassement. Notre spécifica- tion sera alors une composante d’une spécification plus large dont une autre partie précisera le comportement au-delà des limites. Selon une approche de sécurité, ce comportement pourrait être d’atterrir immédiatement. Aussi, si la modélisation formelle demande une certaine expertise pour minimiser la complexité de la vérification, elle rend accessibles aux non spécialistes beaucoup d’informa- tions pour peu qu’un bon outillage aide à lever l’obstacle du langage logique avec lequel peu d’ingénieurs sont familia- risés. Il faut aussi noter que ce langage logique reste très accessible si l’on se restreint à des formules simples. Discussion et conclusion Face à la complexité croissante des systèmes, la modéli- sation formelle présente de nombreux intérêts pour les acti- vités de conception, validation et vérification, en particulier en termes de rigueur et de sûreté. Cet article en a donné un aperçu, illustré par un exemple basé sur la méthode Event-B qui a l’avantage d’offrir un processus de raffinement formel complet. Elle n’est qu’une des méthodes disponibles. Beaucoup d’environnements de conception outillés existent, basés sur ce type d’approche. Ils proposent non seulement des solutions de preuve, mais aussi des outils de validation complémentaires tels que la simulation rapide, le prototy- page, la génération de tests, etc. L’expérience montre qu’à elle seule, la description rigoureuse et non ambiguë des exi- gences de haut niveau améliorent fortement le développe- ment en réduisant dès le début les risques d’erreur. L’effort de modélisation, effectué tôt dans le développement, est souvent compensé par une économie en aval : moins de tests, moins d’erreurs tardivement détectées, etc. Comme la discipline est assez récente, de nombreux tra- vaux sur ce sujet sont encore académiques et les outils ne sont pas toujours faciles à utiliser. Peu d’ingénieurs en acti- vité sont familiarisés avec ces méthodes, or l’expertise est nécessaire à leur bonne mise en œuvre ; même avec des approches de type « presse-bouton » (comme en offre le model-checking par exemple), l’écriture des modèles a un fort impact sur l’efficacité des outils. Une expertise du do- maine d’application est également indispensable pour assu- rer l’adéquation du modèle à la réalité. Tous ces aspects font que les méthodes formelles sont longtemps restées réser- vées au génie logiciel. Cependant, la situation évolue et la portée de ces méthodes s’étend. Beaucoup d’outils facilitent l’appréhension des mo- dèles. Par exemple, il existe des traducteurs de modèles B en langage « pseudo-naturel ». Il y a des présentations graphiques de spécifications. Les chercheurs de la marine américaine ont récemment développé un simulateur 3D pour les modèles formels afin de travailler sur les drones [8]. Certaines organisa- tions intègrent désormais des équipes formelles dans leur per- sonnel ; pour exemple la RATP qui a une longue expérience avec la méthode B – logiciel. L’intégration de ces approches dans les processus de conception hérités et le savoir-faire de l’ingénierie actuelle se fait progressivement. Introduire de la rigueur non seulement dans le dévelop- pement des composants mais aussi dans le processus de conception lui-même est nécessaire. Cela contribue à aug- menter la maîtrise globale du système. La mise en œuvre d’une approche formelle permet l’identification méthodique des conditions et hypothèses sous lesquelles le système est garanti. Avec Event-B, c’est le processus de raffinement lui- même qui est formalisé. Cela montre l’intérêt de modéliser non seulement les systèmes mais aussi les processus. Une telle démarche ouvre la porte à un outillage qui non seu- lement peut faciliter la conception mais permet aussi d’en articuler les différentes phases et donc potentiellement d’étendre le raisonnement rigoureux à une perception plus globale du système. Une méthodologie à base formalisée n’implique pas une formalisation complète. Chaque tâche (de validation par exemple) y joue un rôle clairement identifié et sa réa- lisation résulte d’un choix, compromis entre les techniques possibles, leur coût, le temps à y consacrer et le niveau de fiabilité attendu. Intégrer une description précise des acteurs et de leurs rôles est également utile. Enfin, organiser les in- formations issues du processus de conception au sein d’un outil permet de mémoriser la réflexion intellectuelle qui a structuré le développement et peut être très utile par la suite lors de la rédaction de la documentation ou pour de la réuti- lisation, par exemple. Pour conclure, les méthodes formelles constituent un ap- port important pour le développement de systèmes fiables. Si leur caractère récent et le peu d’expertise disponible en la matière font que leur intégration dans les processus in- dustriels reste encore modeste, il est néanmoins déjà bien réel. Le développement de méthodologies spécialisées qui s’appuient sur ces approches est une piste prometteuse pour augmenter la maîtrise des systèmes complexes et faciliter leur développement. De nombreuses recherches actuelles portent sur ce sujet. Références [1] S. Jacobs and V. Kuncak, Towards Complete Reasoning about Axiomatic Specifications, pp. 278–293. Berlin, Heidelberg: Springer Berlin Heidelberg, 2011. URSI DOSSIER 2 84 ZREE N°5/2017 [2] E. M. Clarke, Jr., O. Grumberg, and D. A. Peled, Model Checking. Cambridge, USA: MIT Press, 1999. [3] J.-R. Abrial, Modeling in Event-B: System and Software Engineering. New York, NY, USA: Cambridge University Press, 1st ed., 2010. [4] T. J. Tanzi and F. Lefeuvre, “The Contribution Of Radio Sciences to Disaster Management,” in International Symposium on Geo-information for Disaster Management - Gi4DM 2011, Turkey. [5] S. Coudert and T. J. Tanzi, “Formal Methods for Safe Design of Autonomous Systems Dedicated to Risk Management” in FirstT IFIP Conference on Information Technology in Disaster Risk Reduction, ITDRR 2016, Sophia, Bulgaria. [6] A. Platzer, “A complete axiomatization of quantified differential dynamic logic for distributed hybrid systems,” Logical Methods in Computer Science, vol. 8, no. 4, pp. 1–44, 2012. Special issue for selected papers from CSL’10. [7] R. Banach, M. Butler, S. Qin, N. Verma, and H. Zhu, “Core hybrid event-b i: Single hybrid event-b machines,” Science of Computer Programming, vol. 105, pp. 92 – 123, 2015. [8] C. L. Heitmeyer and E. I. Leonard, “Obtaining trust in autonomous systems: Tools for formal model synthesis and validation,” in FormaliSE 2015, USA, pp. 54–60, IEEE Press, 2015. [9] J. L. Krivine and G. Kreisel, “Éléments de logique mathématique (théorie des modèles)”, Dunod, Paris, 1966; “Elements of mathematical logic (model theory)”, North Holland, Amsterdam, 1967 [10] Michel Pagani, Damiano Mazza, « Preuves et programmes: Outils classiques », Cours M2, Master en Logique Mathématique et Fondements de l’Informatique, Université Paris Diderot - Paris 7 [11] Hugo Herbelin, « Contenu calculatoire des preuves de la logique classique », Cours M2, Master en Logique Mathématique et Fondements de l’Informatique, Université Paris Diderot - Paris 7 LES AUTEURS Sophie Coudert est maître de conférences à Télécom- ParisTech. Elle travaille sur les méthodes formelles et leur application à des domaines tels que les services télépho- niques, les SOC (Systems on Chip) ou les transports col- lectifs. Dominique Legros a effectué son doctorat au Centre de mathématiques appliquées de l’Ecole des mines de Paris. Il est actuellement directeur technique de ENGIE INEO UTS qui développe des solutions techniques pour le transport urbain.