Asynchronous Composition of Local Interface LTL Properties

The verification of asynchronous software components is very challenging due to the non-deterministic interleaving of components and concurrent access to shared variables. Compositional approaches decouple the problem of verifying local properties specified over the component interfaces from the problem of composing them to ensure some global property. In this paper, we focus on symbolic model checking techniques for Linear-time Temporal Logic [24] (LTL) properties on asynchronous software components communicating through data ports. Differently from event-based composition, the local properties can specify constraints on the input provided by other components, making their composition more complex. We propose a new LTL rewriting that translates a local property into a global one taking into account interleaving with other processes. We demonstrate that for every possible global trace, the local LTL property is satisfied by its projection on the local symbols if and only if the rewritten LTL property is satisfied by the global trace. This rewriting is then optimized, reducing the size of the resulting formula and leaving it unchanged when the temporal property is stutter invariant. We also consider an alternative approach where the local formulas are first translated into fair transition systems and then composed. This work has been implemented inside the contract-based design model checking tool OCRA 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.