V-Model Design Layers (ECSS-E-ST-10C Compliant)

Overview

Eight layers: the seven ECSS-E-ST-10C layers (mission, system, segment, subsystem, assembly, unit, part) plus a project-specific component layer inserted between unit and part.

Depth-based ordering

Each Layer is assigned an integer depth in the range 0..7, and the Ord instance together with the Layer.supports relation are defined uniformly in terms of this depth. A larger depth denotes a lower layer (further decomposition).

Layer	depth	Description
mission	0	Overall mission
system	1	A single spacecraft or ground station as a whole
segment	2	Major divisions such as space segment / ground segment
subsystem	3	AOCS, EPS, TCS, ...
assembly	4	Assemblies: avionics boxes, valve stacks
unit	5	Units: individual sensors, a single MCU
component	6	Components: an ADC IC, a motor (project-specific)
part	7	Terminal parts: resistors, bolts, ...

The Ord instance orders layers naturally by depth, so mission < system < ... < part, matching the usual ECSS hierarchy diagrams where higher levels appear with smaller indices.

inductive VerifiedMBSE.VV.Layer : Type

V-model design layer: the seven ECSS-E-ST-10C layers plus a project-specific component layer.

• mission : Layer
• system : Layer
• segment : Layer
• subsystem : Layer
• assembly : Layer
• unit : Layer
• component : Layer
• part : Layer

@[implicit_reducible]

instance VerifiedMBSE.VV.instReprLayer : Repr Layer

Equations

• VerifiedMBSE.VV.instReprLayer = { reprPrec := VerifiedMBSE.VV.instReprLayer.repr }

def VerifiedMBSE.VV.instReprLayer.repr : Layer → Nat → Std.Format

Equations

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

def VerifiedMBSE.VV.instBEqLayer.beq : Layer → Layer → Bool

Equations

• VerifiedMBSE.VV.instBEqLayer.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance VerifiedMBSE.VV.instBEqLayer : BEq Layer

Equations

• VerifiedMBSE.VV.instBEqLayer = { beq := VerifiedMBSE.VV.instBEqLayer.beq }

@[implicit_reducible]

instance VerifiedMBSE.VV.instDecidableEqLayer : DecidableEq Layer

Equations

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

def VerifiedMBSE.VV.Layer.depth : Layer → Nat

Depth of each layer (0 = topmost mission, 7 = bottom-most part).

The supports relation and the Ord instance are both defined in terms of this depth.

Equations

• VerifiedMBSE.VV.Layer.mission.depth = 0
• VerifiedMBSE.VV.Layer.system.depth = 1
• VerifiedMBSE.VV.Layer.segment.depth = 2
• VerifiedMBSE.VV.Layer.subsystem.depth = 3
• VerifiedMBSE.VV.Layer.assembly.depth = 4
• VerifiedMBSE.VV.Layer.unit.depth = 5
• VerifiedMBSE.VV.Layer.component.depth = 6
• VerifiedMBSE.VV.Layer.part.depth = 7

@[implicit_reducible]

instance VerifiedMBSE.VV.instOrdLayer : Ord Layer

Layer ordering via depth.

Produces the natural order mission (0) < system (1) < ... < part (7), in agreement with the usual ECSS hierarchy diagrams (upper layers have smaller indices).

Equations

• VerifiedMBSE.VV.instOrdLayer = { compare := fun (a b : VerifiedMBSE.VV.Layer) => compare a.depth b.depth }