Anzeige
Erschienen in:
2014 | OriginalPaper | Buchkapitel
Code Generation for Event-B
verfasst von : Andreas Fürst, Thai Son Hoang, David Basin, Krishnaji Desai, Naoto Sato, Kunihiko Miyazaki
Erschienen in: Integrated Formal Methods
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We present an approach to generating program code from Event-B models that is correct-by-construction. Correctness is guaranteed by the combined use of well-definedness restrictions, refinement, and assertions. By enforcing the well-definedness of the translated model, we prevent runtime errors that originate from semantic differences between the target language and Event-B, such as different interpretations of the range of integer values. Using refinement, we show that the generated code correctly implements the original Event-B model. We provide a simple yet powerful scheduling language that allows one to specify an execution sequence of the model’s guarded events where assertions are used to express properties established by the event execution sequence, which are necessary for well-definedness and refinement proofs.