ConStaBL——以状态机重新审视软件工程

状态图是一种用于系统的可视化建模语言。在本文中，我们扩展了先前关于带有局部变量的模块化状态图的工作，并提出了带有并发的状态图的更新操作语义。我们的状态图变体具有局部变量，其与语言语义的其余部分有显著的交互。我们的语义在仿真中不允许转移冲突，并且在该意义上比大多数其他可用的状态图语义更为严格。它允许并发执行动作代码的任意交错，从而实现对系统的更精确建模及相应的上游分析。我们以仿真算法的形式给出操作语义。我们还基于我们的语义建立了用于定义冲突转移与有效仿真的准则。我们的语义是可执行的，可用于仿真状态图模型并验证其正确性。我们提出了一个对状态图模型进行模糊测试的初步设置，这一想法在文献中似乎尚无先例。我们已将我们的仿真器与知名模糊测试工具结合，对具有非平凡规模的状态图模型进行模糊测试，并发现了通过人工检查难以发现的问题。