文件名称：使用 Event-B 的系统建模：洞察-研究论文
文件大小：776KB
文件格式：PDF
更新时间：2024-06-30 04:27:57
论文研究
存在多种建模语言和框架用于系统的形式化表示和分析。 本文旨在对基于 Event-B 的模型检查进行深入调查。 事件 B 是从早期的 B 语言演变而来的。 由于它对迭代改进的开放性，它已经引起了工业和学术界的合理关注，这些改进从系统的高级抽象开始验证设计。 Rodin 是一个工具，它为基于 Event-B 的模型检查和数学证明提供开源实现平台。 全球的研究人员正在将事件 B 用于工业自动化、嵌入式和安全关键系统的设计以及更多领域。 该手稿提出了一个经过充分研究的分类，考虑到了应用 Event-B 建模的各种广泛领域。 因此，已经确定了研究空白，以突出事件 B 的未来研究方向和应用领域。