Projet SIMOP

Synergie Simulation et Model-Checking Paramétré

Responsable: Olivier De Smet (LURPA), Laurent Fribourg (LSV).

L’objectif de ce projet collaboratif entre le LSV et LURPA est d’évaluer les performances d’une architecture de commande distribuée sujette à panne et d’estimer la plage de valeur des paramètres de fonctionnement de l’architecture qui garantit les performances attendues. Les différents modes de fonctionnement (mode nominal, différentes configurations de mode dégradé) seront pris en compte.

Pour atteindre cet objectif on utilisera le model-checking temporisé paramétré pour sa capacité à fournir des résultats à la fois quantitatifs et garantis sur les paramètres de fonctionnement recherchés. Cependant sa mise en œuvre est généralement limitée par la complexité intrinsèque du problème. Afin d’éviter cet écueil on utilisera au préalable des observations issues de simulation pour limiter l'espace de recherche du model-checking. Ainsi la méthode de model-checking temporisé et paramétré sera dirigée par des résultats issus de simulation.