Transforming Event B Models into Verified C# Implementations

Autor: Rosemary Monahan, 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), Computer Science Department [Maynooth], National University of Ireland Maynooth (Maynooth University), Alexei Lisitsa and Andrei Nemytykh, Project PHC France Ireland 29863WG : Building Reliable Systems: Software Refinement meets Software Verification., Méry, Dominique, 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)-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)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), 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)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft
Rok vydání: 2018
Předmět:
ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO]
Correctness
Theoretical computer science
Computer science
[INFO.INFO-DS]Computer Science [cs]/Data Structures and Algorithms [cs.DS]
Spec#
[INFO.INFO-DS] Computer Science [cs]/Data Structures and Algorithms [cs.DS]
0102 computer and information sciences
02 engineering and technology
computer.software_genre
01 natural sciences
ACM: F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS
Consistency (database systems)
Software
Refinement calculus
0202 electrical engineering
electronic engineering
information engineering
refinement
correct-by-construction
Software system
implementation
Implementation
computer.programming_language
algorithm
business.industry
Programming language
transformation
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
computer.file_format
010201 computation theory & mathematics
020201 artificial intelligence & image processing
Executable
verification
business
computer
Zdroj: VPT@CAV
VPT 2013-First International Workshop on Verification and Program Transformation
VPT 2013-First International Workshop on Verification and Program Transformation, Alexei Lisitsa and Andrei Nemytykh, Jul 2013, Saint Petersburg, Russia. pp.57-73
ISSN: 2398-7340
DOI: 10.29007/9wm9
Popis: The refinement-based approach to developing software is based on thecorrect-by-construction paradigm were software systems are constructed via the step-by-step refinement of an initial high-level specification into a final concrete specification. Proof obligations, generated during this process are discharged to ensure the consistency between refinement levels and hence the system's overall correctness.Here, we are concerned with the refinement of specifications using the Event B modelling language and its associated toolset, the Rodin platform. In particular, we focus on the final steps of the process where the final concrete specification is transformed into an executable algorithm. The transformations involved are (a) the transformation from an Event B specification into a concrete recursive algorithm and (b) the transformation from the recursive algorithm into its equivalent iterative version. We prove both transformations correct and verify the correctness of the final code in a static programme verification environment for C# programs, namely the Spec# programming system.
Databáze: OpenAIRE
Externí odkaz: