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

Source

1/*2 * DE4SDV INC-AEBS-009B nominal moving-vehicle-target evidence slice.3 *4 * This model records the bounded verification composition and evidence obligations5 * exercised by the executable bench. Its native verification case verifies only6 * the measurable System 2 evidence contracts defined here. Relevance links to7 * draft System 1 product-requirement candidates are neither verification nor8 * satisfaction claims. The model does not claim complete conceptual realization,9 * physical brake performance, regulatory compliance, certification,10 * homologation, or type approval.11 */1213package DE4SDV_AEBS009BNominalEvidence {14  private import VerificationCases::*;15  private import VerificationMethodKind::*;16  private import DE4SDV_AEBSNeedsRequirements::Features::AEBS::NeedsRequirements::*;17  private import SAF_Viewpoints::*;18  private import DE4SDV_Stakeholders::*;19  private import Views::*;202122  item def CoordinatorRiskTelemetry;23  item def NativeInterventionDiagnostic;24  item def DriverOverrideSample;25  item def DriverWarningRequest;26  item def EmergencyBrakingRequest {27    doc /*28     * Direct nominal-path AEBS braking demand. This contract is distinct from29     * EmergencyInterventionRequest and MinimumRiskManoeuvreRequest. No MRM30     * request is produced or selected by the bounded 009B composition.31     */32  }33  item def EgoMotionObservation;34  item def NominalGateCommand;35  item def MapPosePair;36  item def BrakingLifecycleState;37  item def Retained009BObservationSet;38  item def Replayed009BEvaluation;3940  port def RiskTelemetryOutput {41    out item riskTelemetry : CoordinatorRiskTelemetry;42  }43  port def RiskTelemetryInput {44    in item riskTelemetry : CoordinatorRiskTelemetry;45  }46  port def InterventionDiagnosticOutput {47    out item interventionDiagnostic : NativeInterventionDiagnostic;48  }49  port def InterventionDiagnosticInput {50    in item interventionDiagnostic : NativeInterventionDiagnostic;51  }52  port def OverrideSampleInput {53    in item overrideSample : DriverOverrideSample;54  }55  port def WarningRequestOutput {56    out item warningRequest : DriverWarningRequest;57  }58  port def WarningRequestInput {59    in item warningRequest : DriverWarningRequest;60  }61  port def BrakingRequestOutput {62    out item brakingRequest : EmergencyBrakingRequest;63  }64  port def BrakingRequestInput {65    in item brakingRequest : EmergencyBrakingRequest;66  }67  port def EgoMotionInput {68    in item egoMotion : EgoMotionObservation;69  }70  port def EgoMotionOutput {71    out item egoMotion : EgoMotionObservation;72  }73  port def GateCommandOutput {74    out item gateCommand : NominalGateCommand;75  }76  port def GateCommandInput {77    in item gateCommand : NominalGateCommand;78  }79  port def MapPosePairOutput {80    out item mapPosePair : MapPosePair;81  }82  port def MapPosePairInput {83    in item mapPosePair : MapPosePair;84  }85  port def LifecycleStateOutput {86    out item lifecycleState : BrakingLifecycleState;87  }88  port def LifecycleStateInput {89    in item lifecycleState : BrakingLifecycleState;90  }9192  part def NativeAutowareAEB009BRole {93    doc /*94     * Uses the pinned Autoware AEB implementation for target processing, RSS95     * collision assessment, and the exact intervention diagnostic tuple only.96     */97    port riskTelemetryOut : RiskTelemetryOutput;98    port interventionDiagnosticOut : InterventionDiagnosticOutput;99  }100101  part def NominalAEBSCoordinator009BRole {102    doc /*103     * Bounded integration role. It derives warning requests from native RSS104     * telemetry, requires a fresh source-stamped false override sample,105     * recognizes only the exact native intervention tuple, emits the direct106     * nominal-path braking request, and releases after continuously fresh held107     * stop evidence. This is not the complete conceptual intervention-decision or108     * emergency-intervention-coordination responsibility.109     */110    port riskTelemetryIn : RiskTelemetryInput;111    port interventionDiagnosticIn : InterventionDiagnosticInput;112    port overrideSampleIn : OverrideSampleInput;113    port egoMotionIn : EgoMotionInput;114    port warningRequestOut : WarningRequestOutput;115    port brakingRequestOut : BrakingRequestOutput;116    port lifecycleStateOut : LifecycleStateOutput;117  }118119  part def NominalVehicleCommandGate009BRole {120    doc /*121     * Receives the coordinator-owned nominal control command with emergency122     * handling disabled. The bounded composition does not select an MRM path.123     */124    port brakingRequestIn : BrakingRequestInput;125    port gateCommandOut : GateCommandOutput;126  }127128  part def IndependentScenarioEvidenceObserver009BRole {129    doc /*130     * Preserves collector-monotonic observations, source stamps, runtime graph131     * identity, and map poses. Replay checks the exact intervention tuple,132     * override freshness, sole nominal publisher, no MRM publishers, continuously133     * fresh stop evidence, and oriented footprint separation for the retained run.134     */135    port warningRequestIn : WarningRequestInput;136    port interventionDiagnosticIn : InterventionDiagnosticInput;137    port overrideSampleIn : OverrideSampleInput;138    port brakingRequestIn : BrakingRequestInput;139    port egoMotionIn : EgoMotionInput;140    port gateCommandIn : GateCommandInput;141    port mapPosePairIn : MapPosePairInput;142    port lifecycleStateIn : LifecycleStateInput;143  }144145  part def NominalMovingVehicleTargetBench009B {146    port overrideSampleIn : OverrideSampleInput;147    port egoMotionIn : EgoMotionInput;148    port mapPosePairIn : MapPosePairInput;149150    part nativeAEB : NativeAutowareAEB009BRole;151    part coordinator : NominalAEBSCoordinator009BRole;152    part nominalGate : NominalVehicleCommandGate009BRole;153    part evidenceObserver : IndependentScenarioEvidenceObserver009BRole;154155    bind overrideSampleIn = coordinator.overrideSampleIn;156    bind overrideSampleIn = evidenceObserver.overrideSampleIn;157    bind egoMotionIn = coordinator.egoMotionIn;158    bind egoMotionIn = evidenceObserver.egoMotionIn;159    bind mapPosePairIn = evidenceObserver.mapPosePairIn;160161    flow from nativeAEB.riskTelemetryOut.riskTelemetry162      to coordinator.riskTelemetryIn.riskTelemetry;163    flow from nativeAEB.interventionDiagnosticOut.interventionDiagnostic164      to coordinator.interventionDiagnosticIn.interventionDiagnostic;165    flow from nativeAEB.interventionDiagnosticOut.interventionDiagnostic166      to evidenceObserver.interventionDiagnosticIn.interventionDiagnostic;167    flow from coordinator.warningRequestOut.warningRequest168      to evidenceObserver.warningRequestIn.warningRequest;169    flow from coordinator.brakingRequestOut.brakingRequest170      to nominalGate.brakingRequestIn.brakingRequest;171    flow from coordinator.brakingRequestOut.brakingRequest172      to evidenceObserver.brakingRequestIn.brakingRequest;173    flow from coordinator.lifecycleStateOut.lifecycleState174      to evidenceObserver.lifecycleStateIn.lifecycleState;175    flow from nominalGate.gateCommandOut.gateCommand176      to evidenceObserver.gateCommandIn.gateCommand;177178    exhibit state brakingLifecycle {179      doc /*180       * armed enters brakingLatched only after the exact native diagnostic and a181       * fresh false override evaluation. brakingLatched enters182       * releasedAfterVerifiedStop only after speed <= 0.1 m/s is continuously183       * observed with gaps <= 0.2 s for >= 0.5 s. The release state is absorbing184       * for this one-shot scenario and does not depend on diagnostic clearing.185       */186      state armed;187      state brakingLatched;188      state releasedAfterVerifiedStop;189    }190  }191192  requirement def Nominal009BEvidenceContractRequirement;193194  requirement evidenceContract009BWarningLead : Nominal009BEvidenceContractRequirement {195    doc /* EC-AEBS-009B-01; System 2 evidence contract; method: retained evaluator replay. */196    subject bench : NominalMovingVehicleTargetBench009B;197    require constraint {198      doc /* The replayed collector-monotonic warning request shall precede the exact native intervention diagnostic by at least 0.8 s. */199    }200  }201202  requirement evidenceContract009BFreshOverrideClear : Nominal009BEvidenceContractRequirement {203    doc /* EC-AEBS-009B-02; System 2 evidence contract; method: source-stamp and receipt-freshness analysis. */204    subject bench : NominalMovingVehicleTargetBench009B;205    require constraint {206      doc /* Nominal 009B intervention evidence shall include a source-stamped false override sample that remains within the 0.2 s freshness bound at intervention. Conscious true override behavior is deferred to INC-AEBS-009D. */207    }208  }209210  requirement evidenceContract009BNominalBrakingPath : Nominal009BEvidenceContractRequirement {211    doc /* EC-AEBS-009B-03; System 2 evidence contract; method: runtime-graph and command replay. */212    subject bench : NominalMovingVehicleTargetBench009B;213    require constraint {214      doc /* Runtime graph evidence shall periodically sample the coordinator as the sole nominal gate-input publisher and no MRM publishers from the accepted pre-intervention topology snapshot through verified-stop release, reject any contradictory sample, and reject any sampling gap above 1.0 s; the observed direct EmergencyBrakingRequest shall follow the paired exact native intervention diagnostic. */215    }216  }217218  requirement evidenceContract009BVerifiedStopRelease : Nominal009BEvidenceContractRequirement {219    doc /* EC-AEBS-009B-04; System 2 evidence contract; method: source-stamped odometry and lifecycle replay. */220    subject bench : NominalMovingVehicleTargetBench009B;221    require constraint {222      doc /* Braking shall remain latched until each ego-odometry source stamp is replayed against a collector stamp from the same ROS clock and remains within 0.2 s, speed stays at or below 0.1 m/s for at least 0.5 s, and no receipt gap exceeds 0.2 s; release shall be absorbing for the one-shot scenario and independent of diagnostic retention. */223    }224  }225226  requirement evidenceContract009BIndependentNoncollision : Nominal009BEvidenceContractRequirement {227    doc /* EC-AEBS-009B-05; System 2 evidence contract; method: retained map-pose oriented-footprint analysis. */228    subject bench : NominalMovingVehicleTargetBench009B;229    require constraint {230      doc /* For the retained run, replay shall compute the oriented footprint relation from preserved map poses, reject overlap or touching, require positive then opening separation, and require a fresh footprint relation covering release. */231    }232  }233234  part bench : NominalMovingVehicleTargetBench009B;235236  verification def NominalMovingVehicleTargetVerification009B {237    doc /*238     * Defines execution of the pinned Autoware software in a simulated moving-target239     * environment, collects observations independently, replays the evidence240     * contract, and returns a native verification verdict. The execution is a241     * combined test-and-analysis verification method; it is not product242     * validation, regulatory compliance evidence, or type-approval evidence.243     */244    subject verifiedBench : NominalMovingVehicleTargetBench009B;245246    objective nominalEvidenceObjective {247      verify evidenceContract009BWarningLead;248      verify evidenceContract009BFreshOverrideClear;249      verify evidenceContract009BNominalBrakingPath;250      verify evidenceContract009BVerifiedStopRelease;251      verify evidenceContract009BIndependentNoncollision;252    }253254    action collectData {255      @VerificationMethod{ kind = test; }256      doc /* The independent scenario observer collects typed runtime observations and provenance from the configured bench. */257      out item retainedObservations : Retained009BObservationSet;258    }259260    action processData {261      @VerificationMethod{ kind = analyze; }262      doc /* The repository validator reconstructs typed observations and independently replays the evaluator against the controlled scenario contract. */263      in item retainedObservations : Retained009BObservationSet = collectData.retainedObservations;264      out item replayedEvaluation : Replayed009BEvaluation;265    }266267    action evaluateData {268      @VerificationMethod{ kind = analyze; }269      doc /* The replayed outcome and evidence-contract results are mapped to the verification verdict without treating a stored success label as evidence. */270      in item replayedEvaluation : Replayed009BEvaluation = processData.replayedEvaluation;271      out verdict : VerdictKind;272    }273274    return verdict : VerdictKind = evaluateData.verdict;275  }276277  verification nominalMovingVehicleTargetVerification009B278    : NominalMovingVehicleTargetVerification009B {279    @VerificationMethod{ kind = (test, analyze); }280    subject verifiedBench :> bench;281  }282283  part nominal009BVerificationSystem {284    perform nominalMovingVehicleTargetVerification009B;285  }286287  /*288   * These dependencies record relevance to draft System 1 product-requirement289   * candidates only. They are neither verify nor satisfy relationships. The290   * product candidates remain too broad to claim complete verification from291   * this one bounded simulated scenario.292   */293  dependency warningEvidenceRelevantToWarningCandidate294    from evidenceContract009BWarningLead to reqProvideCollisionWarning;295  dependency overrideClearRelevantToBrakingCandidate296    from evidenceContract009BFreshOverrideClear to reqCommandEmergencyBraking;297  dependency overrideClearRelevantToOverrideCandidate298    from evidenceContract009BFreshOverrideClear to reqAllowDriverOverride;299  dependency brakingPathRelevantToBrakingCandidate300    from evidenceContract009BNominalBrakingPath to reqCommandEmergencyBraking;301302  concern physicalStructureConcern : PhysicalStructureConcern {303    subject;304    stakeholder systemsEngineer : SystemsEngineer;305    stakeholder reviewer : OpenSourceReviewer;306  }307308  concern argumentationAssuranceConcern : ArgumentationAssuranceConcern {309    doc /* Evidence-based assurance claims and their supporting argumentation. */310  }311312  view aebs009BNominalEvidenceAssuranceView {313    viewpoint selectedArgumentationAssuranceViewpoint : ArgumentationAssuranceViewpoint {314      frame argumentationAssuranceConcern;315    }316317    expose DE4SDV_AEBS009BNominalEvidence::*;318    render asTreeDiagram;319  }320}321