扩展状态机的形式化精化

在传统的形式化开发过程中，例如使用B方法，非形式化的用户需求被（手动）翻译成一个全局抽象形式化规约。这一翻译尤其难以实现。Event-B方法被开发出来，以通过逐步精化增量式且形式化地构造这样的规约。每个增量考虑到新的属性和系统方面。在本文中，我们提出将一种称为代数状态转移图（ASTD）的图形化表示法与Event-B规约相耦合，以更好地理解软件行为。动态行为由ASTD捕获，其基于自动机和进程代数算子，而数据模型通过Event-B规约描述。我们提出一种方法，增量式地精化此类规约耦合，考虑到控制规约与数据规约之间新的精化关系与一致性条件。我们比较了采用每种方法所获得的规约在可读性与证明复杂性方面的表现。讨论了传统方法与我们的方法的优缺点。整个过程通过一个铁路CBTC类案例研究加以说明。我们的方法得到工具支持，可将ASTD转换为B，并将Event-B转换为B。