Méthodes d'analyse pour la vérification de propriétés quantitatives – MAVEriQ

La variété des défis posés par les systèmes contrôlés par logiciel (en particulier les systèmes cyber-physiques) demande constamment de nouvelles techniques pour évaluer leur performance, sûreté et sécurité. Plus que de savoir si un système donné satisfait ces propriétés, on préfère savoir de combien il les satisfait.

Ainsi, les chercheurs introduisent plusieurs propriétés quantitatives : probabilité de violer une spécification, valeur d'un jeu de simulation, sémantique quantitative des logiques de spécification, mesures de robustesse, entropie comme mesure d'information ou comme mesure de l'ensemble des mauvais comportements. Pour calculer leurs valeurs, les approches usuelles de model-checking ont été augmentées de techniques quantitatives variées : programmation linéaire, théorie des jeux, équations différentielles et intégrales, etc.

Cette diversité cause plusieurs problèmes qui rendent la vérification quantitative extrêmement difficile : il est difficile de choisir la technique la plus pertinente parmi celles qui existent déjà et il est pénible de développer des variantes appropriées pour chaque critère qu'on veut évaluer (problèmes aggravés par des présentations et des terminologies non cohérentes).

Nous croyons qu'en raison de motifs communs apparaissant souvent, pour la vérification quantitative des systèmes temporisés, hybrides et/ou stochastiques, le développement de cadres unifiés atténuerait ces problèmes. Par exemple, les procédés pour calculer les volumes de langage d'un automate temporisé ou les distributions de probabilité des exécutions d'une chaîne de Markov ou d'un automate temporisé stochastique sont similaires. Les espaces des états, des transitions et des comportements sont munis d'une mesure et un opérateur de transfert transformant les mesures est établi. Les propriétés du système sont ensuite déduites des propriétés spectrales de l'opérateur (distribution stationnaire, vitesse de croissance du volume, ...). Le motif commun qui ressort de cet exemple, avec quelques variations, devrait, selon nous, pouvoir unifier bien d'autres problèmes quantitatifs.

La notion d'opérateur de transfert (et sa mesure associée) est centrale pour les méthodes que nous prônons (son analyse spectrale fournit de nombreuses informations sur les algorithmes d'itération de l'opérateur : convergence, vitesse de convergence, point fixe, ...). Son étude est le sujet du premier work package.

Les questions de la forme "Combien de comportements y a-t-il ?" ou "Combien ça coûte ?" sont formalisables en termes d'itérations d'un opérateur. Malheureusement, elles sont souvent algorithmiquement très complexes, voire indécidables. Des techniques d'abstraction et d'approximation permettent de répondre efficacement à ces questions, c'est le sujet du deuxième work package. Un outil prototype sera écrit et testé sur une étude de cas (contrôle robuste de systèmes cyber-physiques).

D'autres questions (robustesse) ont la forme "De combien les comportements d'un système évitent-ils un mauvais état ?" ou "De combien peut-on perturber un modèle ou son exécution en évitant toujours les mauvais états?". Celles-ci utilisent la notion de distance, pour laquelle plusieurs versions existent, avec leurs différentes propriétés. L'étude comparative des distances, leurs liens avec la méthode des opérateurs et leur application aux problèmes de robustesse constituent le troisième work package.

Enfin, quand la complexité du modèle est excessive ou si c'est une boîte noire (souvent vrai pour les systèmes cyber-physiques), sa validation demande d'utiliser des techniques de simulation, pour lesquelles plusieurs méthodes d’échantillonnage existent. Dans le dernier work package, nous considérons les échantillonnage exhaustifs (à distance e près) et probabilisés uniformes. Ces techniques seront aussi implémentées dans un outil et testées sur des études de cas de CPS de du Workshop ARCH (fournies par des acteurs industriels).