textual-notation-of-model/packages/features/aebs/aebs_override_verification.sysml

Source

1/* INC-AEBS-009D conscious-override matrix; planned System 2 executable contracts. */2package DE4SDV_AEBS009DVerification {3  private import VerificationCases::*;4  private import VerificationMethodKind::*;5  private import DE4SDV_AEBSNeedsRequirements::Features::AEBS::NeedsRequirements::*;67  enum def ScenarioIdentity009D {8    freshFalseControl;9    freshTrueOverride;10    staleOverride;11    missingOverride;12    malformedOverride;13    futureStampedOverride;14  }15  enum def EvidenceOutcome009D {16    passBoundedScenario;17    failObservedBehavior;18    inconclusiveCoverage;19    errorEvidence;20  }21  item def Retained009DObservationSet;22  item def Replayed009DEvaluation {23    attribute scenario : ScenarioIdentity009D;24    attribute outcome : EvidenceOutcome009D;25  }26  calc def Map009DOutcomeToVerdict {27    in outcome : EvidenceOutcome009D;28    return verdict : VerdictKind =29      if outcome == EvidenceOutcome009D::passBoundedScenario? VerdictKind::pass30      else if outcome == EvidenceOutcome009D::failObservedBehavior? VerdictKind::fail31      else if outcome == EvidenceOutcome009D::errorEvidence? VerdictKind::error32      else VerdictKind::inconclusive;33  }3435  part def OverrideMatrixBench009D {36    attribute scenario : ScenarioIdentity009D;37  }38  requirement def EvidenceContract009D;39  requirement evidenceContract009DClosedOverrideScenario : EvidenceContract009D {40    subject bench : OverrideMatrixBench009D;41    require constraint { doc /* The bench shall bind exactly one closed override scenario identity. */ }42  }43  requirement evidenceContract009DOverrideFreshnessReplay : EvidenceContract009D {44    subject bench : OverrideMatrixBench009D;45    require constraint { doc /* The bench shall replay source stamp, receipt time, value validity, exact diagnostic-source authorization, and the scenario-specific suppression, release, or degraded disposition. */ }46  }47  requirement evidenceContract009DIndependentVerdict : EvidenceContract009D {48    subject bench : OverrideMatrixBench009D;49    require constraint { doc /* The bench shall retain separate observations, evaluation, provenance, and verdict for each scenario; observer failure shall not pass. */ }50  }5152  part overrideFalseControlBench009D : OverrideMatrixBench009D {53    attribute :>> scenario = ScenarioIdentity009D::freshFalseControl;54  }55  part overrideTrueBench009D : OverrideMatrixBench009D {56    attribute :>> scenario = ScenarioIdentity009D::freshTrueOverride;57  }58  part overrideStaleBench009D : OverrideMatrixBench009D {59    attribute :>> scenario = ScenarioIdentity009D::staleOverride;60  }61  part overrideMissingBench009D : OverrideMatrixBench009D {62    attribute :>> scenario = ScenarioIdentity009D::missingOverride;63  }64  part overrideMalformedBench009D : OverrideMatrixBench009D {65    attribute :>> scenario = ScenarioIdentity009D::malformedOverride;66  }67  part overrideFutureStampedBench009D : OverrideMatrixBench009D {68    attribute :>> scenario = ScenarioIdentity009D::futureStampedOverride;69  }7071  verification def ConsciousOverrideVerification009D {72    subject verifiedBench : OverrideMatrixBench009D;73    objective evidenceObjective009D {74      verify evidenceContract009DClosedOverrideScenario;75      verify evidenceContract009DOverrideFreshnessReplay;76      verify evidenceContract009DIndependentVerdict;77    }78    action collectData {79      @VerificationMethod{ kind = test; }80      out item retainedObservations : Retained009DObservationSet;81    }82    action processData {83      @VerificationMethod{ kind = analyze; }84      in scenarioIdentity : ScenarioIdentity009D = verifiedBench.scenario;85      in item retainedObservations : Retained009DObservationSet = collectData.retainedObservations;86      out item replayedEvaluation : Replayed009DEvaluation;87    }88    action evaluateData {89      @VerificationMethod{ kind = analyze; }90      in item replayedEvaluation : Replayed009DEvaluation = processData.replayedEvaluation;91      out verdict : VerdictKind = Map009DOutcomeToVerdict(replayedEvaluation.outcome);92    }93    return verdict : VerdictKind = evaluateData.verdict;94  }95  verification overrideFalseControlVerification009D : ConsciousOverrideVerification009D {96    @VerificationMethod{ kind = (test, analyze); }97    subject verifiedBench :> overrideFalseControlBench009D;98  }99  verification overrideTrueVerification009D : ConsciousOverrideVerification009D {100    @VerificationMethod{ kind = (test, analyze); }101    subject verifiedBench :> overrideTrueBench009D;102  }103  verification overrideStaleVerification009D : ConsciousOverrideVerification009D {104    @VerificationMethod{ kind = (test, analyze); }105    subject verifiedBench :> overrideStaleBench009D;106  }107  verification overrideMissingVerification009D : ConsciousOverrideVerification009D {108    @VerificationMethod{ kind = (test, analyze); }109    subject verifiedBench :> overrideMissingBench009D;110  }111  verification overrideMalformedVerification009D : ConsciousOverrideVerification009D {112    @VerificationMethod{ kind = (test, analyze); }113    subject verifiedBench :> overrideMalformedBench009D;114  }115  verification overrideFutureStampedVerification009D : ConsciousOverrideVerification009D {116    @VerificationMethod{ kind = (test, analyze); }117    subject verifiedBench :> overrideFutureStampedBench009D;118  }119  part verificationSystem009D {120    perform overrideFalseControlVerification009D;121    perform overrideTrueVerification009D;122    perform overrideStaleVerification009D;123    perform overrideMissingVerification009D;124    perform overrideMalformedVerification009D;125    perform overrideFutureStampedVerification009D;126  }127128  dependency overrideEvidenceRelevantToOverrideCandidate129    from evidenceContract009DOverrideFreshnessReplay to reqAllowDriverOverride;130}131