从 Event-B 动作到 SQL 语句翻译的形式语义与可靠性
软件工程
2016-06-09 v1
摘要
EventB2SQL 工具将 Event-B 模型转换为持久化 Java 应用程序，这些应用程序将模型的状态存储在关系数据库中。大多数 Event-B 赋值被直接转换为 SQL 数据库修改语句，随后可在数据库上执行。在本工作中，我们为表示 Event-B 事件动作的赋值语句集合的翻译提供了形式语义，并证明了其可靠性。这使得生成的代码在正确性方面能够被放心使用。
引用
@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}
}