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_AEBS009EVerification {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 ScenarioIdentity009E {12    clearPath;13    adjacentObject;14    nonClosingTarget;15    belowTrigger;16  }17  enum def EvidenceOutcome009E {18    passBoundedSilence;19    failUnexpectedActivation;20    inconclusiveCoverage;21    errorEvidence;22  }23  item def Retained009EObservationSet;24  item def Replayed009EEvaluation {25    attribute scenario : ScenarioIdentity009E;26    attribute outcome : EvidenceOutcome009E;27  }28  calc def Map009EOutcomeToVerdict {29    in outcome : EvidenceOutcome009E;30    return verdict : VerdictKind =31      if outcome == EvidenceOutcome009E::passBoundedSilence? VerdictKind::pass32      else if outcome == EvidenceOutcome009E::failUnexpectedActivation? VerdictKind::fail33      else if outcome == EvidenceOutcome009E::errorEvidence? VerdictKind::error34      else VerdictKind::inconclusive;35  }3637  part def FalseReactionMatrixBench009E {38    attribute scenario : ScenarioIdentity009E;39  }40  requirement def EvidenceContract009E;41  requirement evidenceContract009EClosedNonActivationScenario : EvidenceContract009E {42    subject bench : FalseReactionMatrixBench009E;43    require constraint { doc /* The bench shall bind one closed scenario identity and a complete observation window. */ }44  }45  requirement evidenceContract009EWarningSilenceWindow : EvidenceContract009E {46    subject bench : FalseReactionMatrixBench009E;47    require constraint { doc /* The bench shall establish warning silence only from a complete periodic window with fresh terminal coverage and no contradictory warning. */ }48  }49  requirement evidenceContract009EBrakingSilenceWindow : EvidenceContract009E {50    subject bench : FalseReactionMatrixBench009E;51    require constraint { doc /* The bench shall establish braking silence only from complete command, required-input-health, and publisher-topology coverage with no contradictory command. */ }52  }5354  part clearPathBench009E : FalseReactionMatrixBench009E {55    attribute :>> scenario = ScenarioIdentity009E::clearPath;56  }57  part adjacentObjectBench009E : FalseReactionMatrixBench009E {58    attribute :>> scenario = ScenarioIdentity009E::adjacentObject;59  }60  part nonClosingTargetBench009E : FalseReactionMatrixBench009E {61    attribute :>> scenario = ScenarioIdentity009E::nonClosingTarget;62  }63  part belowTriggerBench009E : FalseReactionMatrixBench009E {64    attribute :>> scenario = ScenarioIdentity009E::belowTrigger;65  }6667  verification def FalseReactionResistanceVerification009E {68    subject verifiedBench : FalseReactionMatrixBench009E;69    objective evidenceObjective009E {70      verify evidenceContract009EClosedNonActivationScenario;71      verify evidenceContract009EWarningSilenceWindow;72      verify evidenceContract009EBrakingSilenceWindow;73    }74    action collectData {75      @VerificationMethod{ kind = test; }76      out item retainedObservations : Retained009EObservationSet;77    }78    action processData {79      @VerificationMethod{ kind = analyze; }80      in scenarioIdentity : ScenarioIdentity009E = verifiedBench.scenario;81      in item retainedObservations : Retained009EObservationSet = collectData.retainedObservations;82      out item replayedEvaluation : Replayed009EEvaluation;83    }84    action evaluateData {85      @VerificationMethod{ kind = analyze; }86      in item replayedEvaluation : Replayed009EEvaluation = processData.replayedEvaluation;87      out verdict : VerdictKind = Map009EOutcomeToVerdict(replayedEvaluation.outcome);88    }89    return verdict : VerdictKind = evaluateData.verdict;90  }91  verification clearPathNonActivationVerification009E : FalseReactionResistanceVerification009E {92    @VerificationMethod{ kind = (test, analyze); }93    subject verifiedBench :> clearPathBench009E;94  }95  verification adjacentObjectNonActivationVerification009E : FalseReactionResistanceVerification009E {96    @VerificationMethod{ kind = (test, analyze); }97    subject verifiedBench :> adjacentObjectBench009E;98  }99  verification nonClosingTargetNonActivationVerification009E : FalseReactionResistanceVerification009E {100    @VerificationMethod{ kind = (test, analyze); }101    subject verifiedBench :> nonClosingTargetBench009E;102  }103  verification belowTriggerNonActivationVerification009E : FalseReactionResistanceVerification009E {104    @VerificationMethod{ kind = (test, analyze); }105    subject verifiedBench :> belowTriggerBench009E;106  }107  part verificationSystem009E {108    perform clearPathNonActivationVerification009E;109    perform adjacentObjectNonActivationVerification009E;110    perform nonClosingTargetNonActivationVerification009E;111    perform belowTriggerNonActivationVerification009E;112  }113114  dependency warningSilenceEvidenceRelevantToWarningSilenceCandidate115    from evidenceContract009EWarningSilenceWindow to reqResistFalseReaction;116  dependency brakingSilenceEvidenceRelevantToBrakingSilenceCandidate117    from evidenceContract009EBrakingSilenceWindow 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 aebs009EVerificationAssuranceView {130    viewpoint selectedArgumentationAssuranceViewpoint : ArgumentationAssuranceViewpoint {131      frame argumentationAssuranceConcern;132    }133134    expose DE4SDV_AEBS009EVerification::*;135    render asTreeDiagram;136  }137}138