Requirement Refinement and Design Equivalence

Defines DesignEquiv (Univalence-like principle) and RequirementRefinement (requirement refinement chains as path spaces).

def VerifiedMBSE.Equivalence.DesignEquiv (a b : Core.PartDef) : Prop

DesignEquiv: equivalence in the design space. Semantic wrapper around ComponentEquiv.

Equations

• VerifiedMBSE.Equivalence.DesignEquiv a b = VerifiedMBSE.Equivalence.ComponentEquiv a b

theorem VerifiedMBSE.Equivalence.designEquiv_preserves_invariant {a b : Core.PartDef} (h : DesignEquiv a b) : a.invariant ↔ b.invariant

Univalence-like principle: design equivalence preserves invariants.

theorem VerifiedMBSE.Equivalence.designEquiv_preserves_substitutable {a b : Core.PartDef} (h : DesignEquiv a b) : Substitutable a b

Design equivalence implies substitutability.

structure VerifiedMBSE.Equivalence.RequirementRefinement : Type

RequirementRefinement: requirement refinement relation. MBSE version of HoTT path spaces. Refinement: refined → original (a stronger requirement implies the original).

• original : Prop

  Original requirement

• refined : Prop

  Refined requirement

• refines : self.refined → self.original

  Refinement relation

def VerifiedMBSE.Equivalence.RequirementRefinement.compose (r₁₂ r₂₃ : RequirementRefinement) (h : r₁₂.refined = r₂₃.original) : RequirementRefinement

Composition of refinement chains (path composition).

Equations

• r₁₂.compose r₂₃ h = { original := r₁₂.original, refined := r₂₃.refined, refines := ⋯ }

def VerifiedMBSE.Equivalence.RequirementRefinement.id (P : Prop) : RequirementRefinement

Identity refinement (reflexivity path).

Equations

• VerifiedMBSE.Equivalence.RequirementRefinement.id P = { original := P, refined := P, refines := ⋯ }

def VerifiedMBSE.Equivalence.voltage_refinement : RequirementRefinement

Voltage requirement refinement: v ≤ 500 ⊑ v ≤ 1000

Equations

• VerifiedMBSE.Equivalence.voltage_refinement = { original := 150 ≤ 1000, refined := 150 ≤ 500, refines := VerifiedMBSE.Equivalence.voltage_refinement._proof_2 }

def VerifiedMBSE.Equivalence.voltage_refinement₂ : RequirementRefinement

Stricter refinement: v ≤ 200 ⊑ v ≤ 500

Equations

• VerifiedMBSE.Equivalence.voltage_refinement₂ = { original := 150 ≤ 500, refined := 150 ≤ 200, refines := VerifiedMBSE.Equivalence.voltage_refinement₂._proof_2 }

def VerifiedMBSE.Equivalence.voltage_refinement_composed : RequirementRefinement

Composed refinement: v ≤ 200 ⊑ v ≤ 1000

Equations

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