FDIR Specification and StateMachineComponent

Defines FDIRSpec (a bundle of safety, detection, and recovery requirements) and StateMachineComponent, which integrates structural (PartDef) and behavioral (StateMachine) models into a single verified component.

Note on Import

StateMachineKripke をインポートする理由: Always sm P / Eventually sm P / Leads sm P Q の形の呼び出しが、KripkeStructure 版 LTL API に StateMachine → KripkeStructure の coerce 経由で流れるようにするため。

structure VerifiedMBSE.Behavior.FDIRSpec {S D : Type} {inv : S → D → Prop} (sm : StateMachine S D inv) (isFault isNominal : S → Prop) (isSafe : D → Prop) : Prop

FDIRSpec: structure bundling three FDIR requirements. Constructing a value of this type = mechanized verification of all FDIR requirements.

• safety : Always sm fun (x : S) (d : D) => isSafe d

  R1 Safety: □(isSafe d)

• detection : Eventually sm fun (s : S) (x : D) => isFault s

  R2 Fault detectability: ◇(isFault s)

• recovery : Leads sm (fun (s : S) (x : D) => isFault s) fun (s : S) (x : D) => isNominal s

  R3 Fault recoverability: □(isFault s → ◇(isNominal s'))

def VerifiedMBSE.Behavior.SMInvariantCompatible (pd : Core.PartDef) (S : Type) (I : Core.Interpretation) (inv : S → I pd.baseType → Prop) : Prop

SMInvariantCompatible: the state machine invariant implies the PartDef invariant. Consistency condition between structural and behavioral models.

Equations

• VerifiedMBSE.Behavior.SMInvariantCompatible pd S I inv = ∀ (s : S) (d : I pd.baseType), inv s d → pd.invariant

structure VerifiedMBSE.Behavior.StateMachineComponent (I : Core.Interpretation) (pd : Core.PartDef) (S : Type) (inv : S → I pd.baseType → Prop) : Type

StateMachineComponent: component that adds state machine behavior to a PartDef.

• compat : SMInvariantCompatible pd S I inv

  Consistency proof

• sm : StateMachine S (I pd.baseType) inv

  State machine governing the behavior

def VerifiedMBSE.Behavior.StateMachineComponent.WellFormed {I : Core.Interpretation} {pd : Core.PartDef} {S : Type} {inv : S → I pd.baseType → Prop} (smc : StateMachineComponent I pd S inv) : Prop

Consistency condition for StateMachineComponent.

Equations

• smc.WellFormed = smc.sm.WellFormed

def VerifiedMBSE.Behavior.StateMachineComponent.reachable_gives_instance {I : Core.Interpretation} {pd : Core.PartDef} {S : Type} {inv : S → I pd.baseType → Prop} (smc : StateMachineComponent I pd S inv) {s : S} {d : I pd.baseType} (hr : Reachable smc.sm s d) : Core.PartInstance I pd

Phase 2/3 connection theorem: construct a PartInstance from a reachable (state, data) pair.

Equations

• smc.reachable_gives_instance hr = { carrier := d, inv_holds := ⋯ }

noncomputable def VerifiedMBSE.Behavior.StateMachineComponent.wellFormed_gives_instance {I : Core.Interpretation} {pd : Core.PartDef} {S : Type} {inv : S → I pd.baseType → Prop} (smc : StateMachineComponent I pd S inv) (hwf : smc.WellFormed) : Core.PartInstance I pd

If WellFormed, a PartInstance exists.

Equations

• smc.wellFormed_gives_instance hwf = smc.reachable_gives_instance ⋯