textual-notation-of-model/packages/features/aebs/aebs_override_verification.sysml
0 view(s) · 61 declared member(s)
Source
1/* INC-AEBS-009D conscious-override matrix; planned System 2 executable contracts. */2package DE4SDV_AEBSOverrideVerification {3 private import VerificationCases::*;4 private import VerificationMethodKind::*;5 private import DE4SDV_AEBSNeedsRequirements::Features::AEBS::NeedsRequirements::*;67 enum def OverrideScenarioIdentity {8 freshFalseControl;9 freshTrueOverride;10 staleOverride;11 missingOverride;12 malformedOverride;13 futureStampedOverride;14 }15 enum def OverrideEvidenceOutcome {16 passBoundedScenario;17 failObservedBehavior;18 inconclusiveCoverage;19 errorEvidence;20 }21 item def OverrideObservationSet;22 item def OverrideEvaluation {23 attribute scenario : OverrideScenarioIdentity;24 attribute outcome : OverrideEvidenceOutcome;25 }26 calc def MapOverrideOutcomeToVerdict {27 in outcome : OverrideEvidenceOutcome;28 return verdict : VerdictKind =29 if outcome == OverrideEvidenceOutcome::passBoundedScenario? VerdictKind::pass30 else if outcome == OverrideEvidenceOutcome::failObservedBehavior? VerdictKind::fail31 else if outcome == OverrideEvidenceOutcome::errorEvidence? VerdictKind::error32 else VerdictKind::inconclusive;33 }3435 part def OverrideMatrixBench {36 attribute scenario : OverrideScenarioIdentity;37 }38 requirement def OverrideEvidenceContract;39 requirement <'EC-009D-01'>evidenceContractClosedOverrideScenario : OverrideEvidenceContract {40 subject bench : OverrideMatrixBench;41 require constraint statement { language "English" /* The bench shall bind exactly one closed override scenario identity. */ }42 }43 requirement <'EC-009D-02'>evidenceContractOverrideFreshnessReplay : OverrideEvidenceContract {44 subject bench : OverrideMatrixBench;45 require constraint statement { language "English" /* The bench shall replay source stamp, receipt time, value validity, exact diagnostic-source authorization, and the scenario-specific suppression, release, or degraded disposition. A fresh sample is one with source-stamp-to-receipt age at most 0.2 s; suppression is evaluated within a closed window of 0.25 s; runtime-graph sampling gaps above 0.2 s fail the replay. */ }46 }47 requirement <'EC-009D-03'>evidenceContractIndependentVerdict : OverrideEvidenceContract {48 subject bench : OverrideMatrixBench;49 require constraint statement { language "English" /* The bench shall retain separate observations, evaluation, provenance, and verdict for each scenario; observer failure shall not pass. */ }50 }5152 part overrideFalseControlBench : OverrideMatrixBench {53 attribute :>> scenario = OverrideScenarioIdentity::freshFalseControl;54 }55 part overrideTrueBench : OverrideMatrixBench {56 attribute :>> scenario = OverrideScenarioIdentity::freshTrueOverride;57 }58 part overrideStaleBench : OverrideMatrixBench {59 attribute :>> scenario = OverrideScenarioIdentity::staleOverride;60 }61 part overrideMissingBench : OverrideMatrixBench {62 attribute :>> scenario = OverrideScenarioIdentity::missingOverride;63 }64 part overrideMalformedBench : OverrideMatrixBench {65 attribute :>> scenario = OverrideScenarioIdentity::malformedOverride;66 }67 part overrideFutureStampedBench : OverrideMatrixBench {68 attribute :>> scenario = OverrideScenarioIdentity::futureStampedOverride;69 }7071 verification def <'VC-AEBS-009D-DE'>ConsciousOverrideVerification {72 subject verifiedBench : OverrideMatrixBench;73 objective evidenceObjective {74 verify evidenceContractClosedOverrideScenario;75 verify evidenceContractOverrideFreshnessReplay;76 verify evidenceContractIndependentVerdict;77 }78 action collectData {79 @VerificationMethod{ kind = test; }80 out item retainedObservations : OverrideObservationSet;81 }82 action processData {83 @VerificationMethod{ kind = analyze; }84 in scenarioIdentity : OverrideScenarioIdentity = verifiedBench.scenario;85 in item retainedObservations : OverrideObservationSet = collectData.retainedObservations;86 out item replayedEvaluation : OverrideEvaluation;87 }88 action evaluateData {89 @VerificationMethod{ kind = analyze; }90 in item replayedEvaluation : OverrideEvaluation = processData.replayedEvaluation;91 out verdict : VerdictKind = MapOverrideOutcomeToVerdict(replayedEvaluation.outcome);92 }93 return verdict : VerdictKind = evaluateData.verdict;94 }95 verification <'VC-AEBS-009D-01'>overrideFalseControlVerification : ConsciousOverrideVerification {96 @VerificationMethod{ kind = (test, analyze); }97 subject verifiedBench :> overrideFalseControlBench;98 }99 verification <'VC-AEBS-009D-02'>overrideTrueVerification : ConsciousOverrideVerification {100 @VerificationMethod{ kind = (test, analyze); }101 subject verifiedBench :> overrideTrueBench;102 }103 verification <'VC-AEBS-009D-03'>overrideStaleVerification : ConsciousOverrideVerification {104 @VerificationMethod{ kind = (test, analyze); }105 subject verifiedBench :> overrideStaleBench;106 }107 verification <'VC-AEBS-009D-04'>overrideMissingVerification : ConsciousOverrideVerification {108 @VerificationMethod{ kind = (test, analyze); }109 subject verifiedBench :> overrideMissingBench;110 }111 verification <'VC-AEBS-009D-05'>overrideMalformedVerification : ConsciousOverrideVerification {112 @VerificationMethod{ kind = (test, analyze); }113 subject verifiedBench :> overrideMalformedBench;114 }115 verification <'VC-AEBS-009D-06'>overrideFutureStampedVerification : ConsciousOverrideVerification {116 @VerificationMethod{ kind = (test, analyze); }117 subject verifiedBench :> overrideFutureStampedBench;118 }119 part verificationSystem {120 perform overrideFalseControlVerification;121 perform overrideTrueVerification;122 perform overrideStaleVerification;123 perform overrideMissingVerification;124 perform overrideMalformedVerification;125 perform overrideFutureStampedVerification;126 }127128 dependency overrideEvidenceRelevantToOverrideCandidate129 from evidenceContractOverrideFreshnessReplay to reqAllowDriverOverride;130131 /* ─────────────────────────────────────────────────────────────────132 * Lane B: model-resident evaluation scope for the INC-AEBS-009D133 * method-conformance pilot (ADR 0019; docs/method-conformance/).134 *135 * The scope binds the six declared verification usages by their stable136 * explicit identifiers. Contribution set and evaluation scope are137 * distinct: the usages are reused scope members (contributes = false);138 * the scope binding itself is the increment's contribution.139 * ───────────────────────────────────────────────────────────────── */140 private import ScalarValues::*;141 private import DE4SDV_MethodProcess::*;142 private import DE4SDV_MethodConformance::*;143144 part def AebsOverridePilotScopeBase :> MethodEvaluationScope;145146 part <'PSC-009D'>aebsOverridePilotScope : AebsOverridePilotScopeBase {147 attribute :>> incrementId = "INC-AEBS-009D";148 attribute :>> subjectType = "VerificationCaseUsage";149 }150151 /* Evaluation-scope memberships: the six declared verification usages are152 reused scope members (contributes = false); the scope binding itself is153 the increment's contribution. Model-resident per Lane B-R5. */154 item scopeMember01 : EvaluationScopeMembership {155 attribute :>> scopeId = "PSC-009D";156 attribute :>> subjectId = "VC-AEBS-009D-01";157 attribute :>> contributes = false;158 }159 item scopeMember02 : EvaluationScopeMembership {160 attribute :>> scopeId = "PSC-009D";161 attribute :>> subjectId = "VC-AEBS-009D-02";162 attribute :>> contributes = false;163 }164 item scopeMember03 : EvaluationScopeMembership {165 attribute :>> scopeId = "PSC-009D";166 attribute :>> subjectId = "VC-AEBS-009D-03";167 attribute :>> contributes = false;168 }169 item scopeMember04 : EvaluationScopeMembership {170 attribute :>> scopeId = "PSC-009D";171 attribute :>> subjectId = "VC-AEBS-009D-04";172 attribute :>> contributes = false;173 }174 item scopeMember05 : EvaluationScopeMembership {175 attribute :>> scopeId = "PSC-009D";176 attribute :>> subjectId = "VC-AEBS-009D-05";177 attribute :>> contributes = false;178 }179 item scopeMember06 : EvaluationScopeMembership {180 attribute :>> scopeId = "PSC-009D";181 attribute :>> subjectId = "VC-AEBS-009D-06";182 attribute :>> contributes = false;183 }184185 /* Accepted method-contract obligations (PC-009D-*), instantiated from the186 accepted A specification (docs/method-conformance/pilot-obligations.yaml187 + pilot-scope.md). Dependency edges are normative in the YAML twin and188 the pilot-scope dependency graph; they are contract data here, not189 applicability conditions. */190 item obligationScopePopulation : MethodContractObligation {191 attribute :>> obligationId = "PC-009D-SCOPE-POPULATION";192 attribute :>> phase = MethodPhase::phase10_vvEvidence;193 attribute :>> subjectSelector = "the declared pilot scope itself";194 attribute :>> applicability = "candidate revision declares the INC-AEBS-009D pilot scope";195 attribute :>> minimumPopulation = 1;196 attribute :>> permittedEmpty = false;197 attribute :>> predicate = "scope-composition";198 attribute :>> targetFilter = "element type VerificationCaseUsage";199 attribute :>> cardinalityMinimum = 6;200 attribute :>> cardinalityMaximum = 6;201 attribute :>> required = true;202 attribute :>> evaluationSource = EvaluationSourceKind::pinnedModelRecord;203 attribute :>> attestationPolicyRef = "";204 attribute :>> claimBoundary = "declared scope resolves to exactly the six pinned usages as distinct identities";205 }206 item obligationVcBinding : MethodContractObligation {207 attribute :>> obligationId = "PC-009D-VC-BINDING";208 attribute :>> phase = MethodPhase::phase10_vvEvidence;209 attribute :>> subjectSelector = "each of the six declared usages (VerificationCaseUsage)";210 attribute :>> applicability = "candidate revision declares the INC-AEBS-009D pilot scope";211 attribute :>> minimumPopulation = 1;212 attribute :>> permittedEmpty = false;213 attribute :>> predicate = "binding-resolution";214 attribute :>> targetFilter = "API element";215 attribute :>> cardinalityMinimum = 1;216 attribute :>> cardinalityMaximum = 1;217 attribute :>> required = true;218 attribute :>> evaluationSource = EvaluationSourceKind::pinnedModelRecord;219 attribute :>> attestationPolicyRef = "";220 attribute :>> claimBoundary = "each usage binds to exactly one API element by explicit identifier";221 }222 item obligationSubjectMembership : MethodContractObligation {223 attribute :>> obligationId = "PC-009D-SUBJECT-MEMBERSHIP";224 attribute :>> phase = MethodPhase::phase10_vvEvidence;225 attribute :>> subjectSelector = "each of the six usages (VerificationCaseUsage)";226 attribute :>> applicability = "(no applicability condition)";227 attribute :>> minimumPopulation = 1;228 attribute :>> permittedEmpty = false;229 attribute :>> predicate = "verification-subject-membership";230 attribute :>> targetFilter = "member element type OverrideMatrixBench specialization";231 attribute :>> cardinalityMinimum = 1;232 attribute :>> cardinalityMaximum = 1;233 attribute :>> required = true;234 attribute :>> evaluationSource = EvaluationSourceKind::pinnedModelRecord;235 attribute :>> attestationPolicyRef = "";236 attribute :>> claimBoundary = "each usage has exactly one OverrideMatrixBench-specialization subject member";237 }238 item obligationObjectiveContracts : MethodContractObligation {239 attribute :>> obligationId = "PC-009D-OBJECTIVE-CONTRACTS";240 attribute :>> phase = MethodPhase::phase10_vvEvidence;241 attribute :>> subjectSelector = "each of the six usages (VerificationCaseUsage)";242 attribute :>> applicability = "(no applicability condition)";243 attribute :>> minimumPopulation = 1;244 attribute :>> permittedEmpty = false;245 attribute :>> predicate = "verifiedBy-reverse-witness";246 attribute :>> targetFilter = "the three pinned evidence-contract requirement usages";247 attribute :>> cardinalityMinimum = 3;248 attribute :>> cardinalityMaximum = 3;249 attribute :>> required = true;250 attribute :>> evaluationSource = EvaluationSourceKind::pinnedModelRecord;251 attribute :>> attestationPolicyRef = "";252 attribute :>> claimBoundary = "each usage inherits the objective verify witnesses to EC-009D-01..03";253 }254 item obligationUsageMethodMetadata : MethodContractObligation {255 attribute :>> obligationId = "PC-009D-USAGE-METHOD-METADATA";256 attribute :>> phase = MethodPhase::phase10_vvEvidence;257 attribute :>> subjectSelector = "each of the six usages (VerificationCaseUsage)";258 attribute :>> applicability = "(no applicability condition)";259 attribute :>> minimumPopulation = 1;260 attribute :>> permittedEmpty = false;261 attribute :>> predicate = "verification-method-metadata";262 attribute :>> targetFilter = "method-kind value set exactly {test, analyze}";263 attribute :>> cardinalityMinimum = 1;264 attribute :>> cardinalityMaximum = 1;265 attribute :>> required = true;266 attribute :>> evaluationSource = EvaluationSourceKind::pinnedModelRecord;267 attribute :>> attestationPolicyRef = "";268 attribute :>> claimBoundary = "each usage carries @VerificationMethod{kind=(test, analyze)}";269 }270 item obligationDefinitionMethodMetadata : MethodContractObligation {271 attribute :>> obligationId = "PC-009D-DEFINITION-METHOD-METADATA";272 attribute :>> phase = MethodPhase::phase10_vvEvidence;273 attribute :>> subjectSelector = "the shared verification definition ConsciousOverrideVerification (VerificationCaseDefinition)";274 attribute :>> applicability = "(no applicability condition)";275 attribute :>> minimumPopulation = 1;276 attribute :>> permittedEmpty = false;277 attribute :>> predicate = "verification-method-metadata";278 attribute :>> targetFilter = "per-action kind: collectData test; processData analyze; evaluateData analyze";279 attribute :>> cardinalityMinimum = 3;280 attribute :>> cardinalityMaximum = 3;281 attribute :>> required = true;282 attribute :>> evaluationSource = EvaluationSourceKind::pinnedModelRecord;283 attribute :>> attestationPolicyRef = "";284 attribute :>> claimBoundary = "the definition's three actions carry the declared method kinds";285 }286 item obligationProfilePopulation : MethodContractObligation {287 attribute :>> obligationId = "PC-009D-PROFILE-POPULATION";288 attribute :>> phase = MethodPhase::phase10_vvEvidence;289 attribute :>> subjectSelector = "the declared tested scope";290 attribute :>> applicability = "candidate declares the INC-AEBS-009D tested-scope manifest";291 attribute :>> minimumPopulation = 1;292 attribute :>> permittedEmpty = false;293 attribute :>> predicate = "scope-composition";294 attribute :>> targetFilter = "profile identity equality (pinned set, exact)";295 attribute :>> cardinalityMinimum = 6;296 attribute :>> cardinalityMaximum = 6;297 attribute :>> required = true;298 attribute :>> evaluationSource = EvaluationSourceKind::pinnedRepositoryArtifact;299 attribute :>> attestationPolicyRef = "";300 attribute :>> claimBoundary = "the declared tested scope contains exactly the six pinned OverrideScenario identities";301 }302 item obligationExecutionRecord : MethodContractObligation {303 attribute :>> obligationId = "PC-009D-EXECUTION-RECORD";304 attribute :>> phase = MethodPhase::phase10_vvEvidence;305 attribute :>> subjectSelector = "each profile in the declared tested scope";306 attribute :>> applicability = "(no applicability condition)";307 attribute :>> minimumPopulation = 1;308 attribute :>> permittedEmpty = false;309 attribute :>> predicate = "external-evidence-reference";310 attribute :>> targetFilter = "record integrity: sha256 of scenario-evidence.json matches the manifest entry";311 attribute :>> cardinalityMinimum = 1;312 attribute :>> cardinalityMaximum = 1;313 attribute :>> required = true;314 attribute :>> evaluationSource = EvaluationSourceKind::pinnedRepositoryArtifact;315 attribute :>> attestationPolicyRef = "";316 attribute :>> claimBoundary = "each profile has exactly one canonical record with manifest-verified digest";317 }318 item obligationExecutionOutcome : MethodContractObligation {319 attribute :>> obligationId = "PC-009D-EXECUTION-OUTCOME";320 attribute :>> phase = MethodPhase::phase10_vvEvidence;321 attribute :>> subjectSelector = "each profile's canonical record";322 attribute :>> applicability = "(no applicability condition)";323 attribute :>> minimumPopulation = 1;324 attribute :>> permittedEmpty = false;325 attribute :>> predicate = "execution-outcome";326 attribute :>> targetFilter = "disposition from the pinned OverrideDisposition vocabulary; unknown literal = ERROR";327 attribute :>> cardinalityMinimum = 1;328 attribute :>> cardinalityMaximum = 1;329 attribute :>> required = true;330 attribute :>> evaluationSource = EvaluationSourceKind::pinnedRepositoryArtifact;331 attribute :>> attestationPolicyRef = "";332 attribute :>> claimBoundary = "record evaluation.passed == true with the pinned per-profile expected disposition";333 }334 item obligationScopeEquality : MethodContractObligation {335 attribute :>> obligationId = "PC-009D-SCOPE-EQUALITY";336 attribute :>> phase = MethodPhase::phase10_vvEvidence;337 attribute :>> subjectSelector = "each profile's canonical record";338 attribute :>> applicability = "(no applicability condition)";339 attribute :>> minimumPopulation = 1;340 attribute :>> permittedEmpty = false;341 attribute :>> predicate = "conservative-scope-equality";342 attribute :>> targetFilter = "all pinned fields compared; no field may be skipped";343 attribute :>> cardinalityMinimum = 1;344 attribute :>> cardinalityMaximum = 1;345 attribute :>> required = true;346 attribute :>> evaluationSource = EvaluationSourceKind::pinnedRepositoryArtifact;347 attribute :>> attestationPolicyRef = "";348 attribute :>> claimBoundary = "pinned provenance fingerprint fields equal the candidate's declared tested-scope values";349 }350 item obligationAcceptanceAuthority : MethodContractObligation {351 attribute :>> obligationId = "PC-009D-ACCEPTANCE-AUTHORITY";352 attribute :>> phase = MethodPhase::phase10_vvEvidence;353 attribute :>> subjectSelector = "each profile's canonical record";354 attribute :>> applicability = "(no applicability condition)";355 attribute :>> minimumPopulation = 1;356 attribute :>> permittedEmpty = false;357 attribute :>> predicate = "acceptance-record-match";358 attribute :>> targetFilter = "decision population completeness over the closed six-profile universe";359 attribute :>> cardinalityMinimum = 1;360 attribute :>> cardinalityMaximum = 1;361 attribute :>> required = true;362 attribute :>> evaluationSource = EvaluationSourceKind::pinnedRepositoryArtifact;363 attribute :>> attestationPolicyRef = "de4sdv.acceptance.maintainer-decision.v1";364 attribute :>> claimBoundary = "an attributable authorized acceptance decision covers the profile under the proposed policy";365 }366367 /* Tested-scope declaration (candidate-declared comparison target). */368 item testedScope : TestedScopeDeclaration {369 attribute :>> executionHead = "01d9f586865bf7fb4bc0b3f76be2b5a916451da4";370 attribute :>> profileIdentities = "fresh_false_control, fresh_true_conscious_override, stale, missing, malformed, future_stamped";371 }372373 /* Acceptance attestation reference: policy identity + registry location.374 The policy is Proposed (not activated); the registry is currently375 absent — a missing registry is a distinct state, never an empty pass. */376 item acceptanceAttestation : AcceptanceAttestationReference {377 attribute :>> policyRef = "de4sdv.acceptance.maintainer-decision.v1";378 attribute :>> decisionRegistryPath = "docs/acceptance-decisions/";379 }380}381