Modélisation formelle des systèmes critiques
Description détaillée
Composition de langages et de formalismes
La modélisation d'un système peut faire appel à différent formalismes et langages de modélisation pour :
- ses différents composants (automate pour un contrôleur, équations différentielles pour la partie physique, réseaux à flots de données pour la régulation etc.)
- ses différents aspects (fonctionnel, sûreté, consommation d'énergie etc.)
- les différents niveaux d'abstraction auquel on le considère (exigences, spécification, modèles abstraits, implémentations, …)
- les différentes activités de conception (spécification, synthèse, vérification, diagnostic)
On est donc naturellement amené à utiliser conjointement différents formalismes et langages lors de la conception d'un système :
- au moment de l'intégration, il faut combiner les différents composants et s'assurer de la correction de cette composition
- lors des changements de niveau d'abstraction (raffinement), il faut assurer la cohérence des modèles de chaque niveau
- il faut s'assurer que les différentes vues d'un système (fonctionnelles, performances, consommation) ne sont pas contradictoires.
- il faut assurer la cohérence entre les modèles utilisés pour différentes activités.
Méthodologie de développement et ingénierie des modèles
Les méthodologies de développement permettent de contrôler le processus de conception d'un système. L'ingénierie des modèles fournit un cadre et des outils pour créer des modèles, les transformer, définir des langages de modélisation.
Il reste nécessaire de donner un sens précis aux modèles et à leurs transformations, et les méthodologies de développement doivent prendre en compte la sémantique des modèles. L'utilisation des méthodes formelles dans ce cadre permet de compléter la panoplie d'outils purement syntaxiques qui existent, et de vérifier la cohérence des différents modèles utilisés.
Utilisation conjointe de différentes techniques de vérification
La vérification d'un système reste un problème difficile, même lorsqu'on dispose d'une spécification formelle et d'un modèle formel de sa réalisation. Les méthodes complètement automatiques (model-checking) sont appréciées des industriels, mais se heurtent aux limites théoriques des formalismes utilisés. Les méthodes à base de preuves permettent de vérifier des systèmes plus complexes, mais elles font appel à du personnel très spécialisé. Enfin, le test, lorsque la génération des scénarios est faite correctement, reste un outil efficace et relativement simple à mettre en œuvre, même s'il n'est pas exhaustif. Une autre approche consiste à synthétiser le contrôleur du système de façon à ce qu'il soit correct par construction.
L'estimation d'état d'un système (par nature seulement partiellement observable) en fonctionnement, dès que celui-ci s'écarte du fonctionnement nominal en raison de la présence d'aléas, est un enjeu important, qui prélude aux tâches de diagnostic ou de planification d'actions, surtout pour des systèmes autonomes aux ressources limitées. Les propriétés associées qui vont garantir la possibilité de telle ou telle action durant le suivi en ligne peuvent souvent se vérifier hors-ligne sur le modèle de conception. La preuve de ces propriétés formelles (telle que la diagnosticabilité en vue de synthétiser un diagnostiqueur en ligne) peut se heurter à un problème d'indécidabilité comme par exemple pour les automates hybrides modélisant des systèmes hybrides. Il faut alors recourir à des (sur-) ou (sous-)approximations par des formalismes (par exemple automates temporisés) pour lesquels la vérification des propriétés considérés devient décidable et établir une correspondance entre le résultat d'une propriété sur un système approché et le résultat de ce que serait une propriété approchée sur le système réel, avec garantie à epsilon près.
La vérification d'un système complet fait appel à ces différentes techniques, et plusieurs problèmes sont à traiter pour cela :
- le recouvrement entre méthodes (qu'est-il nécessaire de tester quand on a prouvé certaines propriétés sur un système ?)
- l'aspect complémentaire entre les méthodes (guider un model-checker en lui donnant les propriétés déjà prouvées)
- la combinaison des propriétés vérifiées (prouver la correction d'un algorithme sachant qu'on a prouvé qu'une variable d'un système continu ne peut pas sortir d'un certain domaine).
C'est particulièrement le cas pour les systèmes hybrides, qui mélangent discret et continu par le biais de transitions. Cette application a besoin de techniques permettant de raisonner sur les équations différentielles, que ce soit par extension de prouveurs SMT ou par de la preuve interactive. Un verrou est de pouvoir lier un raisonnement mathématique complexe avec une exécution concrète d'un programme (par exemple fait avec des nombres à virgule flottante).
Exemples
Coordination de composantes hétérogènes
Le langage TESL est un langage de spécification polychrone et temporisé pour décrire la causalité et les contraintes temporelles entre événements survenant dans différents composants d'un système. Une sémantique dénotationnelle et une sémantique opérationnelle ont été définies pour TESL en Isabelle/HOL, avec preuve de propriétés sur ces sémantiques.
Vérification de systèmes logiciels automobiles
Les fonctions logicielles présentes dans les voitures coûtent cher à tester. Nous avons montré, sur l'exemple d'un régulateur de vitesse adaptatif, que la génération automatique d'invariants bien choisis permet d'obtenir de très bon résultats pour la vérification de propriétés de modèles SCADE QRS2019. D'autre part, il est possible d'évaluer la qualité d'une spécification par mutation du modèle et comptage du nombre de mutants qui ne sont pas rejetés par cette spécification NFM2020.
Cosimulation de systèmes cyber-physiques avec FMI
La mise au point d'une simulation de système cyber-physique (ici des smart grids) est complexe car il faut fédérer des simulateurs issus d'outils qui utilisent différents formalismes (automates, code Java, modèles Modelica), et les formalismes discrets ne sont pas entièrement supportés par FMI. L'ingénierie des modèles permet de créer des DSL pour décrire ces modèles hétérogènes, et des transformations de modèles permettent de générer les fichiers nécessaires à la co-simulation en limitant les risques d'erreur grâce aux vérifications sémantiques faites sur les modèles MODELSWARD2020.
Modélisation de systèmes à base d’événements.
La méthode Event-B a été utilisée pour implémenter une démarche de modélisation et de vérification de systèmes à base d'états et d'événements. Les actions effectuées par les événements permettent la transition entre états. L’opération de raffinement est utilisée pour structurer le développement, et la preuve de théorèmes pour vérifier des propriétés sur ces systèmes. Comme application de notre démarche, nous avons étudié des problématiques liées aux IHM multimodales Computing2015 et à l'orchestration de services TLSDK2013.
Intégration des ontologies dans le développement de systèmes discrets
Lors de la conception d'un système, l'intégration des contraintes liées à domaine métier est un facteur déterminant pour la satisfaction des exigences système. Cette connaissance du domaine est le plus souvent modélisée grâce à des ontologies qui permettent d'exprimer des propriétés sur les données du domaine. Notre approche propose d'intégrer les ontologies des domaines dans un processus de développement s'appuyant sur Event-B. Elle consiste à anoter les modèles Event-B avec les concepts de l'ontologie, ce qui suppose une formalisation de l'ontologie en Event-B. L'intégration de la description en Event-B de l'ontologie d'un domaine permet de contraindre le système en cours de conception par l'ontologie, et de valider des propriétés du domaine MEDI2019.