textual-notation-of-model/packages/features/middleware/mw_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, evidence roles, and explicit claim boundary for the configured6 * Autoware + AndroidSDV member. It may be planned and exercised incrementally;7 * planned cases are not runtime passes.8 *9 * Contract tests and the bounded Cuttlefish boot record support lower-level10 * claims. Target-runtime provider, transport, ROS 2, Autoware, lifecycle,11 * update, and fault evidence remain blocked until the executable realization12 * and independent observation path exist.13 */1415package DE4SDV_MW010VerificationEvidence {16  private import DE4SDV_MethodContext::*;17  private import DE4SDV_MethodProcess::*;18  private import DE4SDV_ProductLine::*;19  private import DE4SDV_Stakeholders::*;20  private import DE4SDV_ExecutionEnvironments::*;21  private import DE4SDV_MWRequirements::Features::Middleware::Requirements::*;22  private import DE4SDV_MWFunctionalArchitecture::Features::Middleware::FunctionalArchitecture::*;23  private import DE4SDV_MWPhysicalSoftwareRealization::*;24  private import DE4SDV_MWVariabilityConfiguration::*;25  private import VerificationCases::*;26  private import VerificationMethodKind::*;27  private import ScalarValues::*;28  private import SAF_Viewpoints::*;29  private import Views::*;3031  part incMW010 : FeatureIncrement {32    doc /* INC-MW-010: middleware verification, validation, and evidence. */33  }3435  enum def ScenarioIdentity010 {36    signalTranslation;37    lifecycleCoordination;38    healthForwarding;39    vehicleStartup;40    updateCoordination;41    faultDetection;42  }4344  enum def EvidenceOutcome010 {45    passBoundedVerification;46    passBoundedValidation;47    failObservedBehavior;48    inconclusiveMissingEvidence;49    blockedTargetRuntime;50    errorEvidence;51  }5253  enum def EvidenceDisposition010 {54    planned;55    observedBounded;56    partial;57    blocked;58    accepted;59    rejected;60  }6162  item def VehicleSpeedTranslationObservation010 {63    attribute inputSpeedKmh : Real;64    attribute expectedVelocityMps : Real;65    attribute observedVelocityMps : Real;66    attribute sourceContractIdentity : String;67    attribute consumerContractIdentity : String;68    attribute independentObservation : Boolean;69  }7071  item def LifecycleObservation010 {72    attribute stateName : String;73    attribute predecessorState : String;74    attribute successorState : String;75    attribute transitionObserved : Boolean;76  }7778  item def HealthObservation010 {79    attribute healthState : String;80    attribute sourceFresh : Boolean;81    attribute forwarded : Boolean;82    attribute faultIdentity : String;83  }8485  item def RetainedMiddlewareEvidence010 {86    attribute configurationIdentity : String;87    attribute executionEnvironmentIdentity : String;88    attribute contractIdentity : String;89    attribute rawObservationArtifact : String;90    attribute independentObserverIdentity : String;91    attribute disposition : EvidenceDisposition010;92    attribute claimBoundary : String;93  }9495  item def ReplayedMiddlewareEvaluation010 {96    attribute scenario : ScenarioIdentity010;97    attribute outcome : EvidenceOutcome010;98    attribute acceptanceSummary : String;99  }100101  calc def Map010OutcomeToVerdict {102    in outcome : EvidenceOutcome010;103    return verdict : VerdictKind =104      if outcome == EvidenceOutcome010::passBoundedVerification? VerdictKind::pass105      else if outcome == EvidenceOutcome010::passBoundedValidation? VerdictKind::pass106      else if outcome == EvidenceOutcome010::failObservedBehavior? VerdictKind::fail107      else if outcome == EvidenceOutcome010::errorEvidence? VerdictKind::error108      else VerdictKind::inconclusive;109  }110111  part def MiddlewareIntegrationVandVBench010 {112    doc /*113     * System 1 is the configured member under evaluation. System 2 is the114     * engineering/build/test environment and is not a product selection.115     */116    part system1MemberProduct : MWAutowareAAOSSDVConfiguredMember;117    part system2TestEnvironment : AOSPAAOSBuildRuntimeEnvironment;118    attribute scenario : ScenarioIdentity010;119  }120121  part signalTranslationBench010 : MiddlewareIntegrationVandVBench010 {122    attribute :>> scenario = ScenarioIdentity010::signalTranslation;123  }124125  part lifecycleCoordinationBench010 : MiddlewareIntegrationVandVBench010 {126    attribute :>> scenario = ScenarioIdentity010::lifecycleCoordination;127  }128129  part healthForwardingBench010 : MiddlewareIntegrationVandVBench010 {130    attribute :>> scenario = ScenarioIdentity010::healthForwarding;131  }132133  part vehicleStartupBench010 : MiddlewareIntegrationVandVBench010 {134    attribute :>> scenario = ScenarioIdentity010::vehicleStartup;135  }136137  part updateCoordinationBench010 : MiddlewareIntegrationVandVBench010 {138    attribute :>> scenario = ScenarioIdentity010::updateCoordination;139  }140141  part faultDetectionBench010 : MiddlewareIntegrationVandVBench010 {142    attribute :>> scenario = ScenarioIdentity010::faultDetection;143  }144145  requirement def MiddlewareAcceptanceCriterion010146    :> EvidenceContractTraceabilityRequirementCandidate;147148  requirement acceptanceCriterion010SignalTranslation : MiddlewareAcceptanceCriterion010 {149    doc /* AC-MW-010-01; bounded verification of the selected Vehicle.Speed slice. */150    subject bench : MiddlewareIntegrationVandVBench010;151    require constraint {152      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. */153    }154  }155156  requirement acceptanceCriterion010LifecycleCoordination : MiddlewareAcceptanceCriterion010 {157    doc /* AC-MW-010-02; bounded verification of integration lifecycle behavior. */158    subject bench : MiddlewareIntegrationVandVBench010;159    require constraint {160      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. */161    }162  }163164  requirement acceptanceCriterion010HealthForwarding : MiddlewareAcceptanceCriterion010 {165    doc /* AC-MW-010-03; bounded verification of health forwarding. */166    subject bench : MiddlewareIntegrationVandVBench010;167    require constraint {168      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. */169    }170  }171172  requirement acceptanceCriterion010VehicleStartup : MiddlewareAcceptanceCriterion010 {173    doc /* AC-MW-010-04; validation of vehicle/application startup. */174    subject bench : MiddlewareIntegrationVandVBench010;175    require constraint {176      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. */177    }178  }179180  requirement acceptanceCriterion010UpdateCoordination : MiddlewareAcceptanceCriterion010 {181    doc /* AC-MW-010-05; validation of integration update behavior. */182    subject bench : MiddlewareIntegrationVandVBench010;183    require constraint {184      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. */185    }186  }187188  requirement acceptanceCriterion010FaultDetection : MiddlewareAcceptanceCriterion010 {189    doc /* AC-MW-010-06; validation of fault detection and containment. */190    subject bench : MiddlewareIntegrationVandVBench010;191    require constraint {192      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. */193    }194  }195196  requirement acceptanceCriterion010EvidenceIndependence : MiddlewareAcceptanceCriterion010 {197    doc /* AC-MW-010-07; evidence integrity and claim-boundary criterion. */198    subject bench : MiddlewareIntegrationVandVBench010;199    require constraint {200      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. */201    }202  }203204  part boundedAAOSBootBaseline010 : InspectedExecutionEnvironmentEvidence {205    doc /*206     * implementation/aaos-sdv-reference-interop-bench/evidence/207     * aaos-cuttlefish-cloud-proof.yaml. This is bounded x86_64 AOSP build and208     * Cuttlefish boot evidence; it is not provider, transport, ROS 2, Autoware,209     * lifecycle, update, fault, or vehicle interoperability evidence.210     */211  }212213  part contractAndRehearsalEvidence010 : ExecutionEnvironmentEvidenceArtifact {214    doc /*215     * Existing reference-contract and provider-neutral adapter tests support216     * contract and conversion claims only. They are not target-runtime proof.217     */218  }219220  part plannedTargetRuntimeEvidence010 : PlannedExecutionEnvironmentEvidence {221    doc /*222     * Planned evidence for provider binding, deployment, discovery, transport,223     * ROS 2 publication, independent Autoware observation, and lifecycle/fault224     * scenarios on the configured member.225     */226  }227228  part providerBindingEvidenceGap010 : DeferredProductLineScope {229    doc /* GAP-MW-025: Generated/usable VSIDL binding and deployed provider behavior remain unavailable. */230  }231232  part crossDomainTransportEvidenceGap010 : DeferredProductLineScope {233    doc /* GAP-MW-026: Android/KVM-to-Linux/ROS 2 transport, discovery, and deployment evidence remain unavailable. */234  }235236  part independentAutowareObservationGap010 : DeferredProductLineScope {237    doc /* GAP-MW-027: An independent observation of /vehicle/status/velocity_status and Autoware-side provenance remains unavailable. */238  }239240  part lifecycleUpdateFaultEvidenceGap010 : DeferredProductLineScope {241    doc /* GAP-MW-028: Target-runtime lifecycle, update/OTA, health, and fault evidence remains unavailable. */242  }243244  verification def SignalTranslationVerification010 {245    subject verifiedBench : MiddlewareIntegrationVandVBench010;246    objective signalTranslationObjective010 {247      verify acceptanceCriterion010SignalTranslation;248      verify acceptanceCriterion010EvidenceIndependence;249    }250    action collectData {251      @VerificationMethod{ kind = (test, inspect); }252      out item retainedEvidence : RetainedMiddlewareEvidence010;253    }254    action processData {255      @VerificationMethod{ kind = analyze; }256      in scenarioIdentity : ScenarioIdentity010 = verifiedBench.scenario;257      in item retainedEvidence : RetainedMiddlewareEvidence010 = collectData.retainedEvidence;258      out item replayedEvaluation : ReplayedMiddlewareEvaluation010;259    }260    action evaluateData {261      @VerificationMethod{ kind = analyze; }262      in item replayedEvaluation : ReplayedMiddlewareEvaluation010 = processData.replayedEvaluation;263      out verdict : VerdictKind = Map010OutcomeToVerdict(replayedEvaluation.outcome);264    }265    return verdict : VerdictKind = evaluateData.verdict;266  }267268  verification def LifecycleCoordinationVerification010 {269    subject verifiedBench : MiddlewareIntegrationVandVBench010;270    objective lifecycleCoordinationObjective010 {271      verify acceptanceCriterion010LifecycleCoordination;272      verify acceptanceCriterion010EvidenceIndependence;273    }274    action collectData {275      @VerificationMethod{ kind = (test, inspect); }276      out item retainedEvidence : RetainedMiddlewareEvidence010;277    }278    action processData {279      @VerificationMethod{ kind = analyze; }280      in scenarioIdentity : ScenarioIdentity010 = verifiedBench.scenario;281      in item retainedEvidence : RetainedMiddlewareEvidence010 = collectData.retainedEvidence;282      out item replayedEvaluation : ReplayedMiddlewareEvaluation010;283    }284    action evaluateData {285      @VerificationMethod{ kind = analyze; }286      in item replayedEvaluation : ReplayedMiddlewareEvaluation010 = processData.replayedEvaluation;287      out verdict : VerdictKind = Map010OutcomeToVerdict(replayedEvaluation.outcome);288    }289    return verdict : VerdictKind = evaluateData.verdict;290  }291292  verification def HealthForwardingVerification010 {293    subject verifiedBench : MiddlewareIntegrationVandVBench010;294    objective healthForwardingObjective010 {295      verify acceptanceCriterion010HealthForwarding;296      verify acceptanceCriterion010EvidenceIndependence;297    }298    action collectData {299      @VerificationMethod{ kind = (test, inspect); }300      out item retainedEvidence : RetainedMiddlewareEvidence010;301    }302    action processData {303      @VerificationMethod{ kind = analyze; }304      in scenarioIdentity : ScenarioIdentity010 = verifiedBench.scenario;305      in item retainedEvidence : RetainedMiddlewareEvidence010 = collectData.retainedEvidence;306      out item replayedEvaluation : ReplayedMiddlewareEvaluation010;307    }308    action evaluateData {309      @VerificationMethod{ kind = analyze; }310      in item replayedEvaluation : ReplayedMiddlewareEvaluation010 = processData.replayedEvaluation;311      out verdict : VerdictKind = Map010OutcomeToVerdict(replayedEvaluation.outcome);312    }313    return verdict : VerdictKind = evaluateData.verdict;314  }315316  verification def VehicleStartupValidation010 {317    subject verifiedBench : MiddlewareIntegrationVandVBench010;318    objective vehicleStartupObjective010 {319      verify acceptanceCriterion010VehicleStartup;320      verify acceptanceCriterion010LifecycleCoordination;321      verify acceptanceCriterion010EvidenceIndependence;322    }323    action collectData {324      @VerificationMethod{ kind = (test, inspect); }325      out item retainedEvidence : RetainedMiddlewareEvidence010;326    }327    action processData {328      @VerificationMethod{ kind = analyze; }329      in scenarioIdentity : ScenarioIdentity010 = verifiedBench.scenario;330      in item retainedEvidence : RetainedMiddlewareEvidence010 = collectData.retainedEvidence;331      out item replayedEvaluation : ReplayedMiddlewareEvaluation010;332    }333    action evaluateData {334      @VerificationMethod{ kind = analyze; }335      in item replayedEvaluation : ReplayedMiddlewareEvaluation010 = processData.replayedEvaluation;336      out verdict : VerdictKind = Map010OutcomeToVerdict(replayedEvaluation.outcome);337    }338    return verdict : VerdictKind = evaluateData.verdict;339  }340341  verification def UpdateCoordinationValidation010 {342    subject verifiedBench : MiddlewareIntegrationVandVBench010;343    objective updateCoordinationObjective010 {344      verify acceptanceCriterion010UpdateCoordination;345      verify acceptanceCriterion010LifecycleCoordination;346      verify acceptanceCriterion010HealthForwarding;347      verify acceptanceCriterion010EvidenceIndependence;348    }349    action collectData {350      @VerificationMethod{ kind = (test, inspect); }351      out item retainedEvidence : RetainedMiddlewareEvidence010;352    }353    action processData {354      @VerificationMethod{ kind = analyze; }355      in scenarioIdentity : ScenarioIdentity010 = verifiedBench.scenario;356      in item retainedEvidence : RetainedMiddlewareEvidence010 = collectData.retainedEvidence;357      out item replayedEvaluation : ReplayedMiddlewareEvaluation010;358    }359    action evaluateData {360      @VerificationMethod{ kind = analyze; }361      in item replayedEvaluation : ReplayedMiddlewareEvaluation010 = processData.replayedEvaluation;362      out verdict : VerdictKind = Map010OutcomeToVerdict(replayedEvaluation.outcome);363    }364    return verdict : VerdictKind = evaluateData.verdict;365  }366367  verification def FaultDetectionValidation010 {368    subject verifiedBench : MiddlewareIntegrationVandVBench010;369    objective faultDetectionObjective010 {370      verify acceptanceCriterion010FaultDetection;371      verify acceptanceCriterion010HealthForwarding;372      verify acceptanceCriterion010EvidenceIndependence;373    }374    action collectData {375      @VerificationMethod{ kind = (test, inspect); }376      out item retainedEvidence : RetainedMiddlewareEvidence010;377    }378    action processData {379      @VerificationMethod{ kind = analyze; }380      in scenarioIdentity : ScenarioIdentity010 = verifiedBench.scenario;381      in item retainedEvidence : RetainedMiddlewareEvidence010 = collectData.retainedEvidence;382      out item replayedEvaluation : ReplayedMiddlewareEvaluation010;383    }384    action evaluateData {385      @VerificationMethod{ kind = analyze; }386      in item replayedEvaluation : ReplayedMiddlewareEvaluation010 = processData.replayedEvaluation;387      out verdict : VerdictKind = Map010OutcomeToVerdict(replayedEvaluation.outcome);388    }389    return verdict : VerdictKind = evaluateData.verdict;390  }391392  verification signalTranslationVerification010 : SignalTranslationVerification010 {393    @VerificationMethod{ kind = (test, inspect, analyze); }394    subject verifiedBench :> signalTranslationBench010;395  }396397  verification lifecycleCoordinationVerification010 : LifecycleCoordinationVerification010 {398    @VerificationMethod{ kind = (test, inspect, analyze); }399    subject verifiedBench :> lifecycleCoordinationBench010;400  }401402  verification healthForwardingVerification010 : HealthForwardingVerification010 {403    @VerificationMethod{ kind = (test, inspect, analyze); }404    subject verifiedBench :> healthForwardingBench010;405  }406407  verification vehicleStartupValidation010 : VehicleStartupValidation010 {408    @VerificationMethod{ kind = (test, inspect, analyze); }409    subject verifiedBench :> vehicleStartupBench010;410  }411412  verification updateCoordinationValidation010 : UpdateCoordinationValidation010 {413    @VerificationMethod{ kind = (test, inspect, analyze); }414    subject verifiedBench :> updateCoordinationBench010;415  }416417  verification faultDetectionValidation010 : FaultDetectionValidation010 {418    @VerificationMethod{ kind = (test, inspect, analyze); }419    subject verifiedBench :> faultDetectionBench010;420  }421422  part verificationSystem010 {423    perform signalTranslationVerification010;424    perform lifecycleCoordinationVerification010;425    perform healthForwardingVerification010;426    perform vehicleStartupValidation010;427    perform updateCoordinationValidation010;428    perform faultDetectionValidation010;429  }430431  dependency signalTranslationVerificationToRequirement432    from acceptanceCriterion010SignalTranslation433    to reqProvideMiddlewareSignalAccess;434  dependency lifecycleVerificationToRequirement435    from acceptanceCriterion010LifecycleCoordination436    to reqCoordinateMiddlewareLifecycle;437  dependency healthVerificationToRequirement438    from acceptanceCriterion010HealthForwarding439    to reqMonitorMiddlewareHealth;440  dependency startupValidationToDiscoveryRequirement441    from acceptanceCriterion010VehicleStartup442    to reqProvideServiceDiscovery;443  dependency startupValidationToLifecycleRequirement444    from acceptanceCriterion010VehicleStartup445    to reqCoordinateMiddlewareLifecycle;446  dependency updateValidationToRequirement447    from acceptanceCriterion010UpdateCoordination448    to reqCoordinateMiddlewareUpdates;449  dependency faultValidationToHealthRequirement450    from acceptanceCriterion010FaultDetection451    to reqMonitorMiddlewareHealth;452  dependency faultValidationToSafetyRequirement453    from acceptanceCriterion010FaultDetection454    to reqIsolateSafetyPath;455  dependency evidenceIndependenceToTraceabilityRequirement456    from acceptanceCriterion010EvidenceIndependence457    to reqMaintainMiddlewareBoundaryTraceability;458459  dependency verificationConfiguredMemberTrace460    from verificationSystem010461    to DE4SDV_MWVariabilityConfiguration::configuredMember;462  dependency verificationPhysicalBoundaryTrace463    from verificationSystem010464    to DE4SDV_MWPhysicalSoftwareRealization::physicalSoftware;465  dependency verificationSignalMappingTrace466    from signalTranslationVerification010467    to DE4SDV_MWPhysicalSoftwareRealization::physicalSoftware::adapter::aaosSignal::vehicleSpeed;468  dependency verificationContractTrace469    from signalTranslationVerification010470    to DE4SDV_MWPhysicalSoftwareRealization::physicalSoftwareSources::referenceInteropBenchSource;471  dependency verificationExecutionEnvironmentTrace472    from verificationSystem010473    to DE4SDV_MWPhysicalSoftwareRealization::aaosBuildRuntimeEnvironmentCandidate;474  dependency boundedBootBaselineTrace475    from boundedAAOSBootBaseline010476    to DE4SDV_MWPhysicalSoftwareRealization::physicalEnablingSystemGap;477  dependency providerBindingGapTrace478    from plannedTargetRuntimeEvidence010479    to providerBindingEvidenceGap010;480  dependency transportGapTrace481    from plannedTargetRuntimeEvidence010482    to crossDomainTransportEvidenceGap010;483  dependency independentObserverGapTrace484    from plannedTargetRuntimeEvidence010485    to independentAutowareObservationGap010;486  dependency lifecycleUpdateFaultGapTrace487    from plannedTargetRuntimeEvidence010488    to lifecycleUpdateFaultEvidenceGap010;489  dependency targetRuntimeEvidenceToPhase9Gap490    from plannedTargetRuntimeEvidence010491    to DE4SDV_MWVariabilityConfiguration::configuredRuntimeEvidenceGap;492  dependency targetRuntimeEvidenceToPhysicalSourceContractGap493    from plannedTargetRuntimeEvidence010494    to DE4SDV_MWPhysicalSoftwareRealization::physicalSourceContractGap;495  dependency targetRuntimeEvidenceToPhysicalProcessDeploymentGap496    from plannedTargetRuntimeEvidence010497    to DE4SDV_MWPhysicalSoftwareRealization::physicalProcessDeploymentGap;498  dependency targetRuntimeEvidenceToVelocitySignalContractGap499    from plannedTargetRuntimeEvidence010500    to DE4SDV_MWPhysicalSoftwareRealization::velocitySignalContractGap;501502  /* Claim-argument-evidence layer (INC-MW-010).503   *504   * The claim states what the configured member is asserted to realize within505   * the declared claim boundary. Arguments support the claim per verification506   * dimension. Counter-claims bound the claim where evidence is not yet507   * established (GAP-MW-025..028). Verification cases and evidence items508   * reinforce the arguments they are traced to. Planned or blocked evidence509   * never upgrades a verdict to pass.510   */511512  requirement def MiddlewareClaim010513    :> EvidenceContractTraceabilityRequirementCandidate;514515  requirement def MiddlewareArgument010516    :> EvidenceContractTraceabilityRequirementCandidate;517518  requirement def MiddlewareCounterClaim010519    :> EvidenceContractTraceabilityRequirementCandidate;520521  requirement mw010ReferenceContractClaim : MiddlewareClaim010 {522    doc /*523     * CLM-MW-010-01: the configured Autoware + AndroidSDV member realizes the524     * Vehicle.Speed reference contract within the declared claim boundary:525     * signal translation semantics, lifecycle coordination, health forwarding,526     * startup and update coordination, and fault containment are observable,527     * replayable, and independently observed.528     */529    subject claimSubject : MiddlewareIntegrationVandVBench010;530    require constraint {531      doc /* The claim is bounded by retained, replayable, independently532        observed evidence bound to the configured member, execution533        environment, and contract identities. It is not target-runtime proof. */534    }535  }536537  requirement signalTranslationArgument010 : MiddlewareArgument010 {538    doc /* AGT-MW-010-01: argues that AC-MW-010-01 (bounded signal translation semantics) is satisfied within the claim boundary. */539    subject bench : MiddlewareIntegrationVandVBench010;540  }541542  requirement lifecycleCoordinationArgument010 : MiddlewareArgument010 {543    doc /* AGT-MW-010-02: argues that AC-MW-010-02 (observable integration lifecycle coordination) is satisfied within the claim boundary. */544    subject bench : MiddlewareIntegrationVandVBench010;545  }546547  requirement healthForwardingArgument010 : MiddlewareArgument010 {548    doc /* AGT-MW-010-03: argues that AC-MW-010-03 (health forwarding without relabeling) is satisfied within the claim boundary. */549    subject bench : MiddlewareIntegrationVandVBench010;550  }551552  requirement vehicleStartupArgument010 : MiddlewareArgument010 {553    doc /* AGT-MW-010-04: argues that AC-MW-010-04 (causally ordered startup readiness) is satisfied within the claim boundary. */554    subject bench : MiddlewareIntegrationVandVBench010;555  }556557  requirement updateCoordinationArgument010 : MiddlewareArgument010 {558    doc /* AGT-MW-010-05: argues that AC-MW-010-05 (update coordination with identity retention) is satisfied within the claim boundary. */559    subject bench : MiddlewareIntegrationVandVBench010;560  }561562  requirement faultDetectionArgument010 : MiddlewareArgument010 {563    doc /* AGT-MW-010-06: argues that AC-MW-010-06 (fault detection and containment) is satisfied within the claim boundary. */564    subject bench : MiddlewareIntegrationVandVBench010;565  }566567  requirement counterClaim010ProviderBinding : MiddlewareCounterClaim010 {568    doc /* CCM-MW-010-01: bounds the claim for GAP-MW-025 scope (provider binding and deployed provider behavior). */569    subject bench : MiddlewareIntegrationVandVBench010;570  }571572  requirement counterClaim010CrossDomainTransport : MiddlewareCounterClaim010 {573    doc /* CCM-MW-010-02: bounds the claim for GAP-MW-026 scope (Android/KVM-to-Linux/ROS 2 transport, discovery, deployment). */574    subject bench : MiddlewareIntegrationVandVBench010;575  }576577  requirement counterClaim010IndependentObservation : MiddlewareCounterClaim010 {578    doc /* CCM-MW-010-03: bounds the claim for GAP-MW-027 scope (independent Autoware observation). */579    subject bench : MiddlewareIntegrationVandVBench010;580  }581582  requirement counterClaim010LifecycleUpdateFault : MiddlewareCounterClaim010 {583    doc /* CCM-MW-010-04: bounds the claim for GAP-MW-028 scope (target-runtime lifecycle, update/OTA, health, fault). */584    subject bench : MiddlewareIntegrationVandVBench010;585  }586587  dependency claimSupportedBySignalArgument588    from signalTranslationArgument010 to mw010ReferenceContractClaim;589  dependency claimSupportedByLifecycleArgument590    from lifecycleCoordinationArgument010 to mw010ReferenceContractClaim;591  dependency claimSupportedByHealthArgument592    from healthForwardingArgument010 to mw010ReferenceContractClaim;593  dependency claimSupportedByStartupArgument594    from vehicleStartupArgument010 to mw010ReferenceContractClaim;595  dependency claimSupportedByUpdateArgument596    from updateCoordinationArgument010 to mw010ReferenceContractClaim;597  dependency claimSupportedByFaultArgument598    from faultDetectionArgument010 to mw010ReferenceContractClaim;599600  dependency signalVerificationReinforcesArgument601    from signalTranslationVerification010 to signalTranslationArgument010;602  dependency lifecycleVerificationReinforcesArgument603    from lifecycleCoordinationVerification010 to lifecycleCoordinationArgument010;604  dependency healthVerificationReinforcesArgument605    from healthForwardingVerification010 to healthForwardingArgument010;606  dependency startupValidationReinforcesArgument607    from vehicleStartupValidation010 to vehicleStartupArgument010;608  dependency updateValidationReinforcesArgument609    from updateCoordinationValidation010 to updateCoordinationArgument010;610  dependency faultValidationReinforcesArgument611    from faultDetectionValidation010 to faultDetectionArgument010;612613  dependency contractEvidenceReinforcesArgument614    from contractAndRehearsalEvidence010 to signalTranslationArgument010;615  dependency bootBaselineReinforcesArgument616    from boundedAAOSBootBaseline010 to vehicleStartupArgument010;617618  dependency counterClaimProviderBindingCountersClaim619    from counterClaim010ProviderBinding to mw010ReferenceContractClaim;620  dependency counterClaimTransportCountersClaim621    from counterClaim010CrossDomainTransport to mw010ReferenceContractClaim;622  dependency counterClaimObservationCountersClaim623    from counterClaim010IndependentObservation to mw010ReferenceContractClaim;624  dependency counterClaimLifecycleCountersClaim625    from counterClaim010LifecycleUpdateFault to mw010ReferenceContractClaim;626627  dependency counterClaimProviderBindingGapTrace628    from counterClaim010ProviderBinding to providerBindingEvidenceGap010;629  dependency counterClaimTransportGapTrace630    from counterClaim010CrossDomainTransport to crossDomainTransportEvidenceGap010;631  dependency counterClaimObservationGapTrace632    from counterClaim010IndependentObservation to independentAutowareObservationGap010;633  dependency counterClaimLifecycleGapTrace634    from counterClaim010LifecycleUpdateFault to lifecycleUpdateFaultEvidenceGap010;635636  concern argumentationAssuranceConcern : ArgumentationAssuranceConcern {637    doc /* Evidence-based assurance claims and their supporting argumentation. */638    subject;639    stakeholder systemsEngineer : SystemsEngineer;640    stakeholder verificationEngineer : VerificationEngineer;641    stakeholder reviewer : OpenSourceReviewer;642  }643644  view mw010VerificationAssuranceView {645    viewpoint selectedArgumentationAssuranceViewpoint : ArgumentationAssuranceViewpoint {646      frame argumentationAssuranceConcern;647    }648    doc /*649     * Positive evidence slice: the claim branches that currently have retained650     * evidence. Open counterclaims and gaps are published separately.651     */652    expose mw010ReferenceContractClaim;653    expose signalTranslationArgument010;654    expose vehicleStartupArgument010;655    expose contractAndRehearsalEvidence010;656    expose boundedAAOSBootBaseline010;657    expose claimSupportedBySignalArgument;658    expose claimSupportedByStartupArgument;659    expose contractEvidenceReinforcesArgument;660    expose bootBaselineReinforcesArgument;661    attribute maxCompartmentEntries = 0;662    attribute showAnnotationRows = false;663    render asTreeDiagram;664  }665666  view mw010OpenCounterclaimAssuranceView {667    viewpoint selectedOpenCounterclaimAssuranceViewpoint : ArgumentationAssuranceViewpoint {668      frame argumentationAssuranceConcern;669    }670    doc /*671     * Challenge slice: unresolved counterclaims against the reference claim and672     * the explicit evidence gaps that prevent target-runtime assurance.673     */674    expose mw010ReferenceContractClaim;675    expose counterClaim010ProviderBinding;676    expose counterClaim010CrossDomainTransport;677    expose counterClaim010IndependentObservation;678    expose counterClaim010LifecycleUpdateFault;679    expose providerBindingEvidenceGap010;680    expose crossDomainTransportEvidenceGap010;681    expose independentAutowareObservationGap010;682    expose lifecycleUpdateFaultEvidenceGap010;683    expose counterClaimProviderBindingCountersClaim;684    expose counterClaimTransportCountersClaim;685    expose counterClaimObservationCountersClaim;686    expose counterClaimLifecycleCountersClaim;687    expose counterClaimProviderBindingGapTrace;688    expose counterClaimTransportGapTrace;689    expose counterClaimObservationGapTrace;690    expose counterClaimLifecycleGapTrace;691    attribute maxCompartmentEntries = 0;692    attribute showAnnotationRows = false;693    render asTreeDiagram;694  }695}696