Abstraction Levels and Design Parameters

Defines AbstractionLevel (MBSE analogue of n-truncation) and DesignParameter (discrete analogue of cubical structure).

inductive VerifiedMBSE.Equivalence.AbstractionLevel : Type

AbstractionLevel: design abstraction level. MBSE analogue of HoTT n-truncation.

• concept : AbstractionLevel

  Concept level: requirements only

• logical : AbstractionLevel

  Logical level: interface definitions

• physical : AbstractionLevel

  Physical level: concrete implementation

@[implicit_reducible]

instance VerifiedMBSE.Equivalence.instReprAbstractionLevel : Repr AbstractionLevel

Equations

• VerifiedMBSE.Equivalence.instReprAbstractionLevel = { reprPrec := VerifiedMBSE.Equivalence.instReprAbstractionLevel.repr }

def VerifiedMBSE.Equivalence.instReprAbstractionLevel.repr : AbstractionLevel → Nat → Std.Format

Equations

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

def VerifiedMBSE.Equivalence.instBEqAbstractionLevel.beq : AbstractionLevel → AbstractionLevel → Bool

Equations

• VerifiedMBSE.Equivalence.instBEqAbstractionLevel.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance VerifiedMBSE.Equivalence.instBEqAbstractionLevel : BEq AbstractionLevel

Equations

• VerifiedMBSE.Equivalence.instBEqAbstractionLevel = { beq := VerifiedMBSE.Equivalence.instBEqAbstractionLevel.beq }

@[implicit_reducible]

instance VerifiedMBSE.Equivalence.instDecidableEqAbstractionLevel : DecidableEq AbstractionLevel

Equations

• VerifiedMBSE.Equivalence.instDecidableEqAbstractionLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def VerifiedMBSE.Equivalence.AbstractionLevel.refines : AbstractionLevel → AbstractionLevel → Prop

Refinement relation between abstraction levels: lower refines upper.

Equations

• VerifiedMBSE.Equivalence.AbstractionLevel.physical.refines VerifiedMBSE.Equivalence.AbstractionLevel.logical = True
• VerifiedMBSE.Equivalence.AbstractionLevel.physical.refines VerifiedMBSE.Equivalence.AbstractionLevel.concept = True
• VerifiedMBSE.Equivalence.AbstractionLevel.logical.refines VerifiedMBSE.Equivalence.AbstractionLevel.concept = True
• x✝¹.refines x✝ = False

theorem VerifiedMBSE.Equivalence.AbstractionLevel.refines_trans {l₁ l₂ l₃ : AbstractionLevel} (h₁₂ : l₁.refines l₂) (h₂₃ : l₂.refines l₃) : l₁.refines l₃

Abstraction refinement is transitive.

structure VerifiedMBSE.Equivalence.DesignParameter (α : Type) : Type

DesignParameter: design parameter type. Discrete analogue of cubical structure.

• value : α

  Parameter value

• valid : α → Prop

  Valid range

• inRange : self.valid self.value

  Current value is within the valid range

def VerifiedMBSE.Equivalence.ParametricInvariant {α : Type} (param : DesignParameter α) (inv : α → Prop) : Prop

Parametric invariant: inv holds for all valid parameter values. Discrete analogue of cubical path Π(p : I). inv(p).

Equations

• VerifiedMBSE.Equivalence.ParametricInvariant param inv = ∀ (p : α), param.valid p → inv p

def VerifiedMBSE.Equivalence.powerBudgetParam : DesignParameter Nat

Example: power budget parameter (400-600W).

Equations

• VerifiedMBSE.Equivalence.powerBudgetParam = { value := 500, valid := fun (n : Nat) => 400 ≤ n ∧ n ≤ 600, inRange := VerifiedMBSE.Equivalence.powerBudgetParam._proof_3 }