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 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 authors state: “Our objective is not to develop a complete set of requirements, but to gain insights into the modeling process and to identify research directions to address some of the gaps we have encountered in our work.” (Section I, p.2 of the 10-page arXiv PDF). The case study uses a route generator (RG), a trajectory generator (TG), a combined component TTES (the paper never expands this acronym), a trajectory follower (TF), an environment (ENV), and a state estimator (SE); TES is the subsystem that remains after TG is split off TTES (Section IV, Fig. 3, pp.5, 7). The paper models two views: “a protocol view that describes the possible sequences of events in the system, and a functional view that describes the properties of the data exchanged among components.” (Section I, p.2).

Paper’s methodology (assembled from Sections II.A, IV and V, pp.3–9; the numbering is mine): (1) decompose decision making into layers “to limit the complexity of the DM problem”, here route generation, trajectory generation and trajectory following; (2) model each capability by assumptions on its goals and environment and guarantees on its decisions; (3) split the model into views, with a specification language and tool per view (PLTL for protocols, many-sorted first-order logic for data); (4) check refinement layer by layer: first {C_RG, C_TTES} ≤ C_AT, then {C_TES, C_TG} ≤ C_TTES, then {C_TF, C_ENV, C_SE} ≤ C_TES (Section IV, p.5); (5) elicit the properties of low-level control through an ontology (Conclusions, p.10). The paper motivates views thus: “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.” (Section I, p.2).

contract algebra

A contract is C=(A,G), with assumption A and guarantee G both specifications. The paper defines the 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.4). The environment semantics is the set of specifications refining A; the implementation semantics is the set of I with I ≤_A G. Contract C' refines C iff A ≤ A' and G' ≤_A G (and G' ≤ G in normal form). A normal-form (saturated) guarantee can, under some assumptions on the specification theory, be computed as G^nf = G ∧ ¬A. The paper follows the formalism of Bauer et al. [12] and cites Le et al. [15] for decomposition (p.4).

For a decomposition {C1,…,Cn} of parent C the paper requires (Equation 1, p.4): the conjunction of the children’s normal-form guarantees refines the parent guarantee G, and for each i, the parent assumption A conjoined with the other children’s normal-form guarantees refines A_i. The conjunction operator C1 ∧ C2 = (A1 ∨ A2, G1^nf ∧ G2^nf) combines views; the paper states that along a functional view Cf and a timing view Ct, {Cf', Cf''} ≤ Cf and {Ct', Ct''} ≤ Ct imply {C', C''} ≤ C (p.4). Its case study uses protocol and functional views, and it says it has “not formally combined the analyses from the protocol and functional views into one single contract” (Section IV.A, p.7). Inference: a Verus encoding could represent each contract as ghost predicates over state and environment inputs, with requires for assumptions, ensures for guarantees, and a proof fn per refinement implication; the paper gives no such encoding.

protocol-view verification

Use past-time linear temporal logic (PLTL) to specify event ordering. Define φ_er = (r ⇒ X^-1(¬r S e)), meaning a response r is generated only for an event e. The RG protocol contract (Eq. 2, pp.5–6) assumes: after a takeoff command to, no new to arrives until the previous one completes (2a); TTES eventually responds to rt with rt_d and issues rt_d only after a past rt (2b). It guarantees that to_d is issued after (and only after) rt_d (2c) and rt is issued after (and only after) to (2d); the formulas also include G(to ⇒ F rt) and G(rt_d ⇒ F to_d). TTES assumes nothing (A = ⊤) and guarantees to respond only to route requests. The top-level contract is A_AT = G(to ⇒ X(¬to U to_d)), G_AT = G(to ⇒ F to_d). The paper says the contracts “can be modeled in OCRA which” can automatically check whether {C_RG, C_TTES} refines C_AT (p.6). The models are at https://github.com/alessandro-pinto/icaa2023models (footnotes, pp.5–6). The paper does not report the outcome of the OCRA run.

functional-view modeling

The functional view uses many-sorted first-order logic (MS-FOL) to capture data properties. The paper defines roadmaps rm=(N,L) as graphs with node coordinates and labels (gate, takeoff, connection point, hold short), link lengths, routes as link sequences with dst(l_i)=src(l_{i+1}), and motion primitives for trajectories (Section IV.A, p.6). The three top-level requirements are: follow the centerline, stop short of hold-short lines, and stay below maximum velocity and acceleration; only the first is formalized, as G_AT^(cl) within a ball of radius δ (Eq. 3, p.6). For solver input, Node, Link, Roadmap, Route and Trj become types, src, linkAt, length and intg become functions, and InN, InL, InBall and ExistRt become predicates (pp.6–7). Background axioms are added only when the proof needs them: “this is needed only if the solution to our verification problem depends on such properties” (p.6); here two axioms are needed, monotonicity of InBall in the radius and symmetry (p.6). The RG contract (unnumbered, pp.6–7) assumes a valid roadmap, n̂ and to in the roadmap, and a non-empty set of routes; it guarantees a route starting at n̂, ending at to, with consecutive links connected and each link in the roadmap. The paper does not require RG to find the best route (footnote 5). The TTES contract (Eq. 4, p.7) assumes a valid route and guarantees that for every link and every distance p along it there is a time t with p = intg(t) and the pose ξ(t) within δ of the primitive. The paper then says: “We can now use an SMT solver to check the refinement between the specification and the composition of RG and T T ES” (p.7; the paper’s spacing), with the model at AT/function/AT.smt2 in the paper’s repository. It names z3 and cvc5 as well-supported provers (p.6), but does not say which solver was run or report a result.

parameterized and inductive refinement

For TTES the number of hold-short locations n_h is a parameter, giving n_h+1 trajectory segments (Section IV.B, p.7). The paper offers two options: assume an upper bound and prove refinement for all n_h up to it, “feasible if the upper bound is known and small”, or use induction: “(1) refinement holds for n_h = 0 and (2) assuming that it holds for n_h ≥ 0, then it holds for n_h + 1” (p.7). The inductive scheme (Fig. 4, p.8) uses a generic TG component with input i and output o, and chains instances by connecting one’s output to the next one’s input. For n=0 the system {C_TG0, C_TES, C_∨} refines C_TTES0, where C_∨ accepts all environments and outputs the disjunction of its inputs; the inductive step shows {C_TTESn, C_TG(n+1), C_∨} refines C_TTES(n+1) (p.8). For the functional view the paper argues that TES guarantees at the end of a segment (zero velocity, bounded state-estimate error) satisfy TES’s initial-state assumptions for the next segment, so “an inductive argument can be used” (p.8). It describes this only in prose; it gives no checked inductive proof. Inference: in Verus, one could encode segment composition as a recursive ghost predicate with a base lemma and an inductive lemma using decreases, and carry the segment invariant in concrete loops with invariant.

The paper also gives a control-level functional model (p.8): the trajectory follower assumes the environment behaves as a simple car with uncertain length bounds and a state estimate within δ_o, and guarantees closed-loop error δ_c; the state estimator guarantees bounded error; an additional axiom composes errors (InBall(p1,p2,δ1) ∧ InBall(p2,p3,δ2) ⇒ InBall(p1,p3,δ1+δ2)). It suggests an ontology of environments and properties in MS-FOL instead of differential dynamic logic or KeYmaera for requirement elicitation (p.8).

uncertainty and evidence

For imperfect implementations such as neural perception (the example is a network estimating cross-track error from images, as in TaxiNet), the paper says an implementation may satisfy its contract only probabilistically, P≥α(I_i ⊗ A_i ≤ G_i), and that “such implementation uncertainty must be propagated through the refinement chain to compute the probability that the top-level requirements are satisfied” (Section IV.C, p.9). It leaves the formal definition aside (footnote 11, “Due to the lack of space”) and proposes no propagation method. The paper lists six research needs in the abstract: heterogeneous-composition semantics, model libraries, lifting verification results to the specification level, probabilistic contracts, standard functional architectures, and a theory of higher-order contracts. It reports a worked model and solver encodings but no benchmark population, runtime, or success denominator, and it does not report the outcome of the refinement checks. The authors caution that “The modeling effort, even for a simplified system, is generally high.” (Section IV.A, p.7). Section IV.D (pp.9–10) adds that relaxing requirements, for example allowing unforeseen obstacles, may force radical architecture changes and “a complete model re-development cycle”.

techniques for the catalog

• layered contract decomposition: split an autonomous system into components and views, each with assumptions and guarantees (shown, Section IV)
• refinement checking: prove child contract composition refines parent guarantees and respects assumptions (Equation 1; protocol check via OCRA, functional check via an SMT solver; results not reported)
• heterogeneous formalization: use PLTL for event protocols and many-sorted first-order logic for data and geometry (shown; their combination into one contract is left as future work)
• parameter induction: base case plus inductive extension over a chain of generic TG components for arbitrarily many segments (sketched in prose)
• uncertainty propagation: a stated need only; attach satisfaction probabilities P≥α to implementations and carry them through refinement (not developed in the paper)

Last edited: 2026-10-18