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

Source

1/* INC-AEBS-009F degraded/unavailable input matrix; planned System 2 executable contracts. */2package DE4SDV_AEBS009FVerification {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 ScenarioIdentity009F {12    staleInput;13    missingInput;14    malformedInput;15    inconsistentInput;16    unavailableInput;17  }18  enum def EvidenceOutcome009F {19    passBoundedDetection;20    failWrongDisposition;21    inconclusiveInstrumentation;22    errorEvidence;23  }24  item def Retained009FObservationSet;25  item def Replayed009FEvaluation {26    attribute scenario : ScenarioIdentity009F;27    attribute outcome : EvidenceOutcome009F;28  }29  calc def Map009FOutcomeToVerdict {30    in outcome : EvidenceOutcome009F;31    return verdict : VerdictKind =32      if outcome == EvidenceOutcome009F::passBoundedDetection? VerdictKind::pass33      else if outcome == EvidenceOutcome009F::failWrongDisposition? VerdictKind::fail34      else if outcome == EvidenceOutcome009F::errorEvidence? VerdictKind::error35      else VerdictKind::inconclusive;36  }3738  part def DegradedInputMatrixBench009F {39    attribute scenario : ScenarioIdentity009F;40  }41  requirement def EvidenceContract009F;42  requirement evidenceContract009FClosedInputHealthScenario : EvidenceContract009F {43    subject bench : DegradedInputMatrixBench009F;44    require constraint { doc /* The bench shall inject exactly one closed stale, missing, malformed, inconsistent, or unavailable input condition after any required healthy baseline. */ }45  }46  requirement evidenceContract009FStateOwnership : EvidenceContract009F {47    subject bench : DegradedInputMatrixBench009F;48    require constraint { doc /* The bench shall retain producer identity, affected topic, source timing, and ordered degraded-state transition and ownership observations. */ }49  }50  requirement evidenceContract009FStatusIndication : EvidenceContract009F {51    subject bench : DegradedInputMatrixBench009F;52    require constraint { doc /* The bench shall retain ordered AEBS status-indication observations for the bound input-health scenario. */ }53  }54  requirement evidenceContract009FObserverFailureIsNotPass : EvidenceContract009F {55    subject bench : DegradedInputMatrixBench009F;56    require constraint { doc /* The bench shall map missing, contradictory, contaminated, or unobservable evidence to inconclusive or error, never pass. */ }57  }5859  part staleInputBench009F : DegradedInputMatrixBench009F {60    attribute :>> scenario = ScenarioIdentity009F::staleInput;61  }62  part missingInputBench009F : DegradedInputMatrixBench009F {63    attribute :>> scenario = ScenarioIdentity009F::missingInput;64  }65  part malformedInputBench009F : DegradedInputMatrixBench009F {66    attribute :>> scenario = ScenarioIdentity009F::malformedInput;67  }68  part inconsistentInputBench009F : DegradedInputMatrixBench009F {69    attribute :>> scenario = ScenarioIdentity009F::inconsistentInput;70  }71  part unavailableInputBench009F : DegradedInputMatrixBench009F {72    attribute :>> scenario = ScenarioIdentity009F::unavailableInput;73  }7475  verification def DegradedUnavailableVerification009F {76    subject verifiedBench : DegradedInputMatrixBench009F;77    objective evidenceObjective009F {78      verify evidenceContract009FClosedInputHealthScenario;79      verify evidenceContract009FStateOwnership;80      verify evidenceContract009FStatusIndication;81      verify evidenceContract009FObserverFailureIsNotPass;82    }83    action collectData {84      @VerificationMethod{ kind = test; }85      out item retainedObservations : Retained009FObservationSet;86    }87    action processData {88      @VerificationMethod{ kind = analyze; }89      in scenarioIdentity : ScenarioIdentity009F = verifiedBench.scenario;90      in item retainedObservations : Retained009FObservationSet = collectData.retainedObservations;91      out item replayedEvaluation : Replayed009FEvaluation;92    }93    action evaluateData {94      @VerificationMethod{ kind = analyze; }95      in item replayedEvaluation : Replayed009FEvaluation = processData.replayedEvaluation;96      out verdict : VerdictKind = Map009FOutcomeToVerdict(replayedEvaluation.outcome);97    }98    return verdict : VerdictKind = evaluateData.verdict;99  }100  verification staleInputVerification009F : DegradedUnavailableVerification009F {101    @VerificationMethod{ kind = (test, analyze); }102    subject verifiedBench :> staleInputBench009F;103  }104  verification missingInputVerification009F : DegradedUnavailableVerification009F {105    @VerificationMethod{ kind = (test, analyze); }106    subject verifiedBench :> missingInputBench009F;107  }108  verification malformedInputVerification009F : DegradedUnavailableVerification009F {109    @VerificationMethod{ kind = (test, analyze); }110    subject verifiedBench :> malformedInputBench009F;111  }112  verification inconsistentInputVerification009F : DegradedUnavailableVerification009F {113    @VerificationMethod{ kind = (test, analyze); }114    subject verifiedBench :> inconsistentInputBench009F;115  }116  verification unavailableInputVerification009F : DegradedUnavailableVerification009F {117    @VerificationMethod{ kind = (test, analyze); }118    subject verifiedBench :> unavailableInputBench009F;119  }120  part verificationSystem009F {121    perform staleInputVerification009F;122    perform missingInputVerification009F;123    perform malformedInputVerification009F;124    perform inconsistentInputVerification009F;125    perform unavailableInputVerification009F;126  }127128  dependency degradedStateEvidenceRelevantToStateTransitionCandidate129    from evidenceContract009FStateOwnership to reqHandleDegradedUnavailableInputs;130  dependency degradedStatusEvidenceRelevantToStatusIndicationCandidate131    from evidenceContract009FStatusIndication to reqIndicateDegradedUnavailableStatus;132133  concern physicalStructureConcern : PhysicalStructureConcern {134    subject;135    stakeholder systemsEngineer : SystemsEngineer;136    stakeholder reviewer : OpenSourceReviewer;137  }138139  concern argumentationAssuranceConcern : ArgumentationAssuranceConcern {140    doc /* Evidence-based assurance claims and their supporting argumentation. */141  }142143  view aebs009FVerificationAssuranceView {144    viewpoint selectedArgumentationAssuranceViewpoint : ArgumentationAssuranceViewpoint {145      frame argumentationAssuranceConcern;146    }147148    expose DE4SDV_AEBS009FVerification::*;149    render asTreeDiagram;150  }151}152