Asynchronous Composition of LTL Properties over Infinite and Finite Traces

TL;DR

The paper tackles verification of asynchronous components connected through data ports, introducing a rewriting-based compositional approach for LTL properties under both infinite and finite traces. It advances a First Order Past LTL with weak truncated semantics and an ITS-based asynchronous composition, providing both a general rewriting (R*) and an optimized variant (R^θ) to map local properties to global ones, including a fairness-aware variant under infinite executions. The approach is implemented in the OCRA tool and evaluated on toySender models, automotive contracts, and pattern-based benchmarks, demonstrating correct equivalence between rewritten global properties and local constraints and showing practical scalability. The work enables robust safety verification for asynchronous systems with finite scheduling, offering practical impact for contract refinement and industrial verification workflows.

Abstract

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.

Figures (7)

• Figure 1: Figure representing the sender model. The colour red represents input variables while the colour blue represents the output variables.
• Figure 2: Graphical representation of $@\tilde{F}$ and $@\tilde{P}$.
• Figure 3: Graphical view of trace projection. White states of $\pi$ represent the states of the sequence $map_i$, pink states represent states in which the local component stutters, and red arrows represent the link between the states of $\pi$ and the states of $\pi_i$ formally represented by $map_k$.
• Figure 4: Graphical representation of rewriting of $X a$. $\pi$ represents the local trace while $\pi^{ST}$ represents the trace of the composition. White states are states of local trace while pink states are states in which the local component is not running. In this example, $a$ is an input variable which happens to be true in state $s_i$ and $s_{i+1}$ of local trace $\pi$ and state $\bar{s}_j$. To show the intuition of the rewriting, we show that Release operator permits to skip the pink states (which are not relevant w.r.t. the local trace). Finally, at state $\bar{s}_{j+3}$$a$ is evaluated since $run$ is true.
• Figure 5: Graphical representation of rewriting of $U$. In this example both $a$ and $b$ variables are input variables. Local trace $\pi$ satisfies $aU b$ at position $i$ since $a$ is true at state $s_i, s_{i+1}$ while $b$ is true at state $s_{i+2}$. The corresponding global trace contains 2 additional states ($\bar{s}_{j+1},\bar{s}_{j+2}$) which are not considered in the rewriting since $\neg state$ holds these 2 states. Finally, the state $\bar{s}_{j+4}$

Theorems & Definitions (49)

• Definition 3.1
• Definition 3.2
• Example 3.3
• Example 3.4
• Definition 3.5
• Theorem 3.6
• proof
• Definition 3.7
• Theorem 3.8
• proof