继承 DEPLOY 遗产：代码生成与仿真
软件工程
2012-10-29 v1
摘要
RODIN 与 DEPLOY 项目为 Event-B 的进一步理论与实际（方法论与工具）进展奠定了坚实基础。我们目前的兴趣在于使用 Event-B 进行信息物理系统的协同仿真。利用该方法，我们旨在分别对环境的各种特征进行仿真，以测试可部署代码。本文有两项贡献：第一是扩展了 DEPLOY 的代码生成工作，增加了从 Event-B 状态机图生成代码的能力；第二是描述了如何利用从状态机生成的代码在单一任务中仿真环境，并仿真并发执行的状态机。我们展示了如何通过控制仿真中遍历非确定性转移的相对速率来检测代码以引导仿真。
引用
@article{arxiv.1210.7034,
title = {Building on the DEPLOY Legacy: Code Generation and Simulation},
author = {Andrew Edmunds and Michael Butler and John Colley},
journal= {arXiv preprint arXiv:1210.7034},
year = {2012}
}
备注
In Proceedings of DS-Event-B 2012: Workshop on the experience of and advances in developing dependable systems in Event-B, in conjunction with ICFEM 2012 - Kyoto, Japan, November 13, 2012