HDR Ciprian TEODOROV
presented & defended at ENSTA Bretagne on Monday, April 3, 2023 at 14:00.
“G∀min∃: Exploring the Boundary Between Executable Specification Languages and Behavior Analysis Tools”
Committee
- Prof. Frank SINGHOFF, Université de Bretagne Occidentale, FR – president of the jury.
- Prof. Frédéric BONIOL, ONERA Toulouse, FR – reviewer.
- Prof Stéphane DUCASSE, INRIA Lille, FR – reviewer.
- Prof. Hans VANGHELUWE, University of Antwerp, BE – reviewer.
- Prof. Jeff GRAY, University of Alabama, USA – examiner.
- Prof. Alain PLANTEC, Université de Bretagne Occidentale, FR – examiner.
- Emmanuel GAUDIN, Founder & CEO, PragmaDev, Paris, FR – invited member.
Abstract The formal verification community strives to prove the correctness of a specification using formal logic and mathematical proofs. The tremendous progress in computer-aided formal verification tools, along with an ever-growing number of success stories renders these methods essential in the system designer toolbox. However, with the advent of domain-specific models and languages, many formalisms are proposed for writing dynamic system specifications, each one adapted to the specific needs of the targeted domain. A new question emerges: How to bridge the gap between these domain-specific formalisms, geared toward domain experts, and the formal verification tools, geared towards mathematicians? One of the answers, ubiquitous in the literature, relies on using model transformations to syntactically translate the domain-specific model to the verification model. We argue that this approach is counterproductive leading to semantic multiplication, which requires equivalence proofs that can be hard to provide and maintain.
In this dissertation, I present a new semantic-level answer developed, refined, and evaluated during the last 10 years with the help of 6 postdoctoral fellows, 8 Ph.D. candidates, and 12 collaborative projects. This approach, named G∀min∃, promises a modular, compositional, and reusable software architecture allowing the design of a wide variety of behavior exploration tools. The core building block of this approach is a language-agnostic semantic-level interface, which acts as a bridge between the dynamic semantics of a domain-specific language and the behavior analysis tools. Here we propose a formalization of the interface along with some reusable operators for creating behavior analysis tools for interactive debugging, model-checking, and runtime monitoring. Besides reviewing almost a decade of fruitful research, this document allows me to introduce some new research directions, which hopefully will ease the burden of creating novel specification-design environments and render the design process more productive.
Résumé La communauté de la vérification formelle s’efforce de prouver la conformité d’une spécification par l’utilisation de la logique formelle et de preuves mathématiques. Les progrès considérables réalisés dans les outils de vérification formelle assistée par ordinateur, ainsi que le nombre croissant de réussites, rendent ces méthodes essentielles dans la boîte à outils des concepteurs de systèmes. Cependant, avec l’avènement des modèles et des langages spécifiques à un domaine, un grand nombre de formalismes ont été proposés pour écrire des spécifications de systèmes dynamiques, chacun étant adapté aux besoins spécifiques du domaine ciblé. Une nouvelle question émerge : Comment combler le fossé entre ces formalismes spécifiques au domaine, orientés vers les experts du domaine et les outils de vérification formelle, orientés vers les mathématiciens ? Une des réponses, omniprésente dans la littérature, repose sur l’utilisation de transformations de modèles pour traduire syntaxiquement le modèle spécifique au domaine vers le modèle de vérification. Nous soutenons que cette approche est contre-productive et conduit à une multiplication sémantique, qui nécessite des preuves d’équivalence qui peuvent être difficiles à fournir et à maintenir.
Dans ce manuscrit, je présente une nouvelle réponse au niveau sémantique développée, raffinée et évaluée au cours des 10 dernières années avec l’aide de 6 ingénieurs postdoctoraux, 8 candidats au doctorat et 12 projets collaboratifs. Cette approche, nommée G∀min∃, promet une architecture logicielle modulaire, compositionnelle et réutilisable permettant la conception d’une grande variété d’outils d’exploration du comportement. La brique de base de cette approche est une interface de niveau sémantique agnostique au langage, qui agit comme un pont entre la sémantique dynamique d’un langage spécifique au domaine et les outils d’analyse du comportement. Nous proposons ici une formalisation de l’interface ainsi que quelques opérateurs réutilisables pour la création d’outils d’analyse du comportement pour le débogage interactif, le contrôle de modèle et la surveillance de l’exécution. En plus de passer en revue près d’une décennie de recherches fructueuses, ce document me permet de présenter quelques nouvelles directions de recherche, qui, nous l’espérons, allégeront le poids de la création de nouveaux environnements de conception de spécifications, et rendront le processus de conception plus productif.