Towards Verification of Constituent Systems through Automated Proof

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

purpose and architecture

The paper presents two Symphony plugins for proving contractual properties of constituent systems (CSs) in a System of Systems: a Proof Obligation Generator (POG) and a Theorem Prover Plugin (TPP). Its abstract states, “To support verification of these obligations we have developed a proof obligation generator and theorem prover plugin for Symphony.” (abstract, p. 1) The TPP translates CML model obligations to Isabelle/HOL and attempts automated discharge; completed proof obligations are intended as evidence that a CS conforms to its contract.

CML models stateful reactive processes, types, functions, channels, operations, and CSP-style concurrent actions. Symphony’s semantic stack gives CML a UTP denotational, operational, and axiomatic foundation; the POG generates obligations and the TPP uses a visitor to translate the CML abstract syntax tree into Isabelle definitions (§II, pp. 1–2). Isabelle’s LCF architecture ensures proofs are correct with respect to a secure logical core (§II–III, p. 2); auto, sledgehammer, and nitpick are Isabelle facilities named in §III (p. 2), and cml tac is the CML-specific tactic that maps a CML formula onto a HOL formula (§IV, p. 3). At the time of writing only cml tac is available in the Proof Session, and exposing sledgehammer and nitpick in the TPP is future work (§IV, p. 4; §VI, p. 6).

generating proof obligations

The POG categorizes goals as safe use of partial operators, safe use of functions with preconditions, type compatibility for unions, invariants and subtypes, and satisfiability of implicitly defined functions and operations (§IV, p. 2). The POG generates, for a CML document, proof goals for high-level properties such as internal consistency, contractual correctness of operations, and termination (§II, p. 2). The authors say: “The TPP can then be used to attempt discharge of these proof obligations, resulting in concrete proof objects for the properties.” (§II, p. 2)

The division example shows the repair loop. For division(x,y) == x / y, the POG initially generates forall x:int, y:int & (y <> 0), which the paper calls “not satisfiable”, so discharge fails (§IV, p. 3). Adding the precondition pre y <> 0 to the function lets the revised obligation be discharged. The call divby2(x) == division(x,2) then creates a separate precondition obligation forall x : int & pre_division(x,2), generated at all points in the model where the function is called (§IV, p. 3). Inference: the workflow is therefore to generate an obligation; inspect a failed formula; strengthen the function precondition or add a guard; regenerate; discharge the revised formula; and check every caller obligation.

Inference: In Verus, use requires for the divisor condition, ensures for the result, and call-site proof obligations generated by Verus when invoking the function. A failed call obligation is repaired by proving the required precondition in the caller, not by weakening the callee contract. Verus spec fn and proof functions can express mathematical division conditions, while executable division still needs an appropriate Rust type and runtime behavior.

translation and automated discharge

The TPP is a deep embedding of CML in Isabelle/UTP: “we give an explicit semantics to each of the operators of CML processes within Isabelle” (§IV, p. 3). It translates a CML model and its POs into Isabelle theory files. The paper says, “These theory files can then be submitted to Isabelle for discharging through various automated proof tactics such as auto and sledgehammer, or the cml tac tactic that maps a CML formula onto a HOL formula.” (§IV, p. 3) In the fully automated mode users choose which PO to discharge and tactic selection and result collection are hidden; users who know Isabelle can instead write and discharge model-specific conjectures directly (§IV, p. 3).

The authors “envisage” two functionalities, Quick check and Proof Session (§IV, p. 3), described in the future tense. Quick check is a fully automated process that lists POs, with their predicates, linked to model elements; each PO can be read as a possible inconsistency that guides the user to add preconditions or guards (§IV, pp. 3–4). Proof Session creates a timestamped read-only snapshot of the CML sources, generates POs, translates the model and POs into Isabelle theories, lets the user submit POs for discharge, and stores the results with the snapshot (§IV, pp. 3–4). The paper states that each set of POs and proofs “are only valid for the particular version of the model they were generated from” (§IV, p. 4).

Inference: A Verus integration should generate a stable proof target from a versioned Rust module, retain the exact source and dependency versions, and rerun obligations after edits. Verus checks the resulting Rust contracts directly; an external translator would add a trusted semantic boundary comparable to the CML-to-Isabelle translation.

constituent-system example

The paper models a railway Dwarf Signal CS with a DwarfType state record, a ProperState subtype (dark, stop, warning, drive), invariants such as NeverShowAll, MaxOneLampChange, ForbidStopToDrive, DarkOnlyToStop, and DarkOnlyFromStop, and operations Init, SetNewProperState, TurnOn, and TurnOff (§V, pp. 4–5). Init assigns mk_DwarfType(stop, {}, {}, stop, stop, stop) to the state variable dw and has a postcondition requiring lastproperstate, laststate, currentstate, and desiredproperstate to equal stop and turnoff and turnon to be empty. For Init the POG emits two subtype obligations (PO1, PO2) and a postcondition obligation (PO3) (§V, p. 5). The paper reports that the obligations shown for Init are discharged (Fig. 6, p. 5).

The authors say that discharging all POs would give “a contractual model which is verified to be both internally consistent and, through encoding the safety properties which must be met by a signal, is safe with respect to the requirements placed on that contract.” (§V, p. 5) However, the same section says “several are not” discharged: those POs that “rely upon the value of the Dwarf process state variable dw at a given point of time”. Possible causes given are that the VDM-based PO expressions “require further adaption to CML” or the “early stage of development of the TPP proof tactics” (§V, p. 5). The POG also does not handle the CML actions that dictate the ordering of internal events and operation calls, so they are omitted from the paper (§V, p. 5).

Inference: In Verus, encode the state record as a Rust struct with a representation invariant proved by a predicate, and prove each operation’s ensures preserves that predicate. Concurrent event ordering requires a Verus state-machine or other explicit transition model; a sequential struct invariant alone is insufficient.

evidence, trust, and limits

The paper provides architecture, proof-goal categories, formulas, a worked railway model, and screenshots of discharged and failed obligations. It reports no benchmark denominator, timing distribution, success percentage, or defect-detection rate. Its concrete evidence is a prototype and a small illustrative CS model. The authors propose as future work a more comprehensive calculus such as a Hoare logic or weakest precondition calculus, SoS-level obligations (invariants over the whole SoS, or composing verified constituent interfaces), a CS refinement tool that reuses the POG to enumerate refinement provisos, and exposing more native Isabelle facilities such as sledgehammer and nitpick (§VI, pp. 5–6). They also say the TPP is the first attempt at tightly integrating a theorem prover into the VDM family of tools and that both plug-ins are at an early development stage (§VI, pp. 5–6).

techniques for the catalog

• proof-obligation generation — enumerate partial-operator, precondition, subtype, invariant, postcondition, and satisfiability goals from a model
• contract repair by failed obligations — use an unsatisfied PO to add a guard or strengthen a precondition, then regenerate caller obligations
• semantic AST translation — deep-embed the model language and translate its AST and obligations into a theorem prover’s logic
• automated tactic discharge — invoke trusted-kernel tactics such as auto, sledgehammer, or a domain-specific tactic on generated theories
• versioned proof sessions — snapshot the model, regenerate obligations, discharge them, and retain proofs with the exact source version
• constituent invariant verification — prove each operation’s postcondition and subtype/invariant obligations for a stateful system model

Last edited: 2026-10-17