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_AEBSDegradedInputVerification {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 DegradedInputScenarioIdentity {12    staleInput;13    missingInput;14    malformedInput;15    inconsistentInput;16    unavailableInput;17  }18  enum def DegradedInputEvidenceOutcome {19    passBoundedDetection;20    failWrongDisposition;21    inconclusiveInstrumentation;22    errorEvidence;23  }24  item def DegradedInputObservationSet;25  item def DegradedInputEvaluation {26    attribute scenario : DegradedInputScenarioIdentity;27    attribute outcome : DegradedInputEvidenceOutcome;28  }29  calc def MapDegradedInputOutcomeToVerdict {30    in outcome : DegradedInputEvidenceOutcome;31    return verdict : VerdictKind =32      if outcome == DegradedInputEvidenceOutcome::passBoundedDetection? VerdictKind::pass33      else if outcome == DegradedInputEvidenceOutcome::failWrongDisposition? VerdictKind::fail34      else if outcome == DegradedInputEvidenceOutcome::errorEvidence? VerdictKind::error35      else VerdictKind::inconclusive;36  }3738  part def DegradedInputMatrixBench {39    attribute scenario : DegradedInputScenarioIdentity;40  }41  requirement def DegradedInputEvidenceContract;42  requirement evidenceContractClosedInputHealthScenario : DegradedInputEvidenceContract {43    subject bench : DegradedInputMatrixBench;44    require constraint statement { language "English" /* The bench shall inject exactly one closed stale, missing, malformed, inconsistent, or unavailable input condition after any required healthy baseline. A degraded state is accepted only while its observation age stays within 0.2 s, detection is closed within a 0.25 s window, and runtime-graph sampling gaps stay at or below 0.2 s. */ }45  }46  requirement evidenceContractStateOwnership : DegradedInputEvidenceContract {47    subject bench : DegradedInputMatrixBench;48    require constraint statement { language "English" /* The bench shall retain producer identity, affected topic, source timing, and ordered degraded-state transition and ownership observations. */ }49  }50  requirement evidenceContractStatusIndication : DegradedInputEvidenceContract {51    subject bench : DegradedInputMatrixBench;52    require constraint statement { language "English" /* The bench shall retain ordered AEBS status-indication observations for the bound input-health scenario. */ }53  }54  requirement evidenceContractObserverFailureIsNotPass : DegradedInputEvidenceContract {55    subject bench : DegradedInputMatrixBench;56    require constraint statement { language "English" /* The bench shall map missing, contradictory, contaminated, or unobservable evidence to inconclusive or error, never pass. */ }57  }5859  part staleInputBench : DegradedInputMatrixBench {60    attribute :>> scenario = DegradedInputScenarioIdentity::staleInput;61  }62  part missingInputBench : DegradedInputMatrixBench {63    attribute :>> scenario = DegradedInputScenarioIdentity::missingInput;64  }65  part malformedInputBench : DegradedInputMatrixBench {66    attribute :>> scenario = DegradedInputScenarioIdentity::malformedInput;67  }68  part inconsistentInputBench : DegradedInputMatrixBench {69    attribute :>> scenario = DegradedInputScenarioIdentity::inconsistentInput;70  }71  part unavailableInputBench : DegradedInputMatrixBench {72    attribute :>> scenario = DegradedInputScenarioIdentity::unavailableInput;73  }7475  verification def DegradedUnavailableVerification {76    subject verifiedBench : DegradedInputMatrixBench;77    objective evidenceObjective {78      verify evidenceContractClosedInputHealthScenario;79      verify evidenceContractStateOwnership;80      verify evidenceContractStatusIndication;81      verify evidenceContractObserverFailureIsNotPass;82    }83    action collectData {84      @VerificationMethod{ kind = test; }85      out item retainedObservations : DegradedInputObservationSet;86    }87    action processData {88      @VerificationMethod{ kind = analyze; }89      in scenarioIdentity : DegradedInputScenarioIdentity = verifiedBench.scenario;90      in item retainedObservations : DegradedInputObservationSet = collectData.retainedObservations;91      out item replayedEvaluation : DegradedInputEvaluation;92    }93    action evaluateData {94      @VerificationMethod{ kind = analyze; }95      in item replayedEvaluation : DegradedInputEvaluation = processData.replayedEvaluation;96      out verdict : VerdictKind = MapDegradedInputOutcomeToVerdict(replayedEvaluation.outcome);97    }98    return verdict : VerdictKind = evaluateData.verdict;99  }100  verification staleInputVerification : DegradedUnavailableVerification {101    @VerificationMethod{ kind = (test, analyze); }102    subject verifiedBench :> staleInputBench;103  }104  verification missingInputVerification : DegradedUnavailableVerification {105    @VerificationMethod{ kind = (test, analyze); }106    subject verifiedBench :> missingInputBench;107  }108  verification malformedInputVerification : DegradedUnavailableVerification {109    @VerificationMethod{ kind = (test, analyze); }110    subject verifiedBench :> malformedInputBench;111  }112  verification inconsistentInputVerification : DegradedUnavailableVerification {113    @VerificationMethod{ kind = (test, analyze); }114    subject verifiedBench :> inconsistentInputBench;115  }116  verification unavailableInputVerification : DegradedUnavailableVerification {117    @VerificationMethod{ kind = (test, analyze); }118    subject verifiedBench :> unavailableInputBench;119  }120  part verificationSystem {121    perform staleInputVerification;122    perform missingInputVerification;123    perform malformedInputVerification;124    perform inconsistentInputVerification;125    perform unavailableInputVerification;126  }127128  dependency degradedStateEvidenceRelevantToStateTransitionCandidate129    from evidenceContractStateOwnership to reqHandleDegradedUnavailableInputs;130  dependency degradedStatusEvidenceRelevantToStatusIndicationCandidate131    from evidenceContractStatusIndication 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 aebsDegradedInputVerificationAssuranceView {144    viewpoint selectedArgumentationAssuranceViewpoint : ArgumentationAssuranceViewpoint {145      frame argumentationAssuranceConcern;146    }147148    expose DE4SDV_AEBSDegradedInputVerification::*;149    render asTreeDiagram;150  }151}152