The verification of asynchronous software components poses significant challenges due to the way components interleave and exchange input/output data concurrently. Compositional strategies aim to address this by separating the task of verifying individual components on local properties from the task of combining them to achieve global properties. This paper concentrates on employing symbolic model checking techniques to verify properties specified in Linear-time Temporal Logic (LTL) on asynchronous software components that interact through data ports. Unlike event-based composition, local properties can now impose constraints on input from other components, increasing the complexity of their composition. We consider both the standard semantics over infinite traces as well as the truncated semantics over finite traces to allow scheduling components only finitely many times. We propose a novel LTL rewriting approach, which converts a local property into a global one while considering the interleaving of infinite or finite execution traces of components. We prove the semantic equivalence of local properties and their rewritten version projected on the local symbols. The rewriting is also optimized to reduce formula size and to leave it unchanged when the temporal property is stutter invariant. These methods have been integrated into the OCRA tool, as part of the contract refinement verification suite. Finally, the different composition approaches were compared through an experimental evaluation that covers various types of specifications.

翻译：异步软件组件的验证因组件间交错执行及并发交换输入/输出数据的方式而面临重大挑战。组合策略旨在通过将局部性质上的单个组件验证任务与组合这些组件实现全局性质的任务相分离来解决该问题。本文聚焦于运用符号模型检测技术，验证通过数据端口交互的异步软件组件上以线性时序逻辑（LTL）描述的性质。与基于事件的组合不同，局部性质现在可对其他组件的输入施加约束，从而增加了组合的复杂性。我们同时考虑了无限迹上的标准语义和有限迹上的截断语义，以允许组件仅被有限次调度。我们提出了一种新颖的LTL重写方法，该方法在考虑组件无限或有限执行迹交错的前提下，将局部性质转换为全局性质。我们证明了局部性质及其在局部符号上投影的重写版本在语义上的等价性。该重写还对化简公式尺寸进行了优化，并在时序性质具有停顿不变性时保持公式不变。这些方法已集成至OCRA工具中，作为契约精化验证套件的一部分。最后，通过覆盖多种规约类型的实验评估，对不同的组合方法进行了比较。