PaperlayerView exact revision on arXiv

Source-linked AI summary

Contract-Based Agentic Systems Engineering: Delegation as Quotient for Assured System Design

Sai Sandeep Damera, Ryan Matheu, John S. Baras

arXiv:2610.33349v1eess.SYcs.ROcs.SY

TL;DR

A delegated component can satisfy its prompt while violating assumptions made by fixed neighbors, and ordinary tests with ideal stand-ins do not expose that failure. The paper computes a SysML v2 contract quotient as the component’s requirement and tests language-model deliveries on live warehouse-robot episodes. The quotient-selected design met the system and dispatched requirements in all 30 episodes, while mission-only and natural-language selections missed dispatched obligations in some episodes.

  • Problem

    A component can satisfy its local requirement yet break a fixed neighbor’s assumption, causing system failure that unit tests with ideal stand-ins do not exercise.

    Source: §1 · p. 3

  • Method

    The paper models system and fixed-component contracts in SysML v2 and computes their quotient to derive the most permissive sound requirement for the delegated component.

    Source: §1 · p. 3, §4.1 · p. 8

  • Results

    The quotient-selected design met the system and dispatched requirements in all 30 episodes, while mission-only selections missed the dispatched requirement in 1 and 9 episodes and the natural-language selection missed it in 9.

    Source: §6.5 · p. 18

  • Takeaways & Limitations

    In the simulated warehouse-robot case, the quotient-derived requirement distinguished preservation obligations that mission-only and natural-language tasks did not state.

    Source: §4.2 · p. 9, §6.5 · p. 18

    A consistent quotient can still be unrealizable because the contract algebra does not encode the causality needed for a component to produce behavior from its observations.

    Source: §4.4 · p. 12

Abstract

from arXiv · show

A component an agent builds from a prompt can satisfy it and still break the system it joins, because the prompt omits what its neighbours assume of it. The artifact to hand over is computed, not written. A SysML v2 requirement with assumed and required constraints is an assume/guarantee contract, so when a system requirement is decomposed over fixed neighbours, the open component's requirement is the contract quotient, the weakest sound one, and again a SysML v2 requirement. Its required constraints carry the neighbours' assumptions, which a requirement for the mission alone drops and unit tests with mocked neighbours cannot reach. Signal Temporal Logic is closed under the quotient. We build the requirements, with derivation, allocation, satisfaction and verification, as a SysML~v2 model and compute the quotient from it. A case study delegates the local controller of a simulated warehouse robot, whose route crosses a worker's path and ends at a dock, to one language model under the quotient requirement, a mission-only requirement and a natural-language task, and scores the deliveries on live episodes against the system requirement from ground truth.

1 | INTRODUCTION

Hand-written component requirements can omit the assumptions fixed neighbors place on a delegated controller, allowing a locally compliant design to break the system. The paper derives a component requirement from the architecture’s contracts and evaluates that approach in a warehouse-robot case study.

1 | INTRODUCTION

  • A controller can meet its local requirement yet break a neighbor’s assumption, causing system failure that ideal stand-ins in unit tests do not exercise.Perception assumes slow enough turning for camera and lidar alignment, while actuation assumes commands stay below saturation.Source: §1 · pp. 2–3
  • Generative agents design against the prompt they receive, which carries no knowledge of the particular architecture’s contracts.The paper argues that agents can deliver candidates faster than an integration team can investigate them.Source: §1 · p. 3
  • The contract quotient gives the missing component the most permissive sound requirement, preserving fixed components’ assumptions that a mission-only requirement omits.The quotient is itself a SysML v2 requirement, and Signal Temporal Logic is closed under it.Source: §1 · p. 3
  • C-BASE computes the quotient from a SysML v2 architecture model and sends the derived requirement through a language-model, harness, and live-evidence workflow.The warehouse-robot case delegates the local controller while perception, localization, and drive remain fixed; deliveries are evaluated against the system requirement using ground truth.Source: §1 · pp. 2–3
  • The case study compares controller delegations under the quotient-derived requirement, a mission-only requirement, and a natural-language task, with fixed-component contracts checked first.The live evaluator attributes each first violation to its conjunct and owner.Source: §1 · p. 4

2 | RELATED WORK

The paper places its SysML v2 workflow alongside MBSE, contract-based design, and agentic robotics work. Its distinction is to derive a delegated component’s requirement from the system and fixed-component contracts rather than hand-writing it or relying on agent checks alone.

2 | RELATED WORK

  • Recasting IDDMBSE in SysML v2 makes requirements first-class model elements linked to architecture and evidence by derivation, allocation, satisfaction, and verification.The paper computes one component’s requirement from the others’ and keeps it in the model.Source: §2 · pp. 4–5
  • Contract-based design frames component assumptions and guarantees, and the quotient solves the missing-component problem; prior work gives closed forms for saturated and polyhedral contracts.The cited lineage includes interface automata, AGREE, and contract meta-theory.Source: §2 · p. 5
  • Existing agentic robotics checks include schemas, postconditions, simulator predicates, and model judges, but do not derive requirements from system contracts or check preservation of neighbor assumptions.The compared toolkits also lack an architecture model that holds the components together.Source: §2 · p. 5

3 | REQUIREMENTS AS CONTRACTS

The paper treats requirements as assume/guarantee contracts and derives the missing component’s most permissive sound requirement by quotient. It carries that construction into SysML v2 and Signal Temporal Logic, then specifies how sampled live traces are scored and attributed.

3.1 | Assume/Guarantee Contracts

  • The quotient is the largest contract whose composition with the fixed components refines the system contract, making it the most permissive sound missing-component requirement.Contracts compose by intersecting component behaviors, and refinement compares their accepted assumptions and guaranteed behaviors.Source: §3.1 · p. 5

3.2 | SysML v2 Requirements

  • A SysML v2 requirement denotes an implication from assumed to required constraints, and because saturated contracts are denoted by requirements, their quotient is again a requirement.The model links requirements to architecture and evidence; drawn episodes cannot establish a claim quantified over every behavior a component can produce.Source: §3.2 · p. 6

3.3 | Signal Temporal Logic as the Assertion Language

  • Signal Temporal Logic contracts are closed under composition and quotient, so repeated requirement derivation remains expressible in STL.STL robustness gives a signed margin, with positive values indicating satisfaction and negative values violation.Source: §3.3 · p. 6

3.4 | Sampled Fragment and Scoring Semantics

  • Sampled-trace scoring attributes a guarantee failure to its component only when that component’s assumption held through the deciding tick.For delegated requirements, prefix and whole-trace readings differ on excused traces; the unit-test harness requires assumptions at every tick, so the readings agree there. The evaluator’s whole-trace verdicts match the architecture model, while prefix reading differed on 44 of 600 and 40 traces under a second seed.Source: §3.4 · pp. 7–8

4 | DELEGATION AS THE QUOTIENT

The missing-component problem is to derive a sound requirement for an open component from the system contract and fixed neighbours’ contracts. The quotient is the most permissive sound requirement; the section develops its preservation obligations, a controller-observable dispatched form, and limits on what behavioral checks and episode evidence establish.

4.1 | The Missing Component Problem and Its Canonical Solution

  • The quotient Cq = Csys/Csib is sound, and every sound requirement for the missing component refines it.Thus it is the canonical, most permissive sound requirement for the open component.Source: §4.1 · pp. 8–9

4.2 | Preservation Obligations

  • Preservation obligations are the fixed components’ assumptions on the missing component, which a mission-only requirement omits.In the example, they are three yaw-rate bounds; each constrains controller outputs and can be checked without neighbors in the loop.Source: §4.2 · p. 9
  • A mission-only requirement can admit an implementation that breaks the system when a legal behavior violates the mission outside the ideal fixed-component guarantees.The stated theorem gives conditions for such a behavior and a composition that violates the system guarantee.Source: §4.2 · p. 10
  • Unit-test harnesses observing only ideal-neighbor behaviors cannot distinguish certain unsound implementations from quotient implementations.They give the same verdict to implementations agreeing on the ideal set; checking the preservation obligations can expose violations on harness traces.Source: §4.2 · pp. 10–11

4.3 | From Quotient to a Dispatched Requirement

  • The dispatched requirement strengthens the quotient into a sound requirement written over the delegated component’s observables.Its guarantee core uses fixed-component bounds; the clearance constraint accounts for report age, perception error, robot motion, and the margin.Source: §4.3 · p. 11

4.4 | Realizability, Evidence, and Risk

  • Consistency does not establish realizability: contracts describe behavior sets without a causality condition.The reference controller meets the dispatched requirement in the harness and all 30 live episodes; its yaw-rate bound is 0.8 rad/s at every tick.Source: §4.4 · p. 12
  • With confidence 1 − β, N independent episodes satisfying a requirement bound the probability of a violating episode by 1 − β^(1/N).Drawn episodes do not establish that every behavior of an implementation satisfies the contract; the bound concerns the operating distribution.Source: §4.4 · p. 12
  • The live evaluator assigns failures to owners by clause and tick, including rules for simultaneous fixed-component failures and missed docks.A fixed-component failure is attributed to the delegated component instead when it broke that component’s assumption by the failure tick.Source: §4.4 · p. 12

5 | C-BASE: THE ARCHITECTURE AND THE DESIGN PIPELINE

C-BASE connects contract computation, agent delivery, harness testing, and live evaluation in a deterministic pipeline around a SysML v2 architecture model. The model records requirements and evidence relationships, while validation checks model constraints and recorded results.

5 | C-BASE: THE ARCHITECTURE AND THE DESIGN PIPELINE

  • C-BASE computes and renders a quotient-based requirement, asks a language model for a delivery, gates it in a mocked-neighbor harness, then runs admitted code live and scores failures.The architecture model, contract kernel, work order, harness, evaluator, and orchestrator connect the pipeline; the kernel and model carry matching contracts.Source: §5 · pp. 12–13
  • The dispatched requirement is the quotient strengthened to controller observables, with each conjunct rendered as Signal Temporal Logic text and an explanation.The work order can instead use the mission-only requirement or a natural-language task; delivery forms include a whole controller, a governor, or a selected governor and parameters.Source: §5 · pp. 12–13

5.1 | The Requirements in the Architecture Model

  • The architecture model links the system requirement to fixed-component contracts and the dispatched controller requirement through derivation, allocation, satisfaction, and verification.The dispatched requirement assumes the environment and fixed-component contract implications, and requires the margin until docked, speed rule, and three preservation conjuncts.Source: §5.1 · p. 13, Figure 3 · p. 14

5.2 | Satisfaction, Verification and Evidence

  • Each recorded episode is a part’s trace, and verification cases check requirement usages on those traces; result items count an arm’s verdicts and name its scoring reading.The model also includes cases for individual fixed-component contract conjuncts.Source: §5.2 · p. 14
  • Syside validation reported zero errors and warnings, and checks caught seeded model defects; compiled constraints matched formula-text values on hand-built traces and evaluator verdicts on random traces.The script’s result-item values matched their sources.Source: §5.2 · p. 14

6 | CASE STUDY: A DELEGATED ROBOT CONTROLLER

The case study delegates a warehouse robot’s local controller to a language model under a quotient-derived requirement, a mission-only requirement, and a natural-language task. It tests the resulting deliveries in a harness and live episodes, including cases where fixed neighbors operate at their contract bounds.

6.1 | System, Mission and Contracts

  • The robot follows a 12 m route to a dock within 90 s while a worker crosses its path; the local-controller slot runs at 20 Hz with perception, localization, and drive fixed.The operating distribution varies worker speed from 0.5 to 0.85 m/s and crossing angle, and the slot receives observations as old as the perception contract allows.Source: §6.1 · p. 15

6.2 | Delegation Artifacts and Harness

  • The dispatched requirement preserves the quotient’s assumptions and specifies slot-input guarantees, including speed, worker-clearance margin, docking, and the fixed components’ yaw-rate bounds.The kernel checked both the dispatched requirement’s refinement of the quotient and its composition with fixed-component contracts against the system requirement; both inclusions held.Source: §6.2 · p. 17
  • The harness evaluates 482 scenarios with contract-bound mocked neighbors for quotient and natural-language conditions, but exact neighbors for the mission-only condition.Scenarios cover crossing walkers, reported person points shifted closer than reality, and two no-person cases.Source: §6.2 · p. 17

6.3 | Contract Calibration and Experimental Protocol

  • Contract calibration changed four bounds and repaired the perception camera projection before any delivery was judged.The localization heading bound holds only at rest because its estimate can lag the body by up to 0.229 rad during a turn in place.Source: §6.3 · pp. 17–18

6.4 | Admission Under Each Requirement

  • Among 384 governors, the dispatched requirement admitted 12, all safe at contract bounds; the mission-only requirement admitted 112, of which 88 broke the system requirement.The agent’s mission-only harness could not distinguish its 24 safe admissions from the 88 unsafe ones because it used ideal neighbors.Source: §6.4 · p. 18

6.5 | Live Results

  • At contract bounds, the unsafe mission-only delivery came within 0.14 m of the worker against the required 0.40 m, while the derived-requirement delivery stayed more than 1.4 m away; the unsafe delivery breached clearance in 6 of 22 searched-setting episodes.On 30 standard episodes, all deliveries kept the worker safe, but the first mission-only selection missed the dispatched requirement once and the resampled and natural-language selections missed it nine times each.Source: §6.5 · pp. 18–19

6.6 | Preservation Obligations, Contract Variants and the Perception Slot

  • A mission-only controller that spins at 1.2 rad/s was admitted in every scenario but refused by the dispatched requirement; live, localization engaged its declared lock in 9 of 9 episodes.The controller reported a successful dock while the robot stood 0.26 m away; the reference was also revised from 1.9 to at most 0.8 rad/s after its initial version was refused.Source: §6.6 · p. 19
  • The quotient tracks safe governors as neighbor contracts change, while the mission-only requirement admits the same 120 governors across variants, including 96 unsafe ones.Variants relaxed or tightened perception freshness or coarsened localization rest error one at a time; the dispatched requirement admits a subset of safe governors that shrinks to none when perception slows.Source: §6.6 · pp. 19–20, Table 4 · p. 20

7 | CONCLUSION

The paper presents the contract quotient as a SysML v2 requirement for delegating a component while preserving system correctness. In a simulated warehouse-robot case study, the quotient-based selection and reference kept the system requirement on every live episode, unlike the mission-only witness.

7 | CONCLUSION

  • The contract quotient is the most permissive sound requirement for a component when the rest of the architecture is fixed.It is obtained by quotienting the system requirement by the fixed components’ contracts.Source: §7 · p. 21
  • The language model’s quotient-based selection and a reference controller each kept the system requirement on every live episode.The model rewrote its perception grounding after a dropped cloud became a harness scenario, and the harness admitted it again.Source: §7 · p. 21
  • The mission-only witness fell below required clearance on every live episode, while a fast-turning controller missed the dock by more than 0.25 m on all nine episodes.The latter controller broke localization’s assumption while turning fast before docking.Source: §7 · p. 21

Significance and Practitioner Points

For component delegation with the architecture fixed, the paper derives a SysML v2 requirement from the system and neighboring components’ requirements. It presents this as a practical way to state neighbors’ assumptions explicitly and reports a controlled comparison of delegation approaches in a simulated robot-navigation stack.

Significance and Practitioner Points

  • A component’s delegation requirement can be derived from the system requirement and other components’ requirements by one algebraic operation.The result is an ordinary SysML v2 requirement with derivation, allocation, satisfaction, and verification links in the model.Source: Significance and Practitioner Points · p. 21
  • The derived requirement makes explicit what other components assume of the delegated component.The passage contrasts these explicit constraints with task descriptions and says integration testing discovers the omissions late.Source: Significance and Practitioner Points · p. 21
  • The paper reports a controlled comparison of quotient-derived, mission-only, and natural-language delegation to a language model on a simulated robot-navigation stack.Source: Significance and Practitioner Points · p. 21
Loading 2610.33349v1…