textual-notation-of-model/packages/features/middleware/middleware_verification_evidence.sysml

Source

1/*2 * DE4SDV middleware verification and validation/evidence model slice.3 *4 * INC-MW-010 defines the verification cases, validation scenarios, acceptance5 * criteria, retained evidence, bounded assurance claim, deferred counterclaims,6 * and Phase 12 baseline decision for the configured Autoware + AndroidSDV7 * member.8 *9 * The accepted baseline is limited to the observed forward Vehicle.Speed chain,10 * bounded real Autoware consumption, invalid-envelope rejection, and provider-11 * loss health disposition. Full lifecycle ordering, update/OTA behavior, the12 * reverse lifecycle/status path, production deployment, full-stack Autoware,13 * safety, and certification claims remain deferred or not claimed.14 */1516package DE4SDV_MiddlewareVerificationEvidence {17  private import DE4SDV_MethodContext::*;18  private import DE4SDV_MethodProcess::*;19  private import DE4SDV_ProductLine::*;20  private import DE4SDV_Stakeholders::*;21  private import DE4SDV_ExecutionEnvironments::*;22  private import DE4SDV_MiddlewareRequirements::Features::Middleware::Requirements::*;23  private import DE4SDV_MiddlewareFunctionalArchitecture::Features::Middleware::FunctionalArchitecture::*;24  private import DE4SDV_MiddlewarePhysicalSoftwareRealization::*;25  private import DE4SDV_MiddlewareVariabilityConfiguration::*;26  private import VerificationCases::*;27  private import VerificationMethodKind::*;28  private import ScalarValues::*;29  private import SAF_Viewpoints::*;30  private import Views::*;3132  part incMW010 : FeatureIncrement {33    doc /* INC-MW-010: middleware verification, validation, and evidence. */34  }3536  enum def MiddlewareScenarioIdentity {37    signalTranslation;38    lifecycleCoordination;39    healthForwarding;40    vehicleStartup;41    updateCoordination;42    faultDetection;43  }4445  enum def MiddlewareEvidenceOutcome {46    passBoundedVerification;47    passBoundedValidation;48    failObservedBehavior;49    inconclusiveMissingEvidence;50    blockedTargetRuntime;51    errorEvidence;52  }5354  enum def MiddlewareEvidenceDisposition {55    planned;56    observedBounded;57    partial;58    blocked;59    accepted;60    rejected;61  }6263  item def VehicleSpeedTranslationObservation {64    attribute inputSpeedKmh : Real;65    attribute expectedVelocityMps : Real;66    attribute observedVelocityMps : Real;67    attribute sourceContractIdentity : String;68    attribute consumerContractIdentity : String;69    attribute independentObservation : Boolean;70  }7172  item def MiddlewareLifecycleObservation {73    attribute stateName : String;74    attribute predecessorState : String;75    attribute successorState : String;76    attribute transitionObserved : Boolean;77  }7879  item def MiddlewareHealthObservation {80    attribute healthState : String;81    attribute sourceFresh : Boolean;82    attribute forwarded : Boolean;83    attribute faultIdentity : String;84  }8586  item def RetainedMiddlewareEvidence {87    attribute configurationIdentity : String;88    attribute executionEnvironmentIdentity : String;89    attribute contractIdentity : String;90    attribute rawObservationArtifact : String;91    attribute independentObserverIdentity : String;92    attribute disposition : MiddlewareEvidenceDisposition;93    attribute claimBoundary : String;94  }9596  item def ReplayedMiddlewareEvaluation {97    attribute scenario : MiddlewareScenarioIdentity;98    attribute outcome : MiddlewareEvidenceOutcome;99    attribute acceptanceSummary : String;100  }101102  calc def MapEvidenceOutcomeToVerdict {103    in outcome : MiddlewareEvidenceOutcome;104    return verdict : VerdictKind =105      if outcome == MiddlewareEvidenceOutcome::passBoundedVerification? VerdictKind::pass106      else if outcome == MiddlewareEvidenceOutcome::passBoundedValidation? VerdictKind::pass107      else if outcome == MiddlewareEvidenceOutcome::failObservedBehavior? VerdictKind::fail108      else if outcome == MiddlewareEvidenceOutcome::errorEvidence? VerdictKind::error109      else VerdictKind::inconclusive;110  }111112  part def MiddlewareIntegrationVandVBench {113    doc /*114     * System 1 is the configured member under evaluation. System 2 is the115     * engineering/build/test environment and is not a product selection.116     */117    part system1MemberProduct : MiddlewareAutowareAAOSSDVConfiguredMember;118    part system2TestEnvironment : AOSPAAOSBuildRuntimeEnvironment;119    attribute scenario : MiddlewareScenarioIdentity;120  }121122  part signalTranslationBench010 : MiddlewareIntegrationVandVBench {123    attribute :>> scenario = MiddlewareScenarioIdentity::signalTranslation;124  }125126  part lifecycleCoordinationBench010 : MiddlewareIntegrationVandVBench {127    attribute :>> scenario = MiddlewareScenarioIdentity::lifecycleCoordination;128  }129130  part healthForwardingBench010 : MiddlewareIntegrationVandVBench {131    attribute :>> scenario = MiddlewareScenarioIdentity::healthForwarding;132  }133134  part vehicleStartupBench010 : MiddlewareIntegrationVandVBench {135    attribute :>> scenario = MiddlewareScenarioIdentity::vehicleStartup;136  }137138  part updateCoordinationBench010 : MiddlewareIntegrationVandVBench {139    attribute :>> scenario = MiddlewareScenarioIdentity::updateCoordination;140  }141142  part faultDetectionBench010 : MiddlewareIntegrationVandVBench {143    attribute :>> scenario = MiddlewareScenarioIdentity::faultDetection;144  }145146  requirement def MiddlewareAcceptanceCriterion147    :> EvidenceContractTraceabilityRequirementCandidate;148149  requirement acceptanceCriterion010SignalTranslation : MiddlewareAcceptanceCriterion {150    doc /* AC-MW-010-01; bounded verification of the selected Vehicle.Speed slice. */151    subject bench : MiddlewareIntegrationVandVBench;152    require constraint {153      doc /* The selected contract shall preserve Vehicle.Speed [km/h] semantics, map 36 km/h to 10 m/s and 72 km/h to 20 m/s through division by 3.6, reject invalid/non-finite samples, and expose the resulting VelocityReport field to an independent observer. */154    }155  }156157  requirement acceptanceCriterion010LifecycleCoordination : MiddlewareAcceptanceCriterion {158    doc /* AC-MW-010-02; bounded verification of integration lifecycle behavior. */159    subject bench : MiddlewareIntegrationVandVBench;160    require constraint {161      doc /* The integration boundary shall make startup, initializing, operational, degraded, and shutdown behavior observable, preserve the declared transition ordering, and prevent use before required binding/readiness. */162    }163  }164165  requirement acceptanceCriterion010HealthForwarding : MiddlewareAcceptanceCriterion {166    doc /* AC-MW-010-03; bounded verification of health forwarding. */167    subject bench : MiddlewareIntegrationVandVBench;168    require constraint {169      doc /* Missing, stale, inconsistent, or unavailable provider/transport/consumer health shall produce an observable degraded or unavailable disposition and shall be forwarded to the application boundary without being relabeled as healthy. */170    }171  }172173  requirement acceptanceCriterion010VehicleStartup : MiddlewareAcceptanceCriterion {174    doc /* AC-MW-010-04; validation of vehicle/application startup. */175    subject bench : MiddlewareIntegrationVandVBench;176    require constraint {177      doc /* A configured member startup scenario shall prove provider registration, service discovery/binding, transport readiness, adapter readiness, and ROS 2 consumer readiness in causal order before the signal is accepted. */178    }179  }180181  requirement acceptanceCriterion010UpdateCoordination : MiddlewareAcceptanceCriterion {182    doc /* AC-MW-010-05; validation of integration update behavior. */183    subject bench : MiddlewareIntegrationVandVBench;184    require constraint {185      doc /* An update/OTA scenario shall retain pre-update and post-update identities and observations and shall detect, rather than silently accept, loss or incompatible change of the required signal, lifecycle, health, discovery, or consumer contracts. */186    }187  }188189  requirement acceptanceCriterion010FaultDetection : MiddlewareAcceptanceCriterion {190    doc /* AC-MW-010-06; validation of fault detection and containment. */191    subject bench : MiddlewareIntegrationVandVBench;192    require constraint {193      doc /* Provider, binding, discovery, transport, adapter, and consumer faults shall be detected and classified at the integration boundary; non-safety middleware failure shall not create an uncontrolled emergency intervention command. */194    }195  }196197  requirement acceptanceCriterion010EvidenceIndependence : MiddlewareAcceptanceCriterion {198    doc /* AC-MW-010-07; evidence integrity and claim-boundary criterion. */199    subject bench : MiddlewareIntegrationVandVBench;200    require constraint {201      doc /* Every retained verdict shall bind the configured member, execution environment, contract identities, raw observations, and independent observer evidence. Missing target-runtime evidence shall be inconclusive or blocked, never a runtime pass. */202    }203  }204205  part boundedAAOSBootBaseline010 : InspectedExecutionEnvironmentEvidence {206    doc /*207     * implementation/aaos-sdv-reference-interop-bench/evidence/208     * aaos-cuttlefish-cloud-proof.yaml. This is bounded x86_64 AOSP build and209     * Cuttlefish boot evidence; it is not provider, transport, ROS 2, Autoware,210     * lifecycle, update, fault, or vehicle interoperability evidence.211     */212  }213214  part contractAndRehearsalEvidence010 : ExecutionEnvironmentEvidenceArtifact {215    doc /*216     * Existing reference-contract and provider-neutral adapter tests support217     * contract and conversion claims only. They are not target-runtime proof.218     */219  }220221  part plannedTargetRuntimeEvidence010 : PlannedExecutionEnvironmentEvidence {222    doc /*223     * Planned evidence for provider binding, deployment, discovery, transport,224     * ROS 2 publication, independent Autoware observation, and lifecycle/fault225     * scenarios on the configured member. The campaign-chain subset of this226     * plan is now retained as runtimeCampaignEvidence011; the adapter-chain227     * and lifecycle/update subset remains planned.228     */229  }230231  part runtimeCampaignEvidence011 : RetainedMiddlewareEvidence {232    doc /*233     * E-MW-011. Retained runtime campaign evidence (2026-08-20) for the234     * configured member's modeled two-VM campaign deployment:235     *236     *   vmA.cuttlefishGuest (provider+observer bundles, sdv_core_cf,237     *   instance1 bootconfig) -> vmA.hostForwarder (adb_logcat_bridge,238     *   accepts DE4SDV_ADB_LOGCAT_FORWARD_ACCEPTED) -> privateTcpBoundary239     *   (VPC tcp:4711) -> vmB.ros2Ingress (vehicle_speed_tcp_bridge node,240     *   strict envelope validation, publishes VelocityReport) ->241     *   vmB.independentObserver (validates 10.0 m/s).242     *243     * Gates 1-7 pass; gate 8 (reverse lifecycle/status) not claimed.244     * Provider process, registration, discovery agent, forwarder accepts,245     * exact topic/type/field, independent observer, and ingress rejection246     * were all observed on the live hosts.247     */248    attribute :>> configurationIdentity = "MW-CONFIG-001";249    attribute :>> executionEnvironmentIdentity = "gcp-europe-west4-a-de4sdv-aaos-build+de4sdv-ros2-autoware";250    attribute :>> contractIdentity = "de4sdv.reference.vehicle_speed.VehicleSpeed -> autoware_vehicle_msgs/msg/VelocityReport";251    attribute :>> rawObservationArtifact = "implementation/aaos-sdv-reference-interop-bench/evidence/e-mw-011-runtime-campaign.yaml";252    attribute :>> independentObserverIdentity = "de4sdv_velocity_report_independent_observer (vmB)";253    attribute :>> disposition = MiddlewareEvidenceDisposition::observedBounded;254    attribute :>> claimBoundary = "Campaign-chain runtime evidence on the two-VM deployment; not adapter-chain, lifecycle/update, safety, or certification evidence.";255  }256257  part runtimeAdapterPathEvidence012 : RetainedMiddlewareEvidence {258    doc /*259     * E-MW-012. Retained direct adapter-path campaign evidence for the same260     * configured member. The AAOS provider and observer service bundles,261     * discovery, direct TCP egress, ROS 2 VelocityReport publication,262     * independent 10.0 m/s observation, and invalid-envelope rejection were263     * observed. Gate 8 remained not claimed.264     */265    attribute :>> configurationIdentity = "MW-CONFIG-001";266    attribute :>> executionEnvironmentIdentity = "gcp-europe-west4-a-de4sdv-aaos-build+de4sdv-ros2-autoware";267    attribute :>> contractIdentity = "de4sdv.reference.vehicle_speed.VehicleSpeed -> autoware_vehicle_msgs/msg/VelocityReport";268    attribute :>> rawObservationArtifact = "implementation/aaos-sdv-reference-interop-bench/evidence/e-mw-012-adapter-path-campaign.yaml";269    attribute :>> independentObserverIdentity = "de4sdv_velocity_report_independent_observer (vmB)";270    attribute :>> disposition = MiddlewareEvidenceDisposition::observedBounded;271    attribute :>> claimBoundary = "Direct campaign adapter path only; not bidirectional, production-deployment, lifecycle/update, safety, or certification evidence.";272  }273274  part runtimeAutowareConsumerEvidence013 : RetainedMiddlewareEvidence {275    doc /*276     * E-MW-013. A real autoware_vehicle_velocity_converter instance consumed277     * /vehicle/status/velocity_status and produced278     * /vehicle/status/twist_with_covariance with linear.x = 10.0 m/s and279     * covariance[0] = 0.04. This proves bounded Autoware-side consumption by280     * that node, not operation of the full Autoware stack.281     */282    attribute :>> configurationIdentity = "MW-CONFIG-001";283    attribute :>> executionEnvironmentIdentity = "gcp-europe-west4-a-de4sdv-aaos-build+de4sdv-ros2-autoware";284    attribute :>> contractIdentity = "autoware_vehicle_msgs/msg/VelocityReport -> geometry_msgs/msg/TwistWithCovarianceStamped";285    attribute :>> rawObservationArtifact = "implementation/aaos-sdv-reference-interop-bench/evidence/e-mw-013-autoware-consumer.yaml";286    attribute :>> independentObserverIdentity = "autoware_vehicle_velocity_converter output observation (vmB)";287    attribute :>> disposition = MiddlewareEvidenceDisposition::observedBounded;288    attribute :>> claimBoundary = "One real Autoware consumer and its converted output; not localization, planning, perception, control, safety, or certification evidence.";289  }290291  part runtimeHealthDispositionEvidence014 : RetainedMiddlewareEvidence {292    doc /*293     * E-MW-014. Provider loss produced an observable degraded=stale294     * disposition after the five-second freshness bound; provider restoration295     * produced restored=healthy and resumed 10.0 m/s publication. This closes296     * only the health-disposition subset of GAP-MW-028.297     */298    attribute :>> configurationIdentity = "MW-CONFIG-001";299    attribute :>> executionEnvironmentIdentity = "gcp-europe-west4-a-de4sdv-aaos-build+de4sdv-ros2-autoware";300    attribute :>> contractIdentity = "/vehicle/status/velocity_status provider-loss health disposition";301    attribute :>> rawObservationArtifact = "implementation/aaos-sdv-reference-interop-bench/evidence/e-mw-014-health-disposition.yaml";302    attribute :>> independentObserverIdentity = "retained VM-B bridge log and health-topic observation";303    attribute :>> disposition = MiddlewareEvidenceDisposition::observedBounded;304    attribute :>> claimBoundary = "Provider-loss degraded/restored disposition only; not complete lifecycle ordering, update/OTA, reverse-path, safety, or certification evidence.";305  }306307  part boundedBaselineDecision010 : IncrementLifecycleDecision {308    doc /*309     * BL-MW-010-P12. Phase 12 accepts the bounded forward Vehicle.Speed chain,310     * direct adapter path, independent ROS 2 observation, one real Autoware311     * consumer, invalid-envelope rejection, and provider-loss degraded/restored312     * health disposition demonstrated by E-MW-011 through E-MW-014.313     *314     * Complete lifecycle transition ordering (AC-MW-010-02), update/OTA315     * contract preservation (AC-MW-010-05), and the reverse lifecycle/status316     * path (gate 8) are deferred or not claimed. Production deployment, full317     * Autoware-stack, safety, certification, compliance, homologation, and318     * type-approval claims are also excluded. INC-MW-010 closes with these319     * residual counterclaims and gaps still explicit.320     */321  }322323  part successorIncrementDecision010 : IncrementLifecycleDecision {324    doc /*325     * Any stakeholder-visible Autoware-to-AAOS visualization and any reverse326     * transport used by it shall be framed as a separate capability increment.327     * It is not added to INC-MW-010 and does not retroactively satisfy gate 8.328     */329  }330331  part providerBindingEvidenceGap010 : DeferredProductLineScope {332    doc /* GAP-MW-025: Generated/usable VSIDL binding and deployed provider behavior remain unavailable. Campaign-chain subset observed (E-MW-011 gate 1: VehicleSpeedProvider:instance running); production adapter-chain binding remains open. */333  }334335  part crossDomainTransportEvidenceGap010 : DeferredProductLineScope {336    doc /* GAP-MW-026: Android/KVM-to-Linux/ROS 2 transport, discovery, and deployment evidence remain unavailable. Campaign-chain subset observed (E-MW-011 gates 3-5: discovery agent, forwarder accepts, exact topic); production adapter-chain transport remains open. */337  }338339  part independentAutowareObservationGap010 : DeferredProductLineScope {340    doc /* GAP-MW-027: Autoware-side provenance for /vehicle/status/velocity_status was unavailable; the campaign-chain subset was observed (E-MW-011 gate 6: independent observer validated 10.0 m/s). A real Autoware node (autoware_vehicle_velocity_converter) now consumes the topic and produces twist_with_covariance with linear.x = 10.0 m/s (E-MW-013); full Autoware stack provenance remains open. */341  }342343  part lifecycleUpdateFaultEvidenceGap010 : DeferredProductLineScope {344    doc /* GAP-MW-028: Target-runtime lifecycle, update/OTA, health, and fault evidence was unavailable. Fault subset observed (E-MW-011 gate 7: ingress rejects non-valid envelopes); health disposition now observed (E-MW-014: degraded=stale within 5s of provider loss, restored=healthy on resume — AC-MW-010-03 satisfied); lifecycle/update/OTA and reverse path remain open (gate 8 not claimed). */345  }346347  verification def SignalTranslationVerification {348    subject verifiedBench : MiddlewareIntegrationVandVBench;349    objective signalTranslationObjective010 {350      verify acceptanceCriterion010SignalTranslation;351      verify acceptanceCriterion010EvidenceIndependence;352    }353    action collectData {354      @VerificationMethod{ kind = (test, inspect); }355      out item retainedEvidence : RetainedMiddlewareEvidence;356    }357    action processData {358      @VerificationMethod{ kind = analyze; }359      in scenarioIdentity : MiddlewareScenarioIdentity = verifiedBench.scenario;360      in item retainedEvidence : RetainedMiddlewareEvidence = collectData.retainedEvidence;361      out item replayedEvaluation : ReplayedMiddlewareEvaluation;362    }363    action evaluateData {364      @VerificationMethod{ kind = analyze; }365      in item replayedEvaluation : ReplayedMiddlewareEvaluation = processData.replayedEvaluation;366      out verdict : VerdictKind = MapEvidenceOutcomeToVerdict(replayedEvaluation.outcome);367    }368    return verdict : VerdictKind = evaluateData.verdict;369  }370371  verification def LifecycleCoordinationVerification {372    subject verifiedBench : MiddlewareIntegrationVandVBench;373    objective lifecycleCoordinationObjective010 {374      verify acceptanceCriterion010LifecycleCoordination;375      verify acceptanceCriterion010EvidenceIndependence;376    }377    action collectData {378      @VerificationMethod{ kind = (test, inspect); }379      out item retainedEvidence : RetainedMiddlewareEvidence;380    }381    action processData {382      @VerificationMethod{ kind = analyze; }383      in scenarioIdentity : MiddlewareScenarioIdentity = verifiedBench.scenario;384      in item retainedEvidence : RetainedMiddlewareEvidence = collectData.retainedEvidence;385      out item replayedEvaluation : ReplayedMiddlewareEvaluation;386    }387    action evaluateData {388      @VerificationMethod{ kind = analyze; }389      in item replayedEvaluation : ReplayedMiddlewareEvaluation = processData.replayedEvaluation;390      out verdict : VerdictKind = MapEvidenceOutcomeToVerdict(replayedEvaluation.outcome);391    }392    return verdict : VerdictKind = evaluateData.verdict;393  }394395  verification def HealthForwardingVerification {396    subject verifiedBench : MiddlewareIntegrationVandVBench;397    objective healthForwardingObjective010 {398      verify acceptanceCriterion010HealthForwarding;399      verify acceptanceCriterion010EvidenceIndependence;400    }401    action collectData {402      @VerificationMethod{ kind = (test, inspect); }403      out item retainedEvidence : RetainedMiddlewareEvidence;404    }405    action processData {406      @VerificationMethod{ kind = analyze; }407      in scenarioIdentity : MiddlewareScenarioIdentity = verifiedBench.scenario;408      in item retainedEvidence : RetainedMiddlewareEvidence = collectData.retainedEvidence;409      out item replayedEvaluation : ReplayedMiddlewareEvaluation;410    }411    action evaluateData {412      @VerificationMethod{ kind = analyze; }413      in item replayedEvaluation : ReplayedMiddlewareEvaluation = processData.replayedEvaluation;414      out verdict : VerdictKind = MapEvidenceOutcomeToVerdict(replayedEvaluation.outcome);415    }416    return verdict : VerdictKind = evaluateData.verdict;417  }418419  verification def VehicleStartupValidation {420    doc /*421     * Modeled as a verification case over System 2 acceptance criteria422     * (SysML v2 provides no native validation-case keyword). Any validation423     * claim against stakeholder needs, intended use, and intended users424     * remains separately scoped and is not made by this case.425     */426    subject verifiedBench : MiddlewareIntegrationVandVBench;427    objective vehicleStartupObjective010 {428      verify acceptanceCriterion010VehicleStartup;429      verify acceptanceCriterion010LifecycleCoordination;430      verify acceptanceCriterion010EvidenceIndependence;431    }432    action collectData {433      @VerificationMethod{ kind = (test, inspect); }434      out item retainedEvidence : RetainedMiddlewareEvidence;435    }436    action processData {437      @VerificationMethod{ kind = analyze; }438      in scenarioIdentity : MiddlewareScenarioIdentity = verifiedBench.scenario;439      in item retainedEvidence : RetainedMiddlewareEvidence = collectData.retainedEvidence;440      out item replayedEvaluation : ReplayedMiddlewareEvaluation;441    }442    action evaluateData {443      @VerificationMethod{ kind = analyze; }444      in item replayedEvaluation : ReplayedMiddlewareEvaluation = processData.replayedEvaluation;445      out verdict : VerdictKind = MapEvidenceOutcomeToVerdict(replayedEvaluation.outcome);446    }447    return verdict : VerdictKind = evaluateData.verdict;448  }449450  verification def UpdateCoordinationValidation {451    doc /*452     * Modeled as a verification case over System 2 acceptance criteria453     * (SysML v2 provides no native validation-case keyword). Any validation454     * claim against stakeholder needs, intended use, and intended users455     * remains separately scoped and is not made by this case.456     */457    subject verifiedBench : MiddlewareIntegrationVandVBench;458    objective updateCoordinationObjective010 {459      verify acceptanceCriterion010UpdateCoordination;460      verify acceptanceCriterion010LifecycleCoordination;461      verify acceptanceCriterion010HealthForwarding;462      verify acceptanceCriterion010EvidenceIndependence;463    }464    action collectData {465      @VerificationMethod{ kind = (test, inspect); }466      out item retainedEvidence : RetainedMiddlewareEvidence;467    }468    action processData {469      @VerificationMethod{ kind = analyze; }470      in scenarioIdentity : MiddlewareScenarioIdentity = verifiedBench.scenario;471      in item retainedEvidence : RetainedMiddlewareEvidence = collectData.retainedEvidence;472      out item replayedEvaluation : ReplayedMiddlewareEvaluation;473    }474    action evaluateData {475      @VerificationMethod{ kind = analyze; }476      in item replayedEvaluation : ReplayedMiddlewareEvaluation = processData.replayedEvaluation;477      out verdict : VerdictKind = MapEvidenceOutcomeToVerdict(replayedEvaluation.outcome);478    }479    return verdict : VerdictKind = evaluateData.verdict;480  }481482  verification def FaultDetectionValidation {483    doc /*484     * Modeled as a verification case over System 2 acceptance criteria485     * (SysML v2 provides no native validation-case keyword). Any validation486     * claim against stakeholder needs, intended use, and intended users487     * remains separately scoped and is not made by this case.488     */489    subject verifiedBench : MiddlewareIntegrationVandVBench;490    objective faultDetectionObjective010 {491      verify acceptanceCriterion010FaultDetection;492      verify acceptanceCriterion010HealthForwarding;493      verify acceptanceCriterion010EvidenceIndependence;494    }495    action collectData {496      @VerificationMethod{ kind = (test, inspect); }497      out item retainedEvidence : RetainedMiddlewareEvidence;498    }499    action processData {500      @VerificationMethod{ kind = analyze; }501      in scenarioIdentity : MiddlewareScenarioIdentity = verifiedBench.scenario;502      in item retainedEvidence : RetainedMiddlewareEvidence = collectData.retainedEvidence;503      out item replayedEvaluation : ReplayedMiddlewareEvaluation;504    }505    action evaluateData {506      @VerificationMethod{ kind = analyze; }507      in item replayedEvaluation : ReplayedMiddlewareEvaluation = processData.replayedEvaluation;508      out verdict : VerdictKind = MapEvidenceOutcomeToVerdict(replayedEvaluation.outcome);509    }510    return verdict : VerdictKind = evaluateData.verdict;511  }512513  verification signalTranslationVerification010 : SignalTranslationVerification {514    @VerificationMethod{ kind = (test, inspect, analyze); }515    subject verifiedBench :> signalTranslationBench010;516  }517518  verification lifecycleCoordinationVerification010 : LifecycleCoordinationVerification {519    @VerificationMethod{ kind = (test, inspect, analyze); }520    subject verifiedBench :> lifecycleCoordinationBench010;521  }522523  verification healthForwardingVerification010 : HealthForwardingVerification {524    @VerificationMethod{ kind = (test, inspect, analyze); }525    subject verifiedBench :> healthForwardingBench010;526  }527528  verification vehicleStartupValidation010 : VehicleStartupValidation {529    @VerificationMethod{ kind = (test, inspect, analyze); }530    subject verifiedBench :> vehicleStartupBench010;531  }532533  verification updateCoordinationValidation010 : UpdateCoordinationValidation {534    @VerificationMethod{ kind = (test, inspect, analyze); }535    subject verifiedBench :> updateCoordinationBench010;536  }537538  verification faultDetectionValidation010 : FaultDetectionValidation {539    @VerificationMethod{ kind = (test, inspect, analyze); }540    subject verifiedBench :> faultDetectionBench010;541  }542543  part verificationSystem010 {544    perform signalTranslationVerification010;545    perform lifecycleCoordinationVerification010;546    perform healthForwardingVerification010;547    perform vehicleStartupValidation010;548    perform updateCoordinationValidation010;549    perform faultDetectionValidation010;550  }551552  dependency signalTranslationVerificationToRequirement553    from acceptanceCriterion010SignalTranslation554    to reqProvideMiddlewareSignalAccess;555  dependency lifecycleVerificationToRequirement556    from acceptanceCriterion010LifecycleCoordination557    to reqCoordinateMiddlewareLifecycle;558  dependency healthVerificationToRequirement559    from acceptanceCriterion010HealthForwarding560    to reqMonitorMiddlewareHealth;561  dependency startupValidationToDiscoveryRequirement562    from acceptanceCriterion010VehicleStartup563    to reqProvideServiceDiscovery;564  dependency startupValidationToLifecycleRequirement565    from acceptanceCriterion010VehicleStartup566    to reqCoordinateMiddlewareLifecycle;567  dependency updateValidationToRequirement568    from acceptanceCriterion010UpdateCoordination569    to reqCoordinateMiddlewareUpdates;570  dependency faultValidationToHealthRequirement571    from acceptanceCriterion010FaultDetection572    to reqMonitorMiddlewareHealth;573  dependency faultValidationToSafetyRequirement574    from acceptanceCriterion010FaultDetection575    to reqIsolateSafetyPath;576  dependency evidenceIndependenceToTraceabilityRequirement577    from acceptanceCriterion010EvidenceIndependence578    to reqMaintainMiddlewareBoundaryTraceability;579580  dependency verificationConfiguredMemberTrace581    from verificationSystem010582    to DE4SDV_MiddlewareVariabilityConfiguration::configuredMember;583  dependency verificationPhysicalBoundaryTrace584    from verificationSystem010585    to DE4SDV_MiddlewarePhysicalSoftwareRealization::physicalSoftware;586  dependency verificationSignalMappingTrace587    from signalTranslationVerification010588    to DE4SDV_MiddlewarePhysicalSoftwareRealization::physicalSoftware::adapter::aaosSignal::vehicleSpeed;589  dependency verificationContractTrace590    from signalTranslationVerification010591    to DE4SDV_MiddlewarePhysicalSoftwareRealization::physicalSoftwareSources::referenceInteropBenchSource;592  dependency verificationExecutionEnvironmentTrace593    from verificationSystem010594    to DE4SDV_MiddlewarePhysicalSoftwareRealization::aaosBuildRuntimeEnvironmentCandidate;595  dependency boundedBootBaselineTrace596    from boundedAAOSBootBaseline010597    to DE4SDV_MiddlewarePhysicalSoftwareRealization::physicalEnablingSystemGap;598  dependency providerBindingGapTrace599    from plannedTargetRuntimeEvidence010600    to providerBindingEvidenceGap010;601  dependency transportGapTrace602    from plannedTargetRuntimeEvidence010603    to crossDomainTransportEvidenceGap010;604  dependency independentObserverGapTrace605    from plannedTargetRuntimeEvidence010606    to independentAutowareObservationGap010;607  dependency lifecycleUpdateFaultGapTrace608    from plannedTargetRuntimeEvidence010609    to lifecycleUpdateFaultEvidenceGap010;610  dependency targetRuntimeEvidenceToPhase9Gap611    from plannedTargetRuntimeEvidence010612    to DE4SDV_MiddlewareVariabilityConfiguration::configuredRuntimeEvidenceGap;613  dependency targetRuntimeEvidenceToPhysicalSourceContractGap614    from plannedTargetRuntimeEvidence010615    to DE4SDV_MiddlewarePhysicalSoftwareRealization::physicalSourceContractGap;616  dependency targetRuntimeEvidenceToPhysicalProcessDeploymentGap617    from plannedTargetRuntimeEvidence010618    to DE4SDV_MiddlewarePhysicalSoftwareRealization::physicalProcessDeploymentGap;619  dependency targetRuntimeEvidenceToVelocitySignalContractGap620    from plannedTargetRuntimeEvidence010621    to DE4SDV_MiddlewarePhysicalSoftwareRealization::velocitySignalContractGap;622623  /* Claim-argument-evidence layer (INC-MW-010).624   *625   * The claim states what the configured member is asserted to realize within626   * the declared claim boundary. Arguments support the claim per verification627   * dimension. Counter-claims bound the claim where evidence is not yet628   * established (GAP-MW-025..028). Verification cases and evidence items629   * reinforce the arguments they are traced to. Planned or blocked evidence630   * never upgrades a verdict to pass.631   */632633  requirement def MiddlewareClaim634    :> EvidenceContractTraceabilityRequirementCandidate;635636  requirement def MiddlewareAssuranceArgument637    :> EvidenceContractTraceabilityRequirementCandidate;638639  requirement def MiddlewareCounterClaim640    :> EvidenceContractTraceabilityRequirementCandidate;641642  requirement mw010ReferenceContractClaim : MiddlewareClaim {643    doc /*644     * CLM-MW-010-01: for MW-CONFIG-001 on the retained two-VM execution645     * environment, the forward Vehicle.Speed slice was observed from the AAOS646     * provider through the direct adapter path to ROS 2, where one real647     * Autoware consumer produced the expected converted output. Invalid648     * envelopes were rejected and provider loss/restoration produced explicit649     * degraded/restored health dispositions.650     */651    subject claimSubject : MiddlewareIntegrationVandVBench;652    require constraint {653      doc /*654       * The claim requires retained E-MW-011 through E-MW-014 evidence bound to655       * the configured member, exact contracts, execution environment, and656       * observer identities. It excludes complete lifecycle ordering,657       * update/OTA, reverse-path, production, full-stack Autoware, safety, and658       * certification claims.659       */660    }661  }662663  requirement signalTranslationArgument010 : MiddlewareAssuranceArgument {664    doc /* AGT-MW-010-01: argues that AC-MW-010-01 (bounded signal translation semantics) is satisfied within the accepted claim boundary. */665    subject bench : MiddlewareIntegrationVandVBench;666  }667668  requirement lifecycleCoordinationArgument010 : MiddlewareAssuranceArgument {669    doc /* AGT-MW-010-02: records the AC-MW-010-02 verification branch; complete lifecycle transition ordering is deferred and does not support the accepted claim. */670    subject bench : MiddlewareIntegrationVandVBench;671  }672673  requirement healthForwardingArgument010 : MiddlewareAssuranceArgument {674    doc /* AGT-MW-010-03: argues that AC-MW-010-03 (provider-loss health disposition without relabeling) is satisfied within the accepted claim boundary. */675    subject bench : MiddlewareIntegrationVandVBench;676  }677678  requirement vehicleStartupArgument010 : MiddlewareAssuranceArgument {679    doc /* AGT-MW-010-04: argues that AC-MW-010-04 (bounded provider, registration, and discovery startup observations) is satisfied within the accepted claim boundary. */680    subject bench : MiddlewareIntegrationVandVBench;681  }682683  requirement updateCoordinationArgument010 : MiddlewareAssuranceArgument {684    doc /* AGT-MW-010-05: records the AC-MW-010-05 verification branch; update/OTA contract preservation is deferred and does not support the accepted claim. */685    subject bench : MiddlewareIntegrationVandVBench;686  }687688  requirement faultDetectionArgument010 : MiddlewareAssuranceArgument {689    doc /* AGT-MW-010-06: argues that AC-MW-010-06 (invalid-envelope rejection) is satisfied within the accepted claim boundary. */690    subject bench : MiddlewareIntegrationVandVBench;691  }692693  requirement counterClaim010ProviderBinding : MiddlewareCounterClaim {694    doc /* CCM-MW-010-01: bounds the claim for GAP-MW-025 scope (production adapter-chain provider binding; campaign-chain provider observed by E-MW-011). */695    subject bench : MiddlewareIntegrationVandVBench;696  }697698  requirement counterClaim010CrossDomainTransport : MiddlewareCounterClaim {699    doc /* CCM-MW-010-02: bounds the claim for GAP-MW-026 scope (production adapter-chain Android/KVM-to-Linux/ROS 2 transport; campaign-chain transport observed by E-MW-011). */700    subject bench : MiddlewareIntegrationVandVBench;701  }702703  requirement counterClaim010IndependentObservation : MiddlewareCounterClaim {704    doc /* CCM-MW-010-03: bounds the claim for GAP-MW-027 scope (full Autoware stack provenance; real consumer node observed by E-MW-013). */705    subject bench : MiddlewareIntegrationVandVBench;706  }707708  requirement counterClaim010LifecycleUpdateFault : MiddlewareCounterClaim {709    doc /* CCM-MW-010-04: bounds the claim for GAP-MW-028 scope (lifecycle, update/OTA, reverse path; fault rejection observed by E-MW-011 gate 7, health disposition observed by E-MW-014). */710    subject bench : MiddlewareIntegrationVandVBench;711  }712713  dependency claimSupportedBySignalArgument714    from signalTranslationArgument010 to mw010ReferenceContractClaim;715  dependency claimSupportedByHealthArgument716    from healthForwardingArgument010 to mw010ReferenceContractClaim;717  dependency claimSupportedByStartupArgument718    from vehicleStartupArgument010 to mw010ReferenceContractClaim;719  dependency claimSupportedByFaultArgument720    from faultDetectionArgument010 to mw010ReferenceContractClaim;721722  dependency signalVerificationReinforcesArgument723    from signalTranslationVerification010 to signalTranslationArgument010;724  dependency lifecycleVerificationReinforcesArgument725    from lifecycleCoordinationVerification010 to lifecycleCoordinationArgument010;726  dependency healthVerificationReinforcesArgument727    from healthForwardingVerification010 to healthForwardingArgument010;728  dependency startupValidationReinforcesArgument729    from vehicleStartupValidation010 to vehicleStartupArgument010;730  dependency updateValidationReinforcesArgument731    from updateCoordinationValidation010 to updateCoordinationArgument010;732  dependency faultValidationReinforcesArgument733    from faultDetectionValidation010 to faultDetectionArgument010;734735  dependency contractEvidenceReinforcesArgument736    from contractAndRehearsalEvidence010 to signalTranslationArgument010;737  dependency bootBaselineReinforcesArgument738    from boundedAAOSBootBaseline010 to vehicleStartupArgument010;739  dependency runtimeCampaignReinforcesSignalArgument740    from runtimeCampaignEvidence011 to signalTranslationArgument010;741  dependency runtimeCampaignReinforcesStartupArgument742    from runtimeCampaignEvidence011 to vehicleStartupArgument010;743  dependency runtimeCampaignReinforcesFaultArgument744    from runtimeCampaignEvidence011 to faultDetectionArgument010;745  dependency runtimeAdapterPathReinforcesSignalArgument746    from runtimeAdapterPathEvidence012 to signalTranslationArgument010;747  dependency runtimeAdapterPathReinforcesStartupArgument748    from runtimeAdapterPathEvidence012 to vehicleStartupArgument010;749  dependency runtimeAdapterPathReinforcesFaultArgument750    from runtimeAdapterPathEvidence012 to faultDetectionArgument010;751  dependency runtimeAutowareConsumerReinforcesSignalArgument752    from runtimeAutowareConsumerEvidence013 to signalTranslationArgument010;753  dependency runtimeHealthDispositionReinforcesHealthArgument754    from runtimeHealthDispositionEvidence014 to healthForwardingArgument010;755  dependency runtimeCampaignTraceToClaim756    from runtimeCampaignEvidence011 to mw010ReferenceContractClaim;757  dependency runtimeAdapterPathTraceToClaim758    from runtimeAdapterPathEvidence012 to mw010ReferenceContractClaim;759  dependency runtimeAutowareConsumerTraceToClaim760    from runtimeAutowareConsumerEvidence013 to mw010ReferenceContractClaim;761  dependency runtimeHealthDispositionTraceToClaim762    from runtimeHealthDispositionEvidence014 to mw010ReferenceContractClaim;763764  dependency counterClaimProviderBindingCountersClaim765    from counterClaim010ProviderBinding to mw010ReferenceContractClaim;766  dependency counterClaimTransportCountersClaim767    from counterClaim010CrossDomainTransport to mw010ReferenceContractClaim;768  dependency counterClaimObservationCountersClaim769    from counterClaim010IndependentObservation to mw010ReferenceContractClaim;770  dependency counterClaimLifecycleCountersClaim771    from counterClaim010LifecycleUpdateFault to mw010ReferenceContractClaim;772773  dependency counterClaimProviderBindingGapTrace774    from counterClaim010ProviderBinding to providerBindingEvidenceGap010;775  dependency counterClaimTransportGapTrace776    from counterClaim010CrossDomainTransport to crossDomainTransportEvidenceGap010;777  dependency counterClaimObservationGapTrace778    from counterClaim010IndependentObservation to independentAutowareObservationGap010;779  dependency counterClaimLifecycleGapTrace780    from counterClaim010LifecycleUpdateFault to lifecycleUpdateFaultEvidenceGap010;781782  dependency boundedClaimToBaselineDecision010783    from mw010ReferenceContractClaim to boundedBaselineDecision010;784  dependency runtimeCampaignToBaselineDecision010785    from runtimeCampaignEvidence011 to boundedBaselineDecision010;786  dependency runtimeAdapterPathToBaselineDecision010787    from runtimeAdapterPathEvidence012 to boundedBaselineDecision010;788  dependency runtimeAutowareConsumerToBaselineDecision010789    from runtimeAutowareConsumerEvidence013 to boundedBaselineDecision010;790  dependency runtimeHealthDispositionToBaselineDecision010791    from runtimeHealthDispositionEvidence014 to boundedBaselineDecision010;792  dependency deferredProviderCounterclaimToBaselineDecision010793    from counterClaim010ProviderBinding to boundedBaselineDecision010;794  dependency deferredTransportCounterclaimToBaselineDecision010795    from counterClaim010CrossDomainTransport to boundedBaselineDecision010;796  dependency deferredObservationCounterclaimToBaselineDecision010797    from counterClaim010IndependentObservation to boundedBaselineDecision010;798  dependency deferredLifecycleCounterclaimToBaselineDecision010799    from counterClaim010LifecycleUpdateFault to boundedBaselineDecision010;800  dependency successorIncrementToBaselineDecision010801    from successorIncrementDecision010 to boundedBaselineDecision010;802803  concern argumentationAssuranceConcern : ArgumentationAssuranceConcern {804    doc /* Evidence-based assurance claims, counterclaims, retained evidence, and the bounded baseline decision. */805    subject;806    stakeholder systemsEngineer : SystemsEngineer;807    stakeholder verificationEngineer : VerificationEngineer;808    stakeholder reviewer : OpenSourceReviewer;809  }810811  view middlewareVerificationAssuranceView {812    viewpoint selectedArgumentationAssuranceViewpoint : ArgumentationAssuranceViewpoint {813      frame argumentationAssuranceConcern;814    }815    doc /*816     * Positive Phase 12 slice: the bounded claim, retained evidence branches,817     * accepted baseline decision, and separately framed successor decision.818     * Open counterclaims and gaps are published separately.819     */820    expose boundedBaselineDecision010;821    expose successorIncrementDecision010;822    expose mw010ReferenceContractClaim;823    expose runtimeCampaignEvidence011;824    expose runtimeAdapterPathEvidence012;825    expose runtimeAutowareConsumerEvidence013;826    expose runtimeHealthDispositionEvidence014;827    expose signalTranslationArgument010;828    expose healthForwardingArgument010;829    expose vehicleStartupArgument010;830    expose faultDetectionArgument010;831    expose contractAndRehearsalEvidence010;832    expose boundedAAOSBootBaseline010;833    expose boundedClaimToBaselineDecision010;834    expose runtimeCampaignToBaselineDecision010;835    expose runtimeAdapterPathToBaselineDecision010;836    expose runtimeAutowareConsumerToBaselineDecision010;837    expose runtimeHealthDispositionToBaselineDecision010;838    expose successorIncrementToBaselineDecision010;839    attribute maxCompartmentEntries = 0;840    attribute showAnnotationRows = false;841    render asTreeDiagram;842  }843844  view middlewareOpenCounterclaimAssuranceView {845    viewpoint selectedOpenCounterclaimAssuranceViewpoint : ArgumentationAssuranceViewpoint {846      frame argumentationAssuranceConcern;847    }848    doc /*849     * Challenge slice: unresolved counterclaims and explicit gaps retained by850     * the bounded Phase 12 decision. They prevent broader production, full-851     * stack, lifecycle/update, and reverse-path assurance.852     */853    expose boundedBaselineDecision010;854    expose mw010ReferenceContractClaim;855    expose counterClaim010ProviderBinding;856    expose counterClaim010CrossDomainTransport;857    expose counterClaim010IndependentObservation;858    expose counterClaim010LifecycleUpdateFault;859    expose providerBindingEvidenceGap010;860    expose crossDomainTransportEvidenceGap010;861    expose independentAutowareObservationGap010;862    expose lifecycleUpdateFaultEvidenceGap010;863    expose counterClaimProviderBindingGapTrace;864    expose counterClaimTransportGapTrace;865    expose counterClaimObservationGapTrace;866    expose counterClaimLifecycleGapTrace;867    expose deferredProviderCounterclaimToBaselineDecision010;868    expose deferredTransportCounterclaimToBaselineDecision010;869    expose deferredObservationCounterclaimToBaselineDecision010;870    expose deferredLifecycleCounterclaimToBaselineDecision010;871    attribute maxCompartmentEntries = 0;872    attribute showAnnotationRows = false;873    render asTreeDiagram;874  }875}876