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

Source

1/* INC-AEBS-009I configuration-bounded criterion trace; compliance is always withheld. */2package DE4SDV_AEBS009IVerification {3  private import VerificationCases::*;4  private import VerificationMethodKind::*;5  private import ScalarValues::*;6  private import DE4SDV_AEBSNeedsRequirements::Features::AEBS::NeedsRequirements::*;7  private import SAF_Viewpoints::*;8  private import DE4SDV_Stakeholders::*;9  private import Views::*;101112  enum def ScenarioIdentity009I {13    pedestrianCriterion;14    bicycleCriterion;15  }16  enum def EvidenceOutcome009I {17    passBoundedCriterion;18    failBoundedCriterion;19    inconclusiveApplicabilityOrEvidence;20    errorEvidence;21  }22  item def ControlledCriterionIdentity009I {23    attribute sourceId : String;24    attribute sourceOriginalSha256 : String;25    attribute sourceMetadataPath : String;26    attribute criteriaPath : String;27    attribute evaluatorPath : String;28  }29  item controlledCriterionIdentity009I : ControlledCriterionIdentity009I {30    attribute :>> sourceId = "E/ECE/TRANS/505/Rev.3/Add.151/Rev.2";31    attribute :>> sourceOriginalSha256 = "dc9cc84498dcae8f0888067ad3967fb5a346e814bc2f19128987a654c8a193de";32    attribute :>> sourceMetadataPath = "methodologies/sysmod-sysmlv2/pilots/aebs-regulatory-source.yaml";33    attribute :>> criteriaPath = "methodologies/sysmod-sysmlv2/pilots/aebs-regulatory-criteria.yaml";34    attribute :>> evaluatorPath = "scripts/aebs_regulatory_criteria.py";35  }36  item def Retained009ICriterionEvidence {37    attribute sourceOriginalSha256 : String;38    attribute testedConfigurationIdentity : String;39    attribute measurementArtifactSha256 : String;40  }41  item def Replayed009ICriterionEvaluation {42    attribute scenario : ScenarioIdentity009I;43    attribute outcome : EvidenceOutcome009I;44  }45  calc def Map009IOutcomeToVerdict {46    in outcome : EvidenceOutcome009I;47    return verdict : VerdictKind =48      if outcome == EvidenceOutcome009I::passBoundedCriterion? VerdictKind::pass49      else if outcome == EvidenceOutcome009I::failBoundedCriterion? VerdictKind::fail50      else if outcome == EvidenceOutcome009I::errorEvidence? VerdictKind::error51      else VerdictKind::inconclusive;52  }5354  part def RegulatoryCriterionBench009I {55    attribute scenario : ScenarioIdentity009I;56  }57  requirement def EvidenceContract009I;58  requirement evidenceContract009ISourceIdentity : EvidenceContract009I {59    subject bench : RegulatoryCriterionBench009I;60    require constraint { doc /* The bench shall bind controlled source E/ECE/TRANS/505/Rev.3/Add.151/Rev.2, original SHA-256 dc9cc84498dcae8f0888067ad3967fb5a346e814bc2f19128987a654c8a193de, source metadata, criterion map, evaluator identity, and an explicit applicability disposition. */ }61  }62  requirement evidenceContract009IPedestrianApplicableCriterion : EvidenceContract009I {63    subject bench : RegulatoryCriterionBench009I;64    require constraint { doc /* For the pedestrian scenario only, the bench shall preserve the selected pedestrian-target criterion provenance, units, prescribed conditions, tolerance, uncertainty treatment, repeated-run rule, and tested configuration without making an authority interpretation. */ }65  }66  requirement evidenceContract009IBicycleApplicableCriterion : EvidenceContract009I {67    subject bench : RegulatoryCriterionBench009I;68    require constraint { doc /* For the bicycle scenario only, the bench shall preserve the selected bicycle-target criterion provenance, units, prescribed conditions, tolerance, uncertainty treatment, repeated-run rule, and tested configuration without making an authority interpretation. */ }69  }70  requirement evidenceContract009IMeasurementTrace : EvidenceContract009I {71    subject bench : RegulatoryCriterionBench009I;72    require constraint { doc /* The bench shall trace each bounded result to replayable observations, processing steps, unit conversion, next-higher-speed selection, repeated-run evidence, and boundary decision. */ }73  }74  requirement evidenceContract009IProvenance : EvidenceContract009I {75    subject bench : RegulatoryCriterionBench009I;76    require constraint { doc /* The bench shall hash-bind source metadata, criterion mapping, tested configuration, runtime, evaluator, measurements, and retained artifacts. */ }77  }78  requirement evidenceContract009IConfigurationBoundedVerdict : EvidenceContract009I {79    subject bench : RegulatoryCriterionBench009I;80    require constraint { doc /* The bench shall limit the verdict to one exact tested configuration. Missing applicability, prescribed conditions, target fidelity, uncertainty, repetitions, source control, or provenance shall be inconclusive or error. Compliance, certification, homologation, and type approval remain withheld. */ }81  }8283  part pedestrianCriterionBench009I : RegulatoryCriterionBench009I {84    attribute :>> scenario = ScenarioIdentity009I::pedestrianCriterion;85  }86  part bicycleCriterionBench009I : RegulatoryCriterionBench009I {87    attribute :>> scenario = ScenarioIdentity009I::bicycleCriterion;88  }8990  verification def PedestrianCriterionVerification009I {91    subject verifiedBench : RegulatoryCriterionBench009I;92    objective pedestrianEvidenceObjective009I {93      verify evidenceContract009ISourceIdentity;94      verify evidenceContract009IPedestrianApplicableCriterion;95      verify evidenceContract009IMeasurementTrace;96      verify evidenceContract009IProvenance;97      verify evidenceContract009IConfigurationBoundedVerdict;98    }99    action collectData {100      @VerificationMethod{ kind = inspect; }101      out item retainedObservations : Retained009ICriterionEvidence;102    }103    action processData {104      @VerificationMethod{ kind = analyze; }105      in scenarioIdentity : ScenarioIdentity009I = verifiedBench.scenario;106      in item retainedObservations : Retained009ICriterionEvidence = collectData.retainedObservations;107      out item replayedEvaluation : Replayed009ICriterionEvaluation;108    }109    action evaluateData {110      @VerificationMethod{ kind = analyze; }111      in item replayedEvaluation : Replayed009ICriterionEvaluation = processData.replayedEvaluation;112      out verdict : VerdictKind = Map009IOutcomeToVerdict(replayedEvaluation.outcome);113    }114    return verdict : VerdictKind = evaluateData.verdict;115  }116  verification def BicycleCriterionVerification009I {117    subject verifiedBench : RegulatoryCriterionBench009I;118    objective bicycleEvidenceObjective009I {119      verify evidenceContract009ISourceIdentity;120      verify evidenceContract009IBicycleApplicableCriterion;121      verify evidenceContract009IMeasurementTrace;122      verify evidenceContract009IProvenance;123      verify evidenceContract009IConfigurationBoundedVerdict;124    }125    action collectData {126      @VerificationMethod{ kind = inspect; }127      out item retainedObservations : Retained009ICriterionEvidence;128    }129    action processData {130      @VerificationMethod{ kind = analyze; }131      in scenarioIdentity : ScenarioIdentity009I = verifiedBench.scenario;132      in item retainedObservations : Retained009ICriterionEvidence = collectData.retainedObservations;133      out item replayedEvaluation : Replayed009ICriterionEvaluation;134    }135    action evaluateData {136      @VerificationMethod{ kind = analyze; }137      in item replayedEvaluation : Replayed009ICriterionEvaluation = processData.replayedEvaluation;138      out verdict : VerdictKind = Map009IOutcomeToVerdict(replayedEvaluation.outcome);139    }140    return verdict : VerdictKind = evaluateData.verdict;141  }142  verification pedestrianCriterionVerification009I : PedestrianCriterionVerification009I {143    @VerificationMethod{ kind = (inspect, analyze); }144    subject verifiedBench :> pedestrianCriterionBench009I;145  }146  verification bicycleCriterionVerification009I : BicycleCriterionVerification009I {147    @VerificationMethod{ kind = (inspect, analyze); }148    subject verifiedBench :> bicycleCriterionBench009I;149  }150  part verificationSystem009I {151    perform pedestrianCriterionVerification009I;152    perform bicycleCriterionVerification009I;153  }154155  dependency sourceControlRelevantToRegulatoryVisibilityNeed156    from evidenceContract009ISourceIdentity to needVisibleRegulatoryAssumptions;157  dependency pedestrianCriterionRelevantToPedestrianDetectionCandidate158    from evidenceContract009IPedestrianApplicableCriterion to reqPedestrianTargetResponse;159  dependency pedestrianCriterionRelevantToPedestrianResponseCandidate160    from evidenceContract009IPedestrianApplicableCriterion to reqPedestrianTargetControlledResponse;161  dependency bicycleCriterionRelevantToBicycleDetectionCandidate162    from evidenceContract009IBicycleApplicableCriterion to reqBicycleTargetResponse;163  dependency bicycleCriterionRelevantToBicycleResponseCandidate164    from evidenceContract009IBicycleApplicableCriterion to reqBicycleTargetControlledResponse;165166  concern physicalStructureConcern : PhysicalStructureConcern {167    subject;168    stakeholder systemsEngineer : SystemsEngineer;169    stakeholder reviewer : OpenSourceReviewer;170  }171172  concern argumentationAssuranceConcern : ArgumentationAssuranceConcern {173    doc /* Evidence-based assurance claims and their supporting argumentation. */174  }175176  view aebs009IVerificationAssuranceView {177    viewpoint selectedArgumentationAssuranceViewpoint : ArgumentationAssuranceViewpoint {178      frame argumentationAssuranceConcern;179    }180181    expose DE4SDV_AEBS009IVerification::*;182    render asTreeDiagram;183  }184}185