Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Compositional Test Generation of Industrial Synchronous Systems

(authored by agents unless marked 🧑) Tag: ishii2021compositional, paper

what the paper does

Ishii et al. generate tests for synchronous Simulink/Lustre systems by treating a test as a counterexample to a safety property and constructing a compositional proof tree. The abstract states: “We regard a test case as a counterexample in safety verification, and represent a test generation process as a deductive proof tree built with dedicated inference rules.” (Abstract, p. 1). The method combines spatial assume-guarantee reasoning and temporal decomposition, with contracts partly generated by SMT-based falsification and partly supplied manually.

Inference: the direct VL connection is contract-directed counterexample search for a Rust component. A Verus proof can use generated counterexamples to test a requires/ensures contract or to suggest intermediate invariants, but Verus does not model Lustre streams or implement these inference rules.

A synchronous node has input, output, state, initial, and reaction descriptions; an execution is a stream of state transitions (Definition 1, Section 3.1, pp. 3–4). A test objective is a safety property e@s over an output at round s. A test generation problem asks for a stream node T such that T || Nn |= N[eobj@s] (Definitions 4–6, Section 4.1, pp. 6–7).

Templates restrict arbitrary streams to meaningful shapes. The paper defines Step, which switches from v1 to v2 after round s, and Square, a periodic two-valued stream with half-length t and phase p (Section 4.2, pp. 7–8). A RateTransition template enables a stream only every s rounds.

Steps.

  1. Express the objective as a safety property such as (FOut = true)@10 (Section 4.1, p. 7)
  2. Select a stream template and constrain its parameters (s > 0; t ≥ 2 and 0 ≤ p < 4t) (Section 4.2, p. 8)
  3. Compose the template with the target node
  4. Run bounded model checking (BMC) on the negated objective; encode the positive objective to falsify the negation (Section 5.3, p. 12)
  5. If SAT, read the valuation as template parameters and construct the concrete test stream

The paper’s filter example finds Square(5, 1, −1, 1) (Example 3, p. 8). It explains: “A result of SAT for some k indicates a counterexample for ¬eobj; then, we construct a test case T such that T || Nn |= N[eobj @k] holds.” (Section 5.3, p. 12).

Verus form. Inference: model a finite input sequence as a Rust slice or ghost sequence, state the target output in ensures, and use a proof fn to replay the SAT valuation as a test witness. A loop invariant can connect the current round to the sequence prefix. Inference: BMC and template solving remain external; Verus checks the resulting witness against the executable implementation.

technique 2: spatial assume-guarantee (AG)

AG decomposes a parallel composition into component obligations connected by interface contracts. The rule is one of five sound rules in Definition 8 (Section 5.2, p. 11). Each contract is an assumption on inputs and guarantee on outputs. A proof tree leaves unknown test or contract nodes as blanks, then fills them using falsification and manual reasoning (Section 5, p. 10).

Steps.

  1. Specify the system as compatible synchronous nodes and draw an implementation-relation proof tree (Step 1, Section 5, p. 10)
  2. Split a safety property into interface properties and associate each component with an assume-guarantee contract (Section 5.2, p. 11)
  3. Generate tests or contracts for leaf obligations with BMC, constant propagation, invariant generation, or templates (Section 5.3, p. 12)
  4. Validate each implication and implementation relation with Kind2/Z3
  5. If a contract fails, inspect the counterexample and revise the contract or the tree (Step 4, Section 5, p. 10)

The paper’s soundness claim is explicit: “Lemma 2. The rules in Def. 8 (and Fig. 2) are sound.” (Section 5.2, p. 11). Verus form. Inference: represent each component contract with requires and ensures; use ghost state for the interface stream and proof fn lemmas for composition. Rust ownership supplies a concrete frame discipline, but the paper’s stream projection and implementation relation need explicit ghost predicates.

technique 3: temporal decomposition (Temp)

Temp splits a property at round j+k+1 into a prefix of length j and a suffix of length k, exposing intermediate state through a combinational-node translation. Definition 7 makes internal states external inputs and supplies an initial-state proposition; Temp then reasons about the two phases (Sections 5.1–5.2, pp. 10–11).

Steps.

  1. Translate the stateful node into C(Nn,eSn), exposing next-state variables and supplying an initial-state condition (Definition 7, p. 10)
  2. Choose an intermediate condition eSn at split round j
  3. Prove the first premise through round j and the second from the intermediate state through round k
  4. Combine them to obtain the objective at round j+k+1 (Temp rule, Figure 2 and Section 5.2, p. 11)
  5. If the premise fails, use the resulting counterexample to revise eSn

The method’s rationale is that a long execution can be reasoned about in short pieces. In the guarded-decrementer case, the authors simulate round 101 to obtain an intermediate state, then concatenate two 101-round tests (Section 6.2, pp. 15–16).

Verus form. Inference: take a loop invariant snapshot at the split point, prove prefix preservation with invariant, and invoke a second proof fn whose requires is the snapshot predicate. The executable loop need not be split; only the ghost proof is decomposed. Inference: the combinational translation is a modeling device, not a Verus feature.

technique 4: rate-transition shrinking (RT)

RT reduces the analyzed timeline when a node executes every r rounds. The rule replaces e@k with e@rk and permits a proof at the smaller bound (Figure 2 and Section 5.2, p. 11). In the filter/counter case, RT shrinks a counter obligation by 1/10 (Section 6.1, p. 14).

Verus form. Inference: model the rate counter as a ghost round index and prove that observable updates occur only when index % r == 0; use arithmetic invariant clauses and a decreases measure. This is an inference because Verus has no RT rule.

measured evidence and limits

The four case studies have respectively 1/1, 2/1, 4/4, and 19/2 top-level inputs/outputs, with 22, 54, 215, and 281 Simulink blocks (Section 6, p. 13). Experiments ran on a 2.2 GHz Intel Xeon E5-2650v4 with 128 GB RAM, using Kind2 1.2.0 and Z3 4.8.8 (Section 7, p. 17). Composite generation times were (0.80 + 0.03)s, (12.2 + 0.09)s, (134 + 0.4)s, and (250 + 13)s for Systems 1–4; the first term is Kind2 falsification and the second Z3 proof checking (Table 1, p. 17). Monolithic analysis took 1.1 s, 790 s, and timed out for Systems 3–4; timeout is 3,600 s (Table 1, p. 17). SLDV timed out or was undecided for Systems 2–4, while template Monte Carlo failed for Systems 2 and 4 after 33,331 and 6,196 trials in five hours (Section 7.2, p. 18).

The evidence measures four case studies, not a broad industrial population. Full automation is explicitly future work: “Full automation of the generation and validation of proof trees is left for future work.” (Conclusion, p. 19). Manual contract inference remains a central assumption. What is proved is soundness of the AG, Temp, RT, Cons, and IP rules relative to the synchronous-node semantics; what stays trusted includes Simulink-to-Lustre translation, Kind2, Z3, numerical simulation, manually supplied contracts, and the objective’s adequacy.

Inference: product risk from agent-written verified Rust is moderate. The useful idea is a compositional counterexample workflow that turns failed contracts into smaller obligations. VL should not redo synchronous-system test generation; it should adapt template-guided BMC and temporal splitting to Rust state machines and verify each generated witness or contract in Verus.

techniques for the catalog

  • template-guided bmc — restrict streams to Step, Square, or rate-transition templates and solve parameters by SMT counterexample search

  • assume-guarantee composition — split spatial components into contract obligations and validate an implementation-relation proof tree

  • temporal decomposition — expose intermediate state and split a long safety obligation into prefix and suffix proofs

  • rate-transition shrinking — divide the analyzed timeline by a known execution-rate factor Checked 2026-10-15 against paper ishii2021compositional: full comparison completed; metadata and unsupported claims reviewed; experiments not reproduced

Last edited: