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

Source

1/* INC-AEBS-009E bounded non-activation matrix; planned System 2 executable contracts. */2package DE4SDV_AEBSNonActivationVerification {3  private import VerificationCases::*;4  private import VerificationMethodKind::*;5  private import DE4SDV_AEBSNeedsRequirements::Features::AEBS::NeedsRequirements::*;6  private import SAF_Viewpoints::*;7  private import DE4SDV_Stakeholders::*;8  private import Views::*;91011  enum def NonActivationScenarioIdentity {12    clearPath;13    adjacentObject;14    nonClosingTarget;15    belowTrigger;16  }17  enum def NonActivationEvidenceOutcome {18    passBoundedSilence;19    failUnexpectedActivation;20    inconclusiveCoverage;21    errorEvidence;22  }23  item def NonActivationObservationSet;24  item def NonActivationEvaluation {25    attribute scenario : NonActivationScenarioIdentity;26    attribute outcome : NonActivationEvidenceOutcome;27  }28  calc def MapNonActivationOutcomeToVerdict {29    in outcome : NonActivationEvidenceOutcome;30    return verdict : VerdictKind =31      if outcome == NonActivationEvidenceOutcome::passBoundedSilence? VerdictKind::pass32      else if outcome == NonActivationEvidenceOutcome::failUnexpectedActivation? VerdictKind::fail33      else if outcome == NonActivationEvidenceOutcome::errorEvidence? VerdictKind::error34      else VerdictKind::inconclusive;35  }3637  part def FalseReactionMatrixBench {38    attribute scenario : NonActivationScenarioIdentity;39  }40  requirement def NonActivationEvidenceContract;41  requirement evidenceContractClosedNonActivationScenario : NonActivationEvidenceContract {42    subject bench : FalseReactionMatrixBench;43    require constraint statement { language "English" /* The bench shall bind one closed scenario identity and a complete observation window: at least 4.0 s duration with no sample gap above 0.75 s and every required input no older than 0.5 s at window close. */ }44  }45  requirement evidenceContractWarningSilenceWindow : NonActivationEvidenceContract {46    subject bench : FalseReactionMatrixBench;47    require constraint statement { language "English" /* The bench shall establish warning silence only from a complete periodic window with fresh terminal coverage and no contradictory warning. */ }48  }49  requirement evidenceContractBrakingSilenceWindow : NonActivationEvidenceContract {50    subject bench : FalseReactionMatrixBench;51    require constraint statement { language "English" /* The bench shall establish braking silence only from complete command, required-input-health, and publisher-topology coverage with no contradictory command. */ }52  }5354  part clearPathBench : FalseReactionMatrixBench {55    attribute :>> scenario = NonActivationScenarioIdentity::clearPath;56  }57  part adjacentObjectBench : FalseReactionMatrixBench {58    attribute :>> scenario = NonActivationScenarioIdentity::adjacentObject;59  }60  part nonClosingTargetBench : FalseReactionMatrixBench {61    attribute :>> scenario = NonActivationScenarioIdentity::nonClosingTarget;62  }63  part belowTriggerBench : FalseReactionMatrixBench {64    attribute :>> scenario = NonActivationScenarioIdentity::belowTrigger;65  }6667  verification def FalseReactionResistanceVerification {68    subject verifiedBench : FalseReactionMatrixBench;69    objective evidenceObjective {70      verify evidenceContractClosedNonActivationScenario;71      verify evidenceContractWarningSilenceWindow;72      verify evidenceContractBrakingSilenceWindow;73    }74    action collectData {75      @VerificationMethod{ kind = test; }76      out item retainedObservations : NonActivationObservationSet;77    }78    action processData {79      @VerificationMethod{ kind = analyze; }80      in scenarioIdentity : NonActivationScenarioIdentity = verifiedBench.scenario;81      in item retainedObservations : NonActivationObservationSet = collectData.retainedObservations;82      out item replayedEvaluation : NonActivationEvaluation;83    }84    action evaluateData {85      @VerificationMethod{ kind = analyze; }86      in item replayedEvaluation : NonActivationEvaluation = processData.replayedEvaluation;87      out verdict : VerdictKind = MapNonActivationOutcomeToVerdict(replayedEvaluation.outcome);88    }89    return verdict : VerdictKind = evaluateData.verdict;90  }91  verification clearPathNonActivationVerification : FalseReactionResistanceVerification {92    @VerificationMethod{ kind = (test, analyze); }93    subject verifiedBench :> clearPathBench;94  }95  verification adjacentObjectNonActivationVerification : FalseReactionResistanceVerification {96    @VerificationMethod{ kind = (test, analyze); }97    subject verifiedBench :> adjacentObjectBench;98  }99  verification nonClosingTargetNonActivationVerification : FalseReactionResistanceVerification {100    @VerificationMethod{ kind = (test, analyze); }101    subject verifiedBench :> nonClosingTargetBench;102  }103  verification belowTriggerNonActivationVerification : FalseReactionResistanceVerification {104    @VerificationMethod{ kind = (test, analyze); }105    subject verifiedBench :> belowTriggerBench;106  }107  part verificationSystem {108    perform clearPathNonActivationVerification;109    perform adjacentObjectNonActivationVerification;110    perform nonClosingTargetNonActivationVerification;111    perform belowTriggerNonActivationVerification;112  }113114  dependency warningSilenceEvidenceRelevantToWarningSilenceCandidate115    from evidenceContractWarningSilenceWindow to reqResistFalseReaction;116  dependency brakingSilenceEvidenceRelevantToBrakingSilenceCandidate117    from evidenceContractBrakingSilenceWindow to reqResistFalseBrakingCommand;118119  concern physicalStructureConcern : PhysicalStructureConcern {120    subject;121    stakeholder systemsEngineer : SystemsEngineer;122    stakeholder reviewer : OpenSourceReviewer;123  }124125  concern argumentationAssuranceConcern : ArgumentationAssuranceConcern {126    doc /* Evidence-based assurance claims and their supporting argumentation. */127  }128129  view aebsNonActivationVerificationAssuranceView {130    viewpoint selectedArgumentationAssuranceViewpoint : ArgumentationAssuranceViewpoint {131      frame argumentationAssuranceConcern;132    }133134    expose DE4SDV_AEBSNonActivationVerification::*;135    render asTreeDiagram;136  }137}138