SubSystemSpec: Parametric Subsystem Abstraction (Kripke-Generalized)

StructuralSpec（構造）、BehavioralSpec（行動）、 FDIRBundle（FDIR の証明束）、およびこれら3つを統合した SubSystemSpec を定義する。

B-7: SubSystemSpec / BehavioralSpec の Kripke 一般化

B-6 で FDIRBundle を ToKripke α S D ベースに統一したのに続き、B-7 で BehavioralSpec と SubSystemSpec も同様に ToKripke α S D ベースに 一般化した。これにより以下が同一型の構造として扱える:

• SubSystemSpec sm — 単一サブシステム仕様（sm : StateMachine S D inv）
• SubSystemSpec psm — 合成サブシステム仕様（psm : ProductStateMachine sm₁ sm₂）

合成（2機合成、ネストにより N 機）は VV/ProductFDIR.lean の SubSystemSpec.compose で提供する。

破壊的変更 (A 案)

B-7 は A 案 を採用している。旧 API:

def epsBehavioral : BehavioralSpec EPSMode Nat epsGlobalInv :=
  { sm := epsSM, wellFormed := epsSM_WellFormed }
def epsSpec : SubSystemSpec EPSMode Nat epsGlobalInv := ...

新 API:

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

BehavioralSpec の wellFormed : sm.WellFormed フィールドは nonEmpty : (toKripke x).NonEmpty に変わる。StateMachine.WellFormed.nonEmpty で変換可能。合成時に必要な強い WellFormed は SubSystemSpec.compose に 明示引数として渡す（FDIRBundle.compose と一貫）。

structure VerifiedMBSE.VV.StructuralSpec : Type

StructuralSpec: サブシステムの構造的側面。

• name : String

  サブシステム名

• parts : List Core.PartDef

  part 定義のリスト

• connectors : List Core.Connector

  connector のリスト

• system : Core.System

  System

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

  system.parts との整合性

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

  system.connectors との整合性

• wellFormed : self.system.WellFormed

  構造的 well-formedness

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

StructuralSpec のスマートコンストラクタ。

Equations

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

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

全 part 不変条件が成立する命題。

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

BehavioralSpec: サブシステムの行動的側面（Kripke 一般化版）。

ToKripke α S D 型クラス経由で意味論が与えられるため、x : α として StateMachine S D inv や ProductStateMachine sm₁ sm₂ を渡せる。

nonEmpty フィールドは Kripke 構造としての非空性（到達可能な (s, d) が存在する）。StateMachine sm の場合は sm.WellFormed から StateMachine.WellFormed.nonEmpty で変換可能。

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

  Kripke 構造としての非空性: 到達可能な (s, d) が存在する。

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

FDIRBundle: FDIR 要件の証明束（統一版、B-6）。

ToKripke α S D 型クラス経由で意味論が与えられるため、x : α として StateMachine S D inv や ProductStateMachine sm₁ sm₂ を直接渡せる。

• FDIRBundle sm (sm : StateMachine S D inv) — 単一サブシステムの FDIR
• FDIRBundle psm (psm : ProductStateMachine sm₁ sm₂) — 合成サブシステムの FDIR

合成された FDIRBundle の構築方法は VV/ProductFDIR.lean の FDIRBundle.compose を参照。

• isFault : S → Prop

  fault 状態の述語

• isRecovery : S → Prop

  recovery 状態の述語

• isSafe : D → Prop

  データの safety 条件

• 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

FDIRBundle から FDIRSpec への変換（StateMachine 特化）。

FDIRSpec は現状 StateMachine 上にのみ定義されているため、この変換は StateMachine 版の FDIRBundle に対してのみ意味を持つ。積状態機械上の FDIRBundle は .isFault / .safety 等のフィールドを直接利用すればよい。

Equations

• ⋯ = ⋯

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

SubSystemSpec: 構造・行動・FDIR を統合したサブシステム仕様（Kripke 一般化版）。

ToKripke α S D 型クラスを通して、StateMachine 版と ProductStateMachine 版を同一構造で扱える。合成は SubSystemSpec.compose (VV/ProductFDIR.lean) で提供。

新しいサブシステムの追加はこの型の 1 インスタンスの構成で完結する。

• structural : StructuralSpec

  構造仕様

• behavioral : BehavioralSpec x

  行動仕様

• fdir : FDIRBundle x

  FDIR 証明束

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

サブシステム名。

Equations

• spec.name = spec.structural.name

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

System を取得する。

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

StateMachine を取得する（StateMachine 特化）。

一般化された SubSystemSpec では x : α なので、StateMachine を 取り出せるのは x : StateMachine S D inv のケースのみ。この版では x 自身がそのまま StateMachine として返される。

Equations

• _spec.stateMachine = sm

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

Consistent: 構造側 WellFormed かつ 行動側 NonEmpty。

旧 API の spec.structural.system.WellFormed ∧ spec.behavioral.sm.WellFormed は、Kripke 一般化後は後者が NonEmpty に弱まる。StateMachine 版では 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

FDIRSpec の自動導出（StateMachine 特化）。

FDIRSpec は StateMachine 特化なので、x : StateMachine S D inv の ケースのみ対応。一般化された SubSystemSpec の他のインスタンス化では 代わりに spec.fdir.safety 等の直接アクセスを使う。

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

サブシステムレベルの VVRecord（S1-WellFormed）。

ev は対応する検証命題 spec.structural.system.WellFormed に対する ValidationEvidence。デフォルトは .trusted spec.structural.wellFormed。

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

システムレベルの VVRecord（R1 Safety）。

ev は Always x (fun _ d => spec.fdir.isSafe d) に対する ValidationEvidence。デフォルトは .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

システムレベルの VVRecord（R3 Recovery）。

ev は Leads 命題に対する ValidationEvidence。 デフォルトは .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

2 つのサブシステムを構造的に合成する。

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

合成後の part 数は各サブシステムの part 数の和に一致する。