Generating Distributed Programs from Event-B Models

Autor: Horatiu Cirstea, Alexis Grall, Dominique Méry
Přispěvatelé: Proof-oriented development of computer-based systems (MOSEL), Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria), Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), TELECOM Nancy, Université de Lorraine (UL), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), LORIA UMR 7503 CNRS, INRIA, Université de LORRAINE
Jazyk: angličtina
Rok vydání: 2020
Předmět:
FOS: Computer and information sciences
ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES
Computer Science - Logic in Computer Science
Process (engineering)
Computer science
Computation
[INFO.INFO-DS]Computer Science [cs]/Data Structures and Algorithms [cs.DS]
02 engineering and technology
[INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE]
computer.software_genre
ACM: F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS
[INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL]
Simple (abstract algebra)
0202 electrical engineering
electronic engineering
information engineering
ComputingMilieux_MISCELLANEOUS
Soundness
Statement (computer science)
Computer Science - Programming Languages
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL]
Event (computing)
Programming language
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
020207 software engineering
Logic in Computer Science (cs.LO)
Transformation (function)
Distributed algorithm
020201 artificial intelligence & image processing
computer
Programming Languages (cs.PL)
Zdroj: International Workshop on Verification and Program Transformation
International Workshop on Verification and Program Transformation, Apr 2020, Dublin, Ireland. pp.110-124, ⟨10.4204/EPTCS.320.8⟩
[Research Report] LORIA UMR 7503 CNRS, INRIA, Université de LORRAINE. 2020, pp.36
VPT/HCVS@ETAPS
DOI: 10.4204/EPTCS.320.8⟩
Popis: Distributed algorithms offer challenges in checking that they meet their specifications. Verification techniques can be extended to deal with the verification of safety properties of distributed algorithms. In this paper, we present an approach for combining correct-by-construction approaches and transformations of formal models (Event-B) into programs (DistAlgo) to address the design of verified distributed programs. We define a subset LB (Local Event-B) of the Event-B modelling language restricted to events modelling the classical actions of distributed programs as internal or local computations, sending messages and receiving messages. We define then transformations of the various elements of the LB language into DistAlgo programs. The general methodology consists in starting from a statement of the problem to program and then progressively producing an LB model obtained after several refinement steps of the initial LB model. The derivation of the LB model is not described in the current paper and has already been addressed in other works. The transformation of LB models into DistAlgo programs is illustrated through a simple example. The refinement process and the soundness of the transformation allow one to produce correct-by-construction distributed programs.
In Proceedings VPT/HCVS 2020, arXiv:2008.02483
Databáze: OpenAIRE
Externí odkaz: