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工具中。最后，通过涵盖各类规范的实验评估，对不同组合方法进行了比较。