用于验证 Event-B 精化插件的 Event-B 框架
软件工程
2017-01-05 v1
摘要
我们提出一个 Event-B 框架用于建模 Event-B 的理论基础。该框架旨在为 Event-B 自身重用精化开发过程。该框架首先通过 Event-B 上下文引入一个函数式内核，然后通过 Event-B 机器定义 Event-B 项目及其静态和动态语义。我们打算将此框架用于与分布相关的 Event-B 插件以及与时序组合和分解相关的 Event-B 扩展的验证。
引用
@article{arxiv.1701.00960,
title = {An Event-B framework for the validation of Event-B refinement plugins},
author = {Jean-Paul Bodeveix and Mamoun Filali and Mohamed Tahar Bhiri and Badr Siala},
journal= {arXiv preprint arXiv:1701.00960},
year = {2017}
}
备注
Event-B day 2016, Tokyo