Formal Semantics and Soundness of a Translation from Event-B Actions to SQL Statements
Software Engineering
2016-06-09 v1
Abstract
The EventB2SQL tool translates Event-B models to persistent Java applications that store the state of the model in a relational database. Most Event-B assignments are translated directly to SQL database modification statements, which can then be executed against the database. In this work, we present a formal semantics for and prove the soundness of the translation of sets of assignment statements representing the actions of an Event-B event. This allows the generated code to be used with confidence in its correctness.
Cite
@article{arxiv.1606.02669,
title = {Formal Semantics and Soundness of a Translation from Event-B Actions to SQL Statements},
author = {Tim Wahls},
journal= {arXiv preprint arXiv:1606.02669},
year = {2016}
}