Learning and Verifying Temporal Specifications for Cyber-Physical Systems

Apprentissage et vérification de systèmes complexes avec des spécifications temporelles Au cours de la dernière décennie, on a assisté à une augmentation sans précédent de l'incorporation de systèmes cyber-physiques complexes utilisés pour effectuer des tâches complexes. La vérification de ces systèmes est nécessaire pour garantir leur sécurité et leur fiabilité, en particulier dans les scénarios de sécurité critiques. La vérification formelle s'est avérée être une méthode éprouvée pour vérifier systématiquement ces systèmes. Elle fournit notamment des techniques permettant de contrôler l'exécution des systèmes par rapport à une spécification formelle. Souvent, ces spécifications sont difficiles à concevoir manuellement, d'où la nécessité de les générer automatiquement à partir des exécutions du système pour les utiliser à des fins de vérification. La logique temporelle a gagné en popularité en tant que spécification formelle en raison de sa rigueur mathématique, de son interprétabilité par l'homme et de sa compatibilité avec diverses techniques de vérification formelle. L'objectif de cette thèse est double : (i) Développer des algorithmes pour apprendre automatiquement des spécifications temporelles à partir d'exécutions de systèmes ; (ii) Appliquer des techniques de vérification formelle pour évaluer l'exactitude du système par rapport aux spécifications acquises.Pour atteindre ces objectifs, dans la partie apprentissage, nous présentons deux algorithmes pour apprendre des spécifications dans des logiques temporelles telles que LTL, MTL et STL. Nos algorithmes sont dans le cadre de l'apprentissage passif et apprennent des spécifications qui séparent un ensemble fini de comportements positifs du système d'un ensemble fini de comportements négatifs. Pour les spécifications LTL, nous présentons un algorithme basé sur la programmation dynamique qui s'appuie sur une forme normale pour un fragment de LTL et utilise des techniques d'énumération efficaces pour apprendre des formules concises à partir des exécutions du système. Pour MTL et STL, nous développons des techniques basées sur un résolveur SMT pour apprendre des formules qui sont non seulement concises mais aussi efficaces pour être appliquées à la vérification formelle du système. Nos algorithmes sont mis en œuvre dans des outils appelés SCARLET et TEAL, et leur efficacité est démontrée par des résultats expérimentaux. Pour la partie vérification, nous nous concentrons sur les problèmes de synthèse de paramètres LTL des One-counter automata, qui est l'un des modèles formels fondamentaux pour représenter les systèmes complexes, à savoir les systèmes avec un espace d'état discret mais infini. One-counter automata sont obtenus en étendant les automates classiques à états finis avec un compteur dont la valeur peut s'étendre sur des entiers non négatifs et être testée pour zéro. Les mises à jour et les tests applicables au compteur peuvent être paramétrés en introduisant un ensemble de variables à valeur entière appelées paramètres. Le problème de la synthèse des paramètres LTL pour de tels automates est de savoir s'il existe une évaluation des paramètres telle que toutes les exécutions infinies de l'automate satisfont une spécification LTL. En s'appuyant sur les travaux existants dans la littérature, (i) nous montrons un réencodage prudent du problème en une restriction décidable de l'arithmétique de Presburger avec divisibilité (PAD), le plus grand fragment décidable connu de PAD jusqu'à présent ; (ii) Nous prouvons que le problème de la synthèse des paramètres est décidable en général et en 3NEXP ; (iii) Nous donnons des algorithmes EXPSPACE pour les cas particuliers du problème où les paramètres ne peuvent être utilisés que dans des contre-tests. Enfin, (iv) nous présentons brièvement le résultat de décidabilité de ce problème sur une extension de ce modèle avec des contraintes de Parikh.