SubSystemSpec: Parametric Subsystem Abstraction (Kripke-Generalized)

This module defines StructuralSpec (structure), BehavioralSpec (behavior), FDIRBundle (FDIR proof bundle), and the integrated SubSystemSpec that combines all three.

Kripke generalization

BehavioralSpec, FDIRBundle, and SubSystemSpec are parameterized by a ToKripke α S D instance. This lets the same structures represent both single-machine and product-machine subsystems uniformly:

• SubSystemSpec sm — single-subsystem specification (sm : StateMachine S D inv)
• SubSystemSpec psm — composite-subsystem specification (psm : ProductStateMachine sm₁ sm₂)

Parallel composition (binary, nestable to N subsystems) is provided by SubSystemSpec.compose in VV/ProductFDIR.lean.

BehavioralSpec.nonEmpty instead of .wellFormed

BehavioralSpec x carries only nonEmpty : (ToKripke.toKripke x).NonEmpty — the Kripke-level non-emptiness of the reachable state–data set. This is the weakest condition that supports the Kripke semantics uniformly across StateMachine and ProductStateMachine.

For the StateMachine case the stronger sm.WellFormed implies NonEmpty via StateMachine.WellFormed.nonEmpty, so callers with a WellFormed proof in hand can always obtain a BehavioralSpec:

def epsBehavioral : BehavioralSpec epsSM :=
  { nonEmpty := epsSM_WellFormed.nonEmpty }
def epsSpec : SubSystemSpec epsSM := ...

Composition needs the full WellFormed strength; SubSystemSpec.compose takes it as an explicit argument, mirroring FDIRBundle.compose.

structure VerifiedMBSE.VV.StructuralSpec : Type

Structural aspect of a subsystem: parts, connectors, system, and a well-formedness proof.

• name : String

  Subsystem name.

• parts : List Core.PartDef

  List of part definitions.

• connectors : List Core.Connector

  List of connectors.

• system : Core.System

  Underlying System.

• system_eq_parts : self.system.parts = self.parts

  Consistency of system.parts with the top-level parts field.

• system_eq_connectors : self.system.connectors = self.connectors

  Consistency of system.connectors with the top-level connectors field.

• wellFormed : self.system.WellFormed

  Structural well-formedness of system.

def VerifiedMBSE.VV.StructuralSpec.mk' (name : String) (parts : List Core.PartDef) (connectors : List Core.Connector) (wf : { parts := parts, connectors := connectors }.WellFormed) : StructuralSpec

Smart constructor for StructuralSpec.

Builds system internally from the supplied parts and connectors, so the consistency fields (system_eq_parts, system_eq_connectors) are discharged by rfl.

Equations

• One or more equations did not get rendered due to their size.

def VerifiedMBSE.VV.StructuralSpec.allPartsInvariant (spec : StructuralSpec) : Prop

Proposition stating that every part invariant in spec holds.

Equations

• spec.allPartsInvariant = ∀ (p : VerifiedMBSE.Core.PartDef), p ∈ spec.parts → p.invariant

structure VerifiedMBSE.VV.BehavioralSpec {α S D : Type} [Behavior.ToKripke α S D] (x : α) : Prop

Behavioral aspect of a subsystem, generalized over any ToKripke α S D.

The type-class parameter [ToKripke α S D] supplies the Kripke semantics for x : α, so the same BehavioralSpec structure works for x : StateMachine S D inv and x : ProductStateMachine sm₁ sm₂.

The only field is nonEmpty, expressing Kripke-level non-emptiness (some reachable (s, d) exists). For x : StateMachine _ _ inv, StateMachine.WellFormed.nonEmpty converts the stronger sm.WellFormed into this field.

• nonEmpty : (Behavior.ToKripke.toKripke x).NonEmpty

  Kripke-level non-emptiness: some reachable (s, d) exists.

structure VerifiedMBSE.VV.FDIRBundle {α S D : Type} [Behavior.ToKripke α S D] (x : α) : Type

Proof bundle for FDIR (Fault Detection, Isolation, and Recovery) requirements, generalized over any ToKripke α S D.

Parameterizing by [ToKripke α S D] lets the same structure carry FDIR obligations for both single and composite subsystems:

• FDIRBundle sm where sm : StateMachine S D inv — single-subsystem FDIR
• FDIRBundle psm where psm : ProductStateMachine sm₁ sm₂ — composite FDIR

Construction of a composite FDIRBundle from two component bundles is provided by FDIRBundle.compose in VV/ProductFDIR.lean.

• isFault : S → Prop

  Predicate characterizing fault states.

• isRecovery : S → Prop

  Predicate characterizing recovery states.

• isSafe : D → Prop

  Safety predicate on data.

• safety : Behavior.Always x fun (x_1 : S) (d : D) => self.isSafe d

  R1 — Safety: □ (isSafe d).

• detection : Behavior.Eventually x fun (s : S) (x_1 : D) => self.isFault s

  R2 — Fault detection: ◇ (isFault s).

• recovery : Behavior.Leads x (fun (s : S) (x_1 : D) => self.isFault s) fun (s : S) (x_1 : D) => self.isRecovery s

  R3 — Fault recovery: □ (isFault ⇒ ◇ isRecovery).

def VerifiedMBSE.VV.FDIRBundle.toFDIRSpec {S D : Type} {inv : S → D → Prop} {sm : Behavior.StateMachine S D inv} (bundle : FDIRBundle sm) : Behavior.FDIRSpec sm bundle.isFault bundle.isRecovery bundle.isSafe

Convert an FDIRBundle to an FDIRSpec (StateMachine specialization).

FDIRSpec is currently defined only over StateMachine, so this conversion is meaningful only when the bundle is over a StateMachine value. For FDIRBundle over a product machine, consume the fields (.isFault, .safety, etc.) directly.

Equations

• ⋯ = ⋯

structure VerifiedMBSE.VV.SubSystemSpec {α S D : Type} [Behavior.ToKripke α S D] (x : α) : Type

A full subsystem specification integrating structure, behavior, and FDIR, generalized over any ToKripke α S D.

Because all three components (StructuralSpec, BehavioralSpec x, FDIRBundle x) are uniform in x : α, the same SubSystemSpec type covers StateMachine and ProductStateMachine instances. Parallel composition is provided by SubSystemSpec.compose in VV/ProductFDIR.lean.

Adding a new subsystem amounts to constructing one value of this type.

• structural : StructuralSpec

  Structural specification.

• behavioral : BehavioralSpec x

  Behavioral specification.

• fdir : FDIRBundle x

  FDIR proof bundle.

def VerifiedMBSE.VV.SubSystemSpec.name {α S D : Type} [Behavior.ToKripke α S D] {x : α} (spec : SubSystemSpec x) : String

Subsystem name (drawn from the structural spec).

Equations

• spec.name = spec.structural.name

def VerifiedMBSE.VV.SubSystemSpec.system {α S D : Type} [Behavior.ToKripke α S D] {x : α} (spec : SubSystemSpec x) : Core.System

Underlying System (drawn from the structural spec).

Equations

• spec.system = spec.structural.system

def VerifiedMBSE.VV.SubSystemSpec.stateMachine {S D : Type} {inv : S → D → Prop} {sm : Behavior.StateMachine S D inv} (_spec : SubSystemSpec sm) : Behavior.StateMachine S D inv

Retrieve the underlying StateMachine (StateMachine specialization).

Because SubSystemSpec is parameterized over x : α, recovering a StateMachine is meaningful only when x : StateMachine S D inv. In that case x itself is the machine and is returned verbatim.

Equations

• _spec.stateMachine = sm

def VerifiedMBSE.VV.SubSystemSpec.Consistent {α S D : Type} [Behavior.ToKripke α S D] {x : α} (spec : SubSystemSpec x) : Prop

Combined consistency: structural System.WellFormed and behavioral Kripke NonEmpty.

The behavioral side is (ToKripke.toKripke x).NonEmpty — the weakest condition that uniformly covers StateMachine and ProductStateMachine. For StateMachine instances this is derivable from the full sm.WellFormed via StateMachine.WellFormed.nonEmpty.

Equations

• spec.Consistent = (spec.structural.system.WellFormed ∧ (VerifiedMBSE.Behavior.ToKripke.toKripke x).NonEmpty)

theorem VerifiedMBSE.VV.SubSystemSpec.fdir_derivable {S D : Type} {inv : S → D → Prop} {sm : Behavior.StateMachine S D inv} (spec : SubSystemSpec sm) : Behavior.FDIRSpec sm spec.fdir.isFault spec.fdir.isRecovery spec.fdir.isSafe

Automatic derivation of FDIRSpec (StateMachine specialization).

FDIRSpec is defined only for StateMachine, so this derivation applies only to x : StateMachine S D inv. For other instances, use the spec.fdir fields (.safety, .detection, .recovery) directly.

def VerifiedMBSE.VV.SubSystemSpec.subsystemRecord {α S D : Type} [Behavior.ToKripke α S D] {x : α} (spec : SubSystemSpec x) (ev : ValidationEvidence spec.structural.system.WellFormed := ValidationEvidence.trusted ⋯) : VVRecord

Subsystem-level VVRecord for the S1-WellFormed property.

ev is the ValidationEvidence attached to spec.structural.system.WellFormed; it defaults to .trusted spec.structural.wellFormed. Pass .contract or .confidence explicitly to select a different evidence layer.

Equations

• One or more equations did not get rendered due to their size.

def VerifiedMBSE.VV.SubSystemSpec.safetyRecord {α S D : Type} [Behavior.ToKripke α S D] {x : α} (spec : SubSystemSpec x) (ev : ValidationEvidence (Behavior.Always x fun (x_1 : S) (d : D) => spec.fdir.isSafe d) := ValidationEvidence.trusted ⋯) : VVRecord

System-level VVRecord for the R1-Safety property.

ev is the ValidationEvidence attached to Always x (fun _ d => spec.fdir.isSafe d); it defaults to .trusted spec.fdir.safety.

Equations

• One or more equations did not get rendered due to their size.

def VerifiedMBSE.VV.SubSystemSpec.recoveryRecord {α S D : Type} [Behavior.ToKripke α S D] {x : α} (spec : SubSystemSpec x) (ev : ValidationEvidence (Behavior.Leads x (fun (s : S) (x_1 : D) => spec.fdir.isFault s) fun (s : S) (x_1 : D) => spec.fdir.isRecovery s) := ValidationEvidence.trusted ⋯) : VVRecord

System-level VVRecord for the R3-Recovery property.

ev is the ValidationEvidence attached to the Leads proposition; it defaults to .trusted spec.fdir.recovery.

Equations

• One or more equations did not get rendered due to their size.

def VerifiedMBSE.VV.StructuralSpec.compose (s1 s2 : StructuralSpec) (bridge : List Core.Connector) (hbridge : ∀ (c : Core.Connector), c ∈ bridge → c.source.part ∈ s1.system.parts ++ s2.system.parts ∧ c.target.part ∈ s1.system.parts ++ s2.system.parts) : StructuralSpec

Parallel structural composition of two StructuralSpecs with an optional list of inter-subsystem bridge connectors.

bridge carries connectors whose endpoints cross between s1 and s2; hbridge witnesses that each endpoint resides in the concatenation of the two operand part lists.

Equations

• One or more equations did not get rendered due to their size.

theorem VerifiedMBSE.VV.StructuralSpec.compose_parts_length (s1 s2 : StructuralSpec) (bridge : List Core.Connector) (hbridge : ∀ (c : Core.Connector), c ∈ bridge → c.source.part ∈ s1.system.parts ++ s2.system.parts ∧ c.target.part ∈ s1.system.parts ++ s2.system.parts) : (s1.compose s2 bridge hbridge).parts.length = s1.system.parts.length + s2.system.parts.length

The composed part count equals the sum of the operand part counts.