State Machine: Dependently Typed Behavioral Model

Defines Transition (with invariant preservation embedded as a type-level proof), StateMachine, the inductive proposition Reachable, and the safety theorem Reachable.inv_holds.

Key Design Decision

Embedding invariant preservation in Transition.preserves makes transitions that violate the invariant unconstructible (type error).

structure VerifiedMBSE.Behavior.Transition (S D : Type) (inv : S → D → Prop) : Type

Transition: transition defined over control state S and data type D. The preserves field guarantees invariant preservation at the type level.

• source : S

  Source control state

• target : S

  Target control state

• guard : D → Prop

  Guard condition

• effect : D → D

  Effect (data transformation)

• preserves (d : D) : self.guard d → inv self.source d → inv self.target (self.effect d)

  Type-level contract for invariant preservation

structure VerifiedMBSE.Behavior.StateMachine (S D : Type) (inv : S → D → Prop) : Type

StateMachine: state machine consisting of an initial state and a list of transitions.

• initialState : S

  Initial control state

• transitions : List (Transition S D inv)

  List of transitions

def VerifiedMBSE.Behavior.StateMachine.WellFormed {S D : Type} {inv : S → D → Prop} (sm : StateMachine S D inv) : Prop

Well-formedness of StateMachine: data satisfying the invariant exists in the initial state.

Equations

• sm.WellFormed = ∃ (d₀ : D), inv sm.initialState d₀

inductive VerifiedMBSE.Behavior.Reachable {S D : Type} {inv : S → D → Prop} (sm : StateMachine S D inv) : S → D → Prop

Reachable: inductive proposition for reachable (control state, data value) pairs. Tracking both enables induction for inv_holds.

• init {S D : Type} {inv : S → D → Prop} {sm : StateMachine S D inv} (d₀ : D) : inv sm.initialState d₀ → Reachable sm sm.initialState d₀

  The initial state is reachable

• step {S D : Type} {inv : S → D → Prop} {sm : StateMachine S D inv} {s : S} {d : D} (t : Transition S D inv) : Reachable sm s d → t ∈ sm.transitions → t.source = s → t.guard d → Reachable sm t.target (t.effect d)

  The next state is reachable via a transition

theorem VerifiedMBSE.Behavior.Reachable.inv_holds {S D : Type} {inv : S → D → Prop} {sm : StateMachine S D inv} {s : S} {d : D} (h : Reachable sm s d) : inv s d

Safety theorem: all reachable pairs satisfy the invariant. Directly provable by induction since Transition.preserves is embedded in the type.

theorem VerifiedMBSE.Behavior.StateMachine.initial_inv_holds {S D : Type} {inv : S → D → Prop} {sm : StateMachine S D inv} (hwf : sm.WellFormed) : ∃ (d : D), inv sm.initialState d

The initial state of a WellFormed state machine has data satisfying the invariant.