Source-linked AI summary
A SysML v2 Domain Library for ROS2 Robot Architectures
Sai Sandeep Damera, John S. Baras
TL;DR
SysML v2 provides no reusable definitions for key ROS2 architecture concepts, so projects reconstruct that vocabulary. This paper presents ros2-sysmlv2 and a model-to-package round trip with a generated conformance monitor. In a ground-robot case study, the monitor reported each of three introduced implementation departures.
Problem
SysML v2 has no ready definitions for ROS2 nodes, endpoints, messages, lifecycle states, QoS policies, and coordinate frames, so each modeling effort builds its own vocabulary.
Source: §1 · p. 2Method
The authors provide a native SysML v2 ROS2 library whose definitions robot models specialize, then generate a package and conformance monitor from the model’s type-directed ROS2 projection.
Source: §1 · p. 2Results
The generated monitor reported each of the three departures introduced in the ground-robot implementation.
Source: §1 · p. 3Takeaways & Limitations
The library provides a reusable, importable SysML v2 vocabulary, and its generated monitor reports where a running ROS2 graph departs from the model.
Source: §7 · p. 16
Abstract
from arXiv · showhide
Systems engineers who model a ROS2 robot in SysML v2 must first model ROS2 itself. Its nodes, communication endpoints, message types, lifecycle states, quality-of-service policies, and coordinate frames have no ready definitions in the language, so each project reconstructs them. We present ros2-sysmlv2, a native SysML v2 domain library that supplies these definitions for reuse. A robot model imports the library and specializes its definitions to declare its own nodes, ports, connections, frames, and parameters. The library maps ROS2 concepts to SysML v2 definitions and usages and organizes them in Primitives, Infrastructure, and Application layers. We check its declarations for parity with the ROS2 Jazzy sources they model. Because every ROS2 element of a model specializes a library definition, a tool can select those elements by type. We state what this selection is and use it for a round trip. A ROS2 package is generated from the selection, and a monitor generated with the package compares the running graph with the same selection and reports every departure against the model. The generation-gap workflow derives topic endpoints and parameter declarations while preserving developer-owned node algorithms. In a case study on a generated ground robot, the generated conformance monitor reported each of the three departures that we introduced in the implementation. The library is distributed as a versioned package that any SysML v2 model can import.
1 | INTRODUCTION
The paper introduces ros2-sysmlv2, a reusable native SysML v2 vocabulary for ROS2 architectures, and a type-directed round trip from robot models to generated packages and conformance monitors. It presents the library’s mapping, organization, source-parity checks, and use in a ground-robot case study.
1 | INTRODUCTION
- ros2-sysmlv2 supplies reusable definitions for ROS2 concepts that SysML v2 models otherwise must reconstruct, and robot models specialize those definitions for their own architectures.The library is organized in Primitives, Infrastructure, and Application layers, and its declarations are checked against the ROS2 Jazzy sources they model.Source: §1 · p. 2
- The generated monitor reported all three departures introduced in the ground-robot implementation.The round trip generates a ROS2 package and monitor from the model’s ROS2 projection while leaving node algorithms in developer-owned files.Source: §1 · p. 3
2 | RELATED WORK
- Unlike prior ROS and robotics modeling approaches, ros2-sysmlv2 uses native SysML v2 definitions and usages, models ROS2 concepts field by field, and is distributed as an importable versioned package.The related-work discussion contrasts it with profiles, custom metamodels, other architecture languages, and ROS 1 code-generation tools.Source: §2 · p. 4
3.1 | A Native Mapping for ROS2 Architecture
- The library maps ROS2 message types to item defs, nodes to part defs, endpoints to port defs, bindings to interface defs, transforms to connection defs, and QoS policies and parameters to attribute defs.Definitions provide reusable types; usages specialize them with architecture-specific values and names.Source: §3.1 · p. 5
3.2 | Semantic Discipline for Definitions and Usages
- The library’s ownership, direction, and composition choices follow SysML v2 semantic rules, and its sources and robot models pass the Syside validator with warnings treated as errors.Referential features are used where port and connection rules require features to reference independently existing elements.Source: §3.2 · pp. 5–6
3.3 | Layers and Packages
- Its seventeen packages are divided into Primitives, Infrastructure, and Application layers, with imports directed within a layer or toward lower layers and no cycles.The packageable library is distributed through a versioned archive; a downstream library can import it and specialize its definitions.Source: §3.3 · p. 6, §3.7 · p. 9
3.4 | Messages and Communication Endpoints
- The library models ROS2 messages, directed publisher and subscriber ports, and topic, service, and action bindings; extraction checks endpoint types and names, while generated tools check QoS compatibility.A topic with multiple subscribers is represented by a separate connection for each publisher-subscriber pair.Source: §3.4 · pp. 7–8
3.5 | Lifecycle, Parameters, and Frames
- Managed nodes use the modeled ROS2 lifecycle; parameters carry types and admissible ranges, and TF2 frames and transforms make frame trees explicit.Eight application archetypes capture recurring node roles, and eight of Nav2’s fourteen node definitions specialize an archetype; checks found parity with the Jazzy sources for every declaration examined.Source: §3.5 · p. 8, §3.6 · p. 8, §3.8 · p. 10
4 | THE SOFTWARE PROJECTION AND THE GENERATED PACKAGE
The type-based projection selects ROS2 usages by specialization, preserving the ownership and connection structure needed for extraction. The bridge turns that selection into a package and monitor while leaving developer-owned node files intact.
4.1 | Selection by Type
- The projection is the largest set of usages typed by a ROS2 root definition, and forms a usage graph with owned ports and parameters and connections ending at selected ports or frames.It is determined by the model, not read order; the proposition assumes a validated model and the stated ownership condition.Source: §4.1 · p. 11
4.2 | The Generated Package
- The bridge extracts selected node names, topics, QoS, and parameter values, then generates a Python or C++ ROS2 package after validating all records.It stops for missing message types, parameters without a known type or default, or invalid ROS2 names; one resolver keeps graph names consistent across generated artifacts.Source: §4.2 · p. 11
- The generator emits lifecycle base classes that declare parameters, create publishers and subscribers on configure, and destroy them on cleanup, shutdown, or error.Generated scripts bring each lifecycle-managed node to the active state.Source: §4.2 · p. 11
- Model interface changes reach regenerated base files while developer-owned node files and algorithms remain in place.Base files are rewritten each run, whereas derived files are not.Source: §4.2 · p. 11
5 | CONFORMANCE OF THE RUNNING GRAPH
The monitor compares keyed records from the extracted model with records observed in the running ROS2 graph. Conformance requires matching keys and every model-pinned coordinate, with persistent departures detectable under stated sampling bounds.
- The extractor keys nodes by fully qualified name, frames by identifier, parameters by owner and name, endpoints by owner, kind and resolved name, and connections by end keys.Model-pinned values become coordinates at those keys; values left open are omitted.Source: §5 · pp. 13–14
- Conformance holds exactly when observed and modeled key sets match for each kind and every pinned coordinate agrees at its key.A departure is a missing modeled key, an extra observed key, or a differing pinned value; the report identifies the key and coordinate.Source: §5 · p. 14
- A departure persisting through the first sample taken at least δ after its start is reported within δ + h + η, under the proposition’s sampling and observation assumptions.The bound assumes sample gaps of at most h, exact records after the graph is constant for δ, and publication within η of a sample.Source: §5 · p. 14
- The generated monitor checks node presence in both directions, endpoint message types, connection ends, and reliability and durability where a preset pins them.It checks presence for services, actions, parameters, and transforms; unspecified values are not counted as agreements.Source: §5 · pp. 13–14
6 | CASE STUDY: CONFORMANCE MONITORING OF A GENERATED ROBOT
The case study applies the library and generated monitor to two ground-robot models, including an ab initio robot and a hybrid model using Nav2. In the generated robot run, the monitor reported each introduced implementation departure.
6 | CASE STUDY: CONFORMANCE MONITORING OF A GENERATED ROBOT
- The ab initio robot model generated a graph with eleven nodes and eleven topic connections, while a hybrid model combined custom subsystems with the library’s Nav2 stack.The projection leaves the robot’s wider structure, behavior, requirements, and onboard-computer allocations in place.Source: §6 · p. 14, Figure 5 · p. 15
- Across 12 monitor cycles, all 11 modeled nodes and connections were present, and message types agreed at all 22 connection ends.Reliability and durability agreed on the 8 topics with pinned values; 2 middleware-deferred presets were not compared, while the map service, three actions, and transform topics were reported absent.Source: §6 · p. 14
- The monitor reported each introduced developer-file change from its first cycle, naming the node and topic and, for policy changes, the reliability and durability coordinates.The model and monitor remained unchanged while only the lidar driver's developer-owned file was modified.Source: §6 · pp. 14–15
7 | CONCLUSION
- The conclusion presents the library’s type-based selection as the basis for generating a ROS2 package and monitor, with checked declarations agreeing with ROS2 Jazzy sources.The conclusion reports two ground-robot models and runtime detection of every introduced departure.Source: §7 · pp. 15–16
Significance and Practitioner Points
- The article says practitioners can install the library as a package and specialize its definitions, while additional ROS2 packages can be added through downstream libraries.The library’s declarations were compared with ROS2 Jazzy sources, and four differing definitions were corrected.Source: Significance and Practitioner Points · p. 16
Data Availability Statement
- The library is openly available under the Apache 2.0 license, with sources in a public repository and releases published as Sysand packages.The supplementary material includes the case-study record and details of the projection, bridge pipeline, and monitor.Source: Data Availability Statement · p. 16, Supporting Information · pp. 16–17
Supplementary Material for A SysML v2 Domain Library for ROS 2 Robot Architectures
The supplementary material details the library’s ROS2 vocabulary, declaration patterns, and mapping checks, as well as the projection, extraction, generation, monitoring, and case-study records.
Supplementary Material for A SysML v2 Domain Library for ROS 2 Robot Architectures
- The material documents ROS2 concepts and library declarations, the path from archetypes to robot models, package mechanics, and the parity check against ROS2 Jazzy.Its seven sections follow the article’s order, with additional definitions, proofs, implementation detail, and case-study records.Source: Supplementary Material for A SysML v2… · p. 19, S1 | THE LIBRARY IN DETAIL · p. 19
- The supplementary material specifies projection laws and the reference extractor, then details bridge stages, monitor keys and counting rules, structural-conformance proofs, and sampling bounds.It also records the case study, including monitor output for the baseline and three departures in Python and C++.Source: Supplementary Material for A SysML v2… · p. 19
S1.1 | ROS2 Concepts
- The ROS2 concept overview describes nodes, topics, services, actions, QoS policies, parameters, managed-node lifecycle, coordinate frames, client libraries, and Nav2.It describes ROS2’s running graph as nodes together with their communication.Source: S1.1 | ROS2 Concepts · pp. 19–20
S1.2 | Endpoints, Topic Connections, and QoS Profiles as Declared
- Publisher and subscriber ports carry topic name, QoS profile, and message item features in opposite directions, while a topic connection relates the ports through its ends.The Controller archetype obtains its lifecycle state machine by specializing LifecycleNode.Source: S1.2 | Endpoints, Topic Connections,… · p. 20
S1.3 | The Lifecycle State Machine as Declared
- The lifecycle definition contains four primary states, six transition states, and 25 transitions registered by rcl_lifecycle.Seven are requested transitions; the other eighteen leave transition states based on callback success, failure, or error.Source: S1.3 | The Lifecycle State Machine as… · p. 20
S1.4 | From Archetype to Robot Model
- ControllerServer specializes the Controller archetype by fixing control frequency, default endpoint names, and message types, and is used in a hybrid robot model.Feature paths through the robot’s part hierarchy connect nodes, and the projection selects the server within the Nav2 stack.Source: S1.4 | From Archetype to Robot Model · pp. 20–21
S1.5 | Packaging, Release, and Downstream Use
ros2-sysmlv2 is imported as a versioned package and specialized by robot models; its declarations are checked against ROS2 Jazzy sources. A downstream library can extend it, and the checked declarations provide the basis for modeling ROS2 elements.
S1.5 | Packaging, Release, and Downstream Use
- A versioned KerML archive packages the library sources and manifests; automated releases check the tag, declared version, and expected file list before publication.Semantic versioning and a changelog identify changes that require existing models to be updated.Source: S1.5 | Packaging, Release, and… · pp. 21–22
- A robot model imports the library by package reference, specializes archetypes, and composes its nodes, connections, Nav2 stack, and frame tree.The described ground-robot model passes validation with the library sources.Source: S1.5 | Packaging, Release, and… · p. 22
- A downstream package installs the published release as a dependency, and its specialized definitions are included in the projection just like the library’s own usages.The validator reports the imports as unresolved when the installed copy is absent.Source: S1.5 | Packaging, Release, and… · p. 22
S1.6 | The Parity Check
- The parity check covers 88 of 120 message types and 311 fields, plus QoS, lifecycle, parameter, frame, and Nav2 declarations.The Nav2 check covers 49 fields across fourteen modeled action and message definitions.Source: S1.6 | The Parity Check · pp. 23–24
- The library is in parity with the ROS2 Jazzy sources on every declaration checked, after the Nav2 field check found and corrected four differing definitions.The checks cover modeled messages, QoS, lifecycle behavior, parameters, frame names, and Nav2 definitions and endpoints.Source: S1.6 | The Parity Check · p. 24
S2 | THE PROJECTION AND ITS LAWS
The projection selects evaluated model usages by whether their types specialize definitions rooted in the library, producing a usage graph when ownership and connection-end closure conditions hold. Its laws characterize the selection’s behavior within one evaluated model and across multiple libraries.
S2 | THE PROJECTION AND ITS LAWS
- The projection selects usages whose types specialize one of the library’s root definitions, rather than usages whose names merely match library definitions.A usage may carry multiple types; selected ports and parameters must have selected owners, and selected connections must have selected ends.Source: S2 | THE PROJECTION AND ITS LAWS · pp. 24–25
- The projection is idempotent, preserves inclusion, distributes over unions and intersections, and is determined by the evaluated model’s usages.It yields an incidence-closed usage graph when applied to an incidence-closed subset.Source: S2 | THE PROJECTION AND ITS LAWS · pp. 25–26
- For a validated model satisfying the owner condition, the projection is the largest subset whose usages have a type under a library root and forms a usage graph.The selection rejects dangling selected usages rather than silently pruning them.Source: S2 | THE PROJECTION AND ITS LAWS · pp. 25–26
- The projection laws compare subsets of one evaluated model; they do not establish how separately evaluated fragments or side-by-side models retain or change cross-boundary references.Re-evaluating changed source is outside these laws.Source: S2 | THE PROJECTION AND ITS LAWS · p. 26
- Selections rooted in two libraries combine by union, and adding a specialization of an existing root leaves that root’s projection unchanged.Intersecting two projections is not generally equivalent to projecting by intersected type sets when usages can have multiple incomparable types.Source: S2 | THE PROJECTION AND ITS LAWS · p. 26
S3 | THE REFERENCE EXTRACTOR AND THE BRIDGE EXTRACTOR
A two-pass reference extractor computes the projection from a model’s containment tree after flattening it into usages with resolved paths. The bridge extractor implements this specification for models that satisfy the owner condition, with stated input constraints and a narrower handling of non-node owners.
S3 | THE REFERENCE EXTRACTOR AND THE BRIDGE EXTRACTOR
- Flattening assigns full feature paths to usages and resolves ownership and connection ends; the reference extractor indexes those usages, then emits those satisfying the selection predicate.The extractor stops if a selected port or parameter has an unselected owner or a selected connection has an unselected end.Source: S3 | THE REFERENCE EXTRACTOR AND THE… · p. 27
- Under unique paths, uniquely resolved ends, lowered boundary delegations, and incidence closure, the two-pass extractor preserves the projection’s usages, maps, types, and values.If incidence closure fails, extraction stops.Source: S3 | THE REFERENCE EXTRACTOR AND THE… · p. 27
- Normalization transfers agreement between specified computations, but does not establish that an implementation uses the specified name-resolution or value functions.The comparison rejects canonical endpoint-key collisions, which can occur despite distinct feature paths.Source: S3 | THE REFERENCE EXTRACTOR AND THE… · p. 28
- The bridge extractor selects user subtypes, reads inherited members once, and resolves connection ends; unlike the reference extractor, it omits library-typed ports on non-node owners rather than stopping.For models satisfying the owner condition, the two extractors agree; the bridge’s 55 regression checks pass on two fixture models.Source: S3 | THE REFERENCE EXTRACTOR AND THE… · p. 28
S4 | THE BRIDGE PIPELINE IN DETAIL
The bridge pipeline extracts selected model elements, validates and generates a ROS2 package, then supplies shared name and configuration handling, lifecycle code, and an activation script. Developer algorithms remain in derived files across regeneration.
S4.1 | Extraction
- The extractor reads inherited effective members once, resolves connection ends by feature paths, and classifies usages by specialization at any depth.Values bound at a usage take precedence over values on its definition.Source: S4.1 | Extraction · pp. 28–29
- The extractor writes architecture.json with node, endpoint, parameter, connection, frame, transform, and requirement records, and stops on unresolved or inconsistent selected elements.It warns but continues for topic-name mismatches after namespace resolution and unevaluable bound values.Source: S4.1 | Extraction · p. 29
S4.2 | Generation
- The generator validates every record before writing and emits a Python or C++ package; regenerated base files coexist with developer-owned derived files that persist.A command-line option can discard derived files when developers want them regenerated.Source: S4.2 | Generation · p. 29
S4.3 | Names, Parameter Values, and QoS Profiles
- One name resolver applies ROS2 naming rules across extraction, launch, parameter files, and monitoring, while modeled parameter types and QoS policies map into generated code and checks.Topic connections are checked for reliability and durability compatibility; middleware-determined policies remain undetermined until observed by the monitor.Source: S4.3 | Names, Parameter Values, and… · pp. 29–30
S4.4 | The Lifecycle Base Class and the Activation Script
- Generated lifecycle base classes declare parameters and manage endpoints through lifecycle callbacks, while derived classes hold developer algorithms; an activation script requests transitions until each node is active or reports failure.The script exits successfully only when every node is active.Source: S4.4 | The Lifecycle Base Class and… · p. 30
S4.5 | The Launch File and the Wired Mode
The generated launch and wired mode make the modeled ROS2 topology runnable, while a generated monitor compares graph observations against keyed model expectations. The monitor reports departures through diagnostic groups and periodic summaries.
S4.5 | The Launch File and the Wired Mode
- The launch starts generated nodes with their parameters, activates them through a lifecycle manager, and starts the monitor, which reports from its first cycle five seconds later.For hybrid models containing Nav2 servers, Nav2 bringup and its own lifecycle manager run alongside the generated launch file.Source: S4.5 | The Launch File and the Wired… · p. 30, S5 | THE GENERATED MONITOR: KEYS,… · p. 31
- In wired mode, generated nodes publish default-constructed messages on timers and log subscription receipts, making the modeled topology exercisable before algorithms exist.Publishing runs at 10 Hz for sensor-data endpoints and 1 Hz otherwise; timers stop when a node deactivates or enters the listed shutdown and recovery states.Source: S4.5 | The Launch File and the Wired… · p. 31
S5 | THE GENERATED MONITOR: KEYS, GROUPS, AND COUNTING RULES
- The monitor queries node, topic, endpoint, QoS, and service information every five seconds, then publishes grouped diagnostics and a summary to /conformance_report and its log.It subscribes to no system topic and sends no requests to system nodes.Source: S5 | THE GENERATED MONITOR: KEYS,… · p. 31
S5.1 | The Expectation Tables and Their Keys
- Expectations are keyed by modeled element: nodes by name and namespace, endpoints by owner, role, and resolved topic, and parameters by owner and name.Connections, QoS expectations, services, actions, and frames use their connection names, topics, resolved names, or identifiers as specified.Source: S5.1 | The Expectation Tables and… · p. 31
- The monitor organizes comparisons into diagnostic groups, with each departure naming the relevant key and, for a value mismatch, its expected and observed values.The expectation tables identify the keys and graph queries used by these groups.Source: S5.1 | The Expectation Tables and… · pp. 31–32
S5.2 | The Diagnostic Groups
The monitor reports structural departures by comparing keyed records and coordinates, and its summary counts distinguish agreement from values that cannot be compared. The paper also formalizes exact conformance as equality of keys and agreement on pinned coordinates.
S5.2 | The Diagnostic Groups
- Missing nodes, wrong message types, broken connections, and incompatible observed profiles at an edge are errors; several other departures, including extra nodes and preset differences, are warnings.A configured name pattern excludes matching nodes from the report.Source: S5.2 | The Diagnostic Groups · p. 32
S5.3 | Counting Rules and the Summary Line
- An expectation without a concrete value is not compared, while an absent endpoint remains compared and lowers the agreeing count.The monitor separately counts certain QoS expectations that are not compared because policies are negotiated, and treats non-concrete compatibility pairs as indeterminate.Source: S5.3 | Counting Rules and the Summary… · p. 33
- The logged summary gives the highest group severity and agreeing/compared counts for six groups, with not-compared counts where applicable.The diagnostic array carries the same counts together with the keys and values named by the groups.Source: S5.3 | Counting Rules and the Summary… · p. 33
S6.1 | Records and Their Comparison
- For complete, well-keyed record maps, conformance holds exactly when all three discrepancy sets—missing keys, extra keys, and coordinate mismatches—are empty.Equality of a key fixes its only possible correspondence, so each nonempty discrepancy provides a named witness.Source: S6.1 | Records and Their Comparison · p. 34
- Exact conformance requires equal modeled and observed key sets for each kind and agreement at every pinned coordinate; departures identify a missing key, an extra key, or a differing coordinate.The comparison rejects duplicate canonical keys during normalization rather than merging records that collide.Source: S6.1 | Records and Their Comparison · pp. 33–34
S6.2 | Restriction of a Global Comparison
A global comparison can be decomposed into scoped comparisons when the scopes cover all keys and preserve agreement at overlaps. The finite-fact contract represents required and permitted structural facts, with derived links kept distinct from declared bindings.
S6.2 | Restriction of a Global Comparison
- Scoped comparisons recover the global result when fixed scopes cover the full key catalog and inherit the same coordinate obligations at overlap keys.Relations must also be covered; separate publisher and subscriber scopes miss the relation between them unless a scope includes both ends.Source: S6.2 | Restriction of a Global… · pp. 34–35
S6.3 | Facts and the Contract
- The finite catalog encodes record presence and coordinate values as facts, while continuous values and unbounded names require a separate finite abstraction.The comparison fixes a model revision, deployment scope, normalization profile, and finite catalog of possible structural facts.Source: S6.3 | Facts and the Contract · p. 35
- Positive Horn rules derive candidate links only for compatible roles with equal resolved channels and interface types; they do not assert wiring, QoS compatibility, or message delivery.A modeled binding remains a separate primitive fact, and rules do not create node or endpoint declarations.Source: S6.3 | Facts and the Contract · p. 35
- A structural contract pairs required facts with permitted facts; both bounds matter because missing required endpoints and extra endpoints that create unintended links must be detectable.Exact equality is the special case where the required and permitted sets are the same.Source: S6.3 | Facts and the Contract · p. 36
- The record contract is extended with separate derived-fact obligations for relation comparison, while closure preserves the primitive facts supplied by the observation.An explicit primitive binding and a derived candidate link retain different meanings.Source: S6.3 | Facts and the Contract · p. 36
S6.4 | The Verdict of a Sampled Monitor
The sampled monitor reasons from lower and upper bounds on established and possible facts, so a verdict is sound only under the stated coverage and scope assumptions. When those bounds leave uncertainty, independently justified deployment constraints can narrow the possible completions.
S6.4 | The Verdict of a Sampled Monitor
- A runtime observer has a partial, time-dependent graph view, and a missing query response alone does not establish that an endpoint is absent.The finite profile must account for all in-scope names and supported values; scope also fixes versions, sample phase, boundary, and infrastructure exclusions.Source: S6.4 | The Verdict of a Sampled Monitor · pp. 36–37
- When the finite profile covers actual facts and the evidence bounds hold, PASS implies conformance and FAIL implies violation; UNKNOWN asserts neither.The bounds identify the affected normalized key when a required fact is absent or a forbidden fact is established.Source: S6.4 | The Verdict of a Sampled Monitor · p. 37
- A required fact outside the upper bound is a concrete missing-fact witness, while an established fact outside the permitted set is a concrete forbidden-fact witness.Either witness makes every deployment compatible with the sound bounds nonconformant.Source: S6.4 | The Verdict of a Sampled Monitor · p. 37
- For an UNKNOWN interval verdict, a nonempty family of independently justified deployment completions can resolve the result; without it, neither universal conformance nor violation is soundly assertable.Every definite verdict from the interval method agrees with the verdict relative to the completion evidence.Source: S6.4 | The Verdict of a Sampled Monitor · pp. 37–38
- Independent configuration evidence that exactly one of two alternatives is present can make all compatible completions derive a required fact and yield PASS.The configuration evidence is obtained rather than assumed from the model's desired availability.Source: S6.4 | The Verdict of a Sampled Monitor · p. 38
- Unexpected endpoints can be reported from positive evidence, but absence requires sound negative coverage; QoS compatibility and equality with a modeled QoS value are separate checks.The generated monitor reports those QoS predicates in separate groups.Source: S6.4 | The Verdict of a Sampled Monitor · p. 38
S6.5 | The Detection Bound
The detection result is conditional on bounded, complete observation of a stable violating deployment. The realization result connects the model, recovered package declarations, and runtime records through shared keys and pinned values.
S6.5 | The Detection Bound
- The detection bound does not follow from Equation (S13) alone: a persistent missing endpoint can remain unknown unless its upper bound is narrowed.The temporal result separately requires bounded observation on a stable scope and complete acquisition.Source: S6.5 | The Detection Bound · p. 38
- Under stable, complete acquisition, a violation that persists through the first sample at or after a + δ is reported as a failure, with reporting adding at most η.For the generated monitor, h is its five-second cycle plus one cycle’s query duration, while δ is middleware graph-discovery time to reflect a change in query results.Source: S6.5 | The Detection Bound · pp. 38–39
S6.6 | From the Model through the Generated Package to the Running Graph
- Conditional structural realization follows when model, recovered declarations, and runtime records are complete, well keyed, and agree on keys and model-pinned coordinates.The contract also transfers to the closure of actual primitive facts when the stated premises hold; sound observation bounds with a PASS verdict can discharge the actual-fact premise.Source: S6.6 | From the Model through the… · p. 39
- Recovery checks what generated files declare, while runtime observation checks what runs in scope, including declarations created outside those files.Generated extensions preserve the conclusion when their resulting inventories and pinned values remain equal to the model’s; the monitor reports departures at current keys.Source: S6.6 | From the Model through the… · p. 39
S7 | THE RECORD OF THE CASE STUDY
The case study projects a ground-robot model into records and a generated package, then checks the launched graph against those records. In the baseline run, the monitor verified the modeled nodes, endpoint types, connections, and comparable QoS expectations while reporting interfaces the package did not generate.
S7.1 | The Model’s Records and the Generated Package
- The model projects eleven nodes into eleven topic connections over nine topics, one service server, three action servers, two parameters, six frames, and five transforms.Ten of eleven publishers declare a QoS preset; the mission coordinator’s publisher declares none.Source: S7.1 | The Model’s Records and the… · p. 40
- The generated monitor carries expectations for 11 nodes, 22 endpoint types, 11 connections, 10 QoS settings, one service, three actions, two parameters, and six frames.The package includes node files, launch and lifecycle components, a monitor, parameter file, and activation script; service and action servers are not generated and are reported missing at warning level.Source: S7.1 | The Model’s Records and the… · p. 40
S7.2 | The Baseline Run
- The baseline monitor verified all 11 nodes, 22 endpoint types, 11 connections, and 11 RxO edges; it compared 8 QoS expectations and 18 divergence expectations.Two QoS expectations and four divergence expectations were not compared because the relevant presets fixed no concrete policy.Source: S7.2 | The Baseline Run · p. 40
- The baseline run also warned that the package lacked the modeled service, actions, and transform topics, while the launch left no package process after teardown.The monitor reported the absent interfaces that the package version does not generate.Source: S7.2 | The Baseline Run · p. 41
S7.3 | The Three Departures
Three controlled changes to the lidar driver produced distinct monitor departures, while the generated Python and C++ packages both ran against the same model-derived checks. The departure diagnostics distinguish missing or mistyped endpoints from QoS disagreement, including cases where edge compatibility remains intact.
S7.3 | The Three Departures
- The departures were isolated to one developer-owned file across a control run and three 45-second runs, with the generated base classes, launch file, and monitor unchanged.The other diagnostic groups and the service, action, and transform warnings remained as in the control.Source: S7.3 | The Three Departures · pp. 41–42
- The monitor reported each introduced lidar-driver departure: replacing /scan, changing LaserScan to std_msgs/String, and changing the sensor-data QoS profile.The topic change broke three connections; the type change was reported by the endpoint-type group, while the QoS change produced policy and divergence warnings despite compatible observed edges.Source: S7.3 | The Three Departures · p. 42
S7.4 | The Same Model in Python and in C++
- Both generated language packages activated all eleven nodes and produced the baseline monitor line before the monitor treated best-available QoS as negotiated and indeterminate.The /map QoS expectation was negotiated; its two connection ends were likewise reported as negotiated, leaving 10 of 11 RxO edges OK and one indeterminate.Source: S7.4 | The Same Model in Python and in… · pp. 42–43