Analyses paramétrées de systèmes concurrents – PACS

Le model-checking est une techniques qui a acquis une certaine reconnaissance
académique, mais son applicabilité en pratique reste toutefois un peu
décevante. Cela est du en partie à deux problèmes : une modélisation un peu
rigide au détriment de la capacité d'abstraction et du passage à l'échelle,
ainsi qu'un retour d'information insuffisant lors de la vérification. Dans ce
projet, nous attaquons ces problèmes en nous plaçant dans le cadre plus riche
et plus souple des modèles formels paramétrés.

Dans ce contexte, certaines caractéristiques du système, comme le nombre de
processus, les délais de communication ou la consommation d'énergie, peuvent ne
pas être des constantes numériques mais des paramètres inconnus. Les questions
liées au model-checking sont alors plus intéressantes : telle propriété
est-elle vraie pour toutes les valeurs possibles des paramètres ? Pour au moins
une ? Voire, quelles sont toutes les valeurs de paramètres la satisfaisant.

En nous appuyant sur les compétences du consortium sur des sujets comme le
model-checking régulier, les systèmes temporisés ou probabilistes, ainsi que
sur nos précédentes contributions à la vérification avec un nombre paramétré de
processus, ou des systèmes temporels paramétrés, incluant le développement
d'outils logiciels, nous développons dans ce projet de nouveaux modèles et
techniques, pour étendre le champ d'application des modèles paramétrés.

Pour atteindre cet objectif, nous étudions les paramètres dans le contexte des
systèmes discrets ou temporisés - hybrides, chacun d'eux également étendu avec
des informations quantitatives : coûts (p. ex. consommation d'énergie) ou
probabilités. Cela nous donne six tâches où les paramètres sont :
1. discrets
2. temporels
3. discrets et temporels ensemble
4. dans les modèles à coûts
5. dans les modèles probabilistes discrets
6. dans les modèles probabilistes à temps continu

Les modèles paramétrés ont un intérêt certain mais les problèmes théoriques
associés sont difficiles. Par exemple, pour le modèle de base des automates
temporisés paramétrés, la simple existence d'une valeur de paramètre
telle qu'un état donné soit accessible est généralement indécidable, même avec
un seul paramètre.

En conséquence, dans toutes ces tâches, nous suivons une approche commune
prenant en compte ces difficultés : formalisation, études de classes décidables
et conception d'algorithmes efficaces (notamment pour la synthèse),
construction pour la classe générale de semi-algorithmes efficaces se
comportant bien dans les cas réalistes, et finalement implémentation de
prototypes.

Cela pose des problèmes difficiles et originaux tels que l'extension du
model-checking régulier aux graphes, l'utilisation d'automates infinis pour
représenter les ensembles de configurations, la construction de classes
décidables utiles de systèmes temporisés ou hybrides ou de propriétés, la
conception de techniques de synthèse approchées, l'étude de modèles à coûts
paramétrés, probabilistes paramétrés, ou l'extension de la vérification
statistique aux modèles paramétrés.

Notre but est de produire des résultats scientifiques de grande qualité, de les
publier dans des journaux et conférences reconnus, mais aussi de produire des
outils logiciels pour transférer nos résultats à la communauté scientifique et à
l'enseignement supérieur. Enfin, nous souhaitons promouvoir la vérification
paramétrée au travers de l'organisation annuelle d'un workshop ouvert,
successeur du workshop SynCoP organisé en 2014.

Au-delà des applications classiques comme les systèmes embarqués, nous en
envisageons de nouvelles comme les maisons intelligentes, où les paramètres
peuvent modéliser les spécificités des résidents. Dans ce contexte, les modèles
à coûts sont d'un intérêt particulier pour modéliser les problèmes
d'optimisation d'énergie.