无穷与有限轨迹上 LTL 性质的异步组合

由于组件并发交错与交换输入/输出数据的方式，异步软件组件的验证提出了重大挑战。组合策略旨在通过将验证单个组件局部性质的任务与组合它们以实现全局性质的任务分离开来解决这一问题。本文集中于采用符号模型检测技术来验证通过数据端口交互的异步软件组件上以线性时序逻辑（LTL）指定的性质。与基于事件的组合不同，局部性质现在可以对来自其他组件的输入施加约束，增加了其组合的复杂性。我们考虑了无穷轨迹上的标准语义以及有限轨迹上的截断语义，以允许仅对组件进行有限次调度。我们提出了一种新颖的 LTL 重写方法，该方法在考虑组件无穷或有限执行轨迹交错的同时，将局部性质转换为全局性质。我们证明了局部性质及其重写版本在局部符号上的投影的语义等价性。该重写还经过了优化，以减小公式大小，并在时序性质具有 stutter 不变性时保持其不变。这些方法已作为契约细化验证套件的一部分集成到 OCRA 工具中。最后，通过涵盖多种规范类型的实验评估，对不同的组合方法进行了比较。