Compositional Abstraction for Timed Systems with Broadcast Synchronization
Hanyue Chen, Miaomiao Zhang, Frits Vaandrager
基于仿真的构图抽象有效地缓解了模型检查中的状态空间爆炸,特别是对于计时系统。 然而,现有方法不支持广播同步,这是多组分系统中非阻塞对多通信进行建模的重要机制。 因此,它们也缺乏一个并行组成运算符,它同时支持广播同步、二进制同步、共享变量和提交位置。 为了解决这个问题,我们提出了一个基于模拟的计时系统组合抽象框架,该框架支持这些建模概念,并与流行的UPPAAL模型检查器兼容。 我们的框架是通用的,唯一的额外限制是,在接收广播信号时,禁止计时自动机更新共享变量。 通过两个案例研究,我们的框架展示了与传统单体方法相比卓越的验证效率。
Simulation-based compositional abstraction effectively mitigates state space explosion in model checking, particularly for timed systems. However, existing approaches do not support broadcast synchronization, an important mechanism for modeling non-blocking one-to-many communication in multi-component systems. Consequently, they also lack a parallel composition operator that simultaneously supports broadcast synchronization, binary synchronization, shared variables, and committed locations. To a...