Utilisation limitée de la mémoire lors de l'analyse de modèles incomplets – GUMMIS

L'approche du model-checking en vérification formelle repose sur deux étapes essentielles : d'abord, représenter un système réel par un modèle formel, puis vérifier si ce modèle satisfait les spécifications données. De ce fait, le modèle doit appartenir à une classe suffisamment expressive pour capturer les propriétés critiques du système, tout en restant suffisamment simple pour en permettre l'analyse.

Différentes classes de modèles ont été développées pour représenter divers aspects du système, tels que les contraintes temporelles, les comportements stochastiques, la concurrence ou l'observabilité partielle, ainsi que pour tenir compte des incertitudes grâce aux paramètres ou au non-déterminisme. L'intégration de l’un ou plusieurs de ces éléments augmente souvent la complexité de l’analyse, conduisant parfois à des résultats d’indécidabilité. C'est pourquoi de nombreuses recherches ont identifié des sous-classes plus simples, généralement en limitant des caractéristiques comme le nombre d'horloges, de paramètres ou de dimensions dans le modèle.

Cependant, la complexité du model-checking ne résulte pas toujours uniquement de ces extensions. Souvent, la source des difficultés réside dans les hypothèses irréalistes du modèle de base. Par exemple, les automates temporisés peuvent exécuter une infinité d'actions en un temps fini, un scénario qui peut mener à des résultats qui, bien que théoriquement correct, présentent un intérêt pratique limité. Il est donc essentiel d'intégrer des hypothèses réalistes dans le modèle, telles que la présence limitée de certaines ressources, des contraintes temporelles ou une concurrence restreinte.

Le but du projet GUMMIS est de trouver le juste équilibre entre la puissance d'expression du modèle et la tractabilité de l'analyse, en introduisant des restrictions reflétant certaines des limitations réelles du système — notamment en termes de mémoire finie.