Automatic generation of proof obligations parameterised by domain theories implementation in Event-B : The EB4EB Framework
Génération automatique d’obligations de preuves paramétrée par des théories de domaine dans Event-B : Le cadre de travail EB4EB
Résumé
Nowadays, we are surrounded by complex critical systems such as microprocessors, railways, home appliances, robots, aeroplanes, and so on. These systems are extremely complex and are safety-critical, and they must be verified and validated. The use of state-based formal methods has proven to be effective in designing complex systems. Event-B has played a key role in the development of such systems. Event-B is a formal system design method that is state-based and correct-by-construction, with a focus on proof and refinement. Event-B facilitates verification of properties such as invariant preservation, convergence, and refinement by generating and discharging proof obligations.Additional properties for system verification, such as deadlock-freeness, reachability, and liveness, must be explicitly defined and verified by the designer or formalised using another formal method. Such an approach reduces re-usability and may introduce errors, particularly in complex systems.To tackle these challenges, we introduced the reflexive EB4EB framework in Event-B. In this framework, each Event-B concept is formalised as a first-class object using First Order Logic (FOL) and set theory. This framework allows for the manipulation and analysis of Event-B models, with extensions for additional, non-intrusive analyses such as temporal properties, weak invariants, deadlock freeness, and so on. This is accomplished through Event-B Theories, which extend the Event-B language with the theory's defined elements, and also by formalising and articulating new proof obligations that are not present in traditional Event-B. Furthermore, Event-B's operational semantics (based on traces) have been formalised, along with a framework for guaranteeing the soundness of the defined theorems, including operators and proof obligations. Finally, the proposed framework and its extensions have been validated across multiple case studies, including Lamport's clock case study, read/write processes, the Peterson algorithm, Automated Teller Machine (ATM), autonomous vehicles, and so on.
De nos jours, nous sommes entourés de systèmes critiques complexes tels que les microprocesseurs, les trains, les appareils intelligents, les robots, les avions, etc. Ces systèmes sont extrêmement complexes et critiques en termes de sûreté, et doivent donc être vérifiés et validés. L'utilisation de méthodes formelles à états s'est avérée efficace pour concevoir des systèmes complexes. Event-B a joué un rôle clé dans le développement de tels systèmes. Event-B est une méthode formelle de conception de systèmes à états avec une approche correcte par construction, qui met l'accent sur la preuve et le raffinement. Event-B facilite la vérification de propriétés telles que la préservation des invariants, la convergence et le raffinement en générant des obligations de preuve et en permettant de les décharger.Certaines propriétés additionnelles du système, telles que l'absence d'inter-blocage, l'atteignabilité ou encore la vivacité, doivent être explicitement encodées et vérifiées par le concepteur, ou formalisées à l'aide d'une autre méthode formelle. Une telle approche pénalise la réutilisabilité des modèles et des techniques, et peut introduire des erreurs, en particulier dans les systèmes complexes.Pour pallier cela, nous avons introduit un "framework" réflexif EB4EB, formalisé au sein de Event-B. Dans ce cadre, chacun des concepts d'Event-B est formalisé comme un objet de première classe en utilisant la logique du premier ordre (FOL) et la théorie des ensembles. EB4EB permet la manipulation et l'analyse de modèles Event-B, et permet la définition d'extensions afin de réaliser des analyses supplémentaires non intrusives sur des modèles, telles que la validation de propriétés temporelles, l'analyse de la couverture d'un invariant, ou encore l'absence de blocage. Ce framework est réalisé grâce aux théories d'Event-B, qui étendent le langage d'Event-B avec des éléments définis dans des théories, et aussi en formalisant de nouvelles obligations de preuves, qui ne sont pas présentes initialement dans Event-B.De plus, la sémantique opérationnelle d'Event-B (basée sur les traces) a été formalisée, de même qu'un cadre qui sert à garantir la correction des théorèmes définis, y compris les opérateurs et les obligations de preuve. Enfin, le cadre proposé et ses extensions ont été validés dans de multiples études de cas, notamment l'horloge de Lamport, le problème du lecteur/rédacteur, l'algorithme de Peterson, les distributeurs automatiques de billets (DAB), les véhicules autonomes, etc.
| Origine | Version validée par le jury (STAR) |
|---|