Leveraging Compositional Methods for Modeling and Verification of an Autonomous Taxi System

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

objective and decomposition

The paper models and verifies an autonomous aircraft taxi system with contract-based composition. The abstract says: “We apply a compositional formal modeling and verification method to an autonomous aircraft taxi system.” (Abstract, p.1). The case study separates route generation (RG), trajectory generation (TG), trajectory execution (TTES), trajectory following (TF), environment (ENV), and state estimation (SE). The system is viewed through a protocol view (event ordering) and a functional view (data and physical properties) (Sections II and IV, pp.1–4).

Apply the methodology by (1) decomposing decision making into layers to limit complexity; (2) assigning each component an assumption/guarantee contract; (3) choosing a specification theory for each view (PLTL for protocols and many-sorted first-order logic for data); (4) composing contracts within and across views; (5) checking refinement at each layer with an automated solver; and (6) repeating until low-level control and environment contracts are reached. The paper explicitly motivates this: “The decomposition of a model into different views offers a way to decompose the modeling and verification problem into sub-problems that can be efficiently addressed using different domain-specific tools.” (Introduction, p.2)

contract algebra

A contract is C=(A,G), with assumption A describing permitted environments and guarantee G describing implementation behavior. An implementation refines a contract when it satisfies G under A; contract refinement is checked by comparing assumptions and guarantees. Parallel composition combines components, and conjunction combines different views. The paper defines the contract pair directly: “Specifically, a contract is a pair C = (A, G) where A and G are specifications called assumption and guarantee, respectively.” (Section III.A, p.3).

For a decomposition {C1,…,Cn} of parent C, require the conjunction of normalized child guarantees to refine the parent guarantee and the parent assumption conjoined with the other children’s guarantees to refine each child assumption (Equation 1, p.3). Procedure: (1) normalize contracts when assumptions can be folded into guarantees; (2) calculate child parallel composition; (3) check implementation and environment refinement; (4) use conjunction to combine functional and timing contracts; (5) retain a refinement proof for each edge. Inference: a Verus encoding would represent each contract as ghost predicates over state and environmental inputs, with requires for assumptions, ensures for guarantees, and a proof fn for each refinement implication.

protocol-view verification

Use past-time linear temporal logic (PLTL) to specify event ordering. For example, the route generator assumes that after a takeoff command no new command arrives until completion, that TTES eventually responds to a route request, and that responses are not spontaneous; it guarantees route and completion events occur in the required order (Section IV.A, Eq. 2, p.4). Encode each component’s assumptions and guarantees as PLTL formulas, then ask OCRA to check {C_RG, C_TTES} ≤ C_AT (p.4). This is a compositional check: if the child contracts refine the parent autonomous-taxi contract, the protocol layer is correct under the declared environment.

functional-view modeling

Represent roadmaps, routes, trajectories, and poses in many-sorted first-order logic. Define types (Node, Link, Roadmap, Route, Traj), functions such as src, dst, length, linkAt, and predicates such as InN, InL, and InBall (Section IV.A, pp.4–5). Add only background axioms needed by the proof, including monotonicity and symmetry of InBall. The route-generator contract assumes a valid roadmap, valid endpoints, and an existing route; its guarantee states that each route link is connected and belongs to the roadmap (Eq. 3, p.5). The TTES contract assumes a valid route and guarantees that every route position has a time whose aircraft pose lies within error radius δ of the prescribed trajectory (Eq. 4, p.5). Encode these formulas in SMT-LIB and use Z3 or cvc5 to check refinement (p.5).

When the number of hold-short segments n_h is variable, either bound it and check every n_h or prove an induction. The paper’s inductive method is: establish refinement for n_h=0; assume refinement for n_h≥0; show that adding one trajectory-generator instance yields refinement for n_h+1 (Section IV.B, pp.5–6). Chain generic TG components so each segment’s completion satisfies the next segment’s initial-state assumptions. Apply the same induction to the functional trajectory vector. Inference: in Verus, encode segment composition as a recursive ghost predicate and prove a base lemma plus an inductive lemma using decreases; concrete Rust loops then carry the segment invariant with invariant.

uncertainty and evidence

For imperfect implementations such as neural perception, model satisfaction probabilistically: a component may satisfy I_i ⊗ A_i ≤ G_i only with probability at least α, and that probability must propagate through the refinement chain (Appendix C, p.7). The paper identifies six research gaps: heterogeneous-contract semantics, model libraries, lifting solver results to specifications, probabilistic contracts, robust architectures, and higher-order contracts (Abstract and Sections IV–V). It reports a worked model and solver encodings but no benchmark population, runtime, or success denominator. Trusted parts are the specification semantics, background axioms, SMT solver, and translation from model formulas to solver input. The authors caution that “The modeling effort, even for a simplified system, is generally high.” (Section IV.A, p.5). Inference: threat to agent-written verified Rust is high for cross-component assumptions and sensor uncertainty; Verus can discharge local refinement but does not supply PLTL model checking, probabilistic contract composition, or solver-result traceability. VL should reuse layered contracts and inductive segment proofs rather than rebuild this decomposition.

techniques for the catalog

layered contract decomposition: split an autonomous system into components and views, each with assumptions and guarantees
refinement checking: prove child contract composition refines parent guarantees and respects assumptions
heterogeneous formalization: use PLTL for event protocols and many-sorted first-order logic for data and geometry
parameter induction: prove a base component chain and an inductive extension for arbitrarily many segments
uncertainty propagation: attach satisfaction probabilities to implementations and carry them through refinement Checked 2026-10-15 against paper pinto2023compositional: full comparison completed; metadata and unsupported claims reviewed; experiments not reproduced

Last edited: 2026-10-15

Steven Hé (Sīchàng)