{"id":"0f6a87b3-7da7-4acb-acc3-2ba16ab8917f","arxiv_id":"2411.14367","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"ROSMonitoring 2.0 adds service monitoring and publication-order reordering to runtime verification for ROS, demonstrated on a battery-supervisor case study.","lead":"This paper extends an existing runtime verification framework for ROS robots so that it can monitor service calls and can reorder messages by publication time. The main practical value is for developers of safety-critical robot systems who want runtime checks beyond simple topic messages.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 1's cross-topic ordering depends on globally comparable publication timestamps, but Algorithm 1 never states the clock domain of getTime(msg); with unsynchronized publisher clocks, min-timestamp selection does not recover true publication order.","rationale":"The reader's weakest_assumption identifies exactly the same load-bearing issue: timestamps must be globally comparable for Theorem 1 to deliver publication order, and Algorithm 1 does not state the clock domain of getTime(msg). My pass confirms this is the most serious gap in the central argument. It is a correctness risk, not merely an implementation detail: without synchronized clocks, the min-timestamp selection in Algorithm 1 can emit messages in an order that inverts true publication order, so the framework's headline feature fails in the distributed setting it claims to support. The paper gives a real proof and a clearly stated Assumption 1, and the case study is a reasonable demonstration on what is likely a single machine, so the contribution is plausible under an added assumption of clock synchronization or a redefinition of 'publication order' as 'order by a global timestamp source.' That is an addressable revision, not a fatal flaw, so the existing CONDITIONAL verdict stands unchanged. The concrete test would settle whether the hidden assumption actually breaks the claimed guarantee.","tokens_in":13546,"tokens_out":3341,"duration_ms":36440,"concrete_test":"Run Algorithm 1 with two publishers on separate hosts, deliberately setting host B's clock 2 seconds ahead of host A, and publish interleaved messages so that the true publication order is A1, B1, A2, B2 while the timestamp order (from local clocks) is B1, A1, B2, A2. Record the order in which messages reach the Oracle; if the Oracle receives B1 before A1, Theorem 1 fails. Additionally, instrument getTime(msg) to log whether it returns header.stamp, ROS time, or wall-clock time, to establish the actual clock domain used.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central correctness claim is Theorem 1 (Section 4.2): Algorithm 1 propagates messages to the Oracle in publication order. The proof is only valid if the timestamps compared in min_time_stamp are globally comparable as publication times. Algorithm 1 line 10 calls getTime(msg), and Section 4.2 does not specify whether this reads a publisher-inserted header stamp, a monitor-side receive timestamp, or ROS time. In a distributed ROS1 system, nodes do not have synchronized clocks by default. If getTime returns publisher-generated timestamps, a later-published message from a node with an advanced clock can carry a smaller timestamp than an earlier-published message from a node with a lagging clock, so the 'smallest timestamp first' rule (line 15, sendEarliestMessageToOracle) emits messages in timestamp order, not publication order, invalidating the conclusion of Theorem 1. Equal timestamps are also unhandled: messages is keyed by timestamp, so two messages from different topics with the same timestamp overwrite one another, causing a missed or misordered message. The case study may avoid this because all nodes plausibly share one machine, but the framework's stated contribution is for general ROS systems, and the abstract claims improved scalability and interoperability. The paper honestly flags deadlock risks and timeouts as future work, but the clock-comparability assumption is not flagged, and Theorem 1 is stated unconditionally.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents ROSMonitoring 2.0, an extension of the ROSMonitoring runtime verification framework that adds two features: monitoring of ROS services (in addition to topics) and reordering of messages across topics and services according to publication time before they are sent to the verification oracle. The reordering is implemented by Algorithm 1, which buffers messages per topic and releases the message with the smallest timestamp once every buffer is non-empty. The paper states Assumption 1 (messages on a single topic arrive in publication order) and proves Lemma 1 and Theorem 1 claiming that the algorithm propagates messages to the oracle in publication order. The authors also describe a case study on a battery-supervisor UAV system, with properties expressed in Past MTL, showing that ordered monitoring avoids the false negatives that unordered monitoring produces, at the cost of increased latency. The service monitoring feature is also ported to ROS2.","tokens_in":13812,"tokens_out":5000,"duration_ms":46099,"significance":"If the correctness claim of Algorithm 1 holds under clearly stated assumptions, the work addresses a genuine problem in runtime verification of distributed robotic systems: cross-topic message interleaving. The service monitoring extension is practically useful and the framework is open source, which supports reproducibility. The paper is clearly written and the case study, while small, illustrates the value of the ordering mechanism. However, the central correctness theorem currently relies on unstated global clock-comparability and liveness assumptions, and the algorithm has a concrete equal-timestamp bug. These issues must be resolved before the central claim is fully established. The empirical evaluation is also too thin to support the accuracy claim quantitatively, but that is secondary to the algorithm's correctness.","major_comments":[{"comment":"The proof of Theorem 1 tacitly assumes that the values returned by getTime(msg) are globally comparable as publication times across all topics. The paper does not specify whether these are publisher-inserted header stamps, ROS time, or monitor-side receive timestamps. In a distributed ROS1 system, nodes do not have synchronized clocks by default; if timestamps originate from different node clocks, the minimum-timestamp selection rule can emit messages in timestamp order rather than publication order, contradicting the conclusion of Theorem 1. Please state the clock-domain assumption explicitly and either restrict the theorem to systems with a global clock or justify that the chosen timestamp source preserves publication order.","section":"Section 4.2, Theorem 1 and Algorithm 1"},{"comment":"The global messages dictionary is keyed by timestamp alone. If two messages on different topics carry the same timestamp, the assignment messages[time_stamp_of_msg] = msg overwrites the earlier entry, so one message is lost while its timestamp remains in buffer[t]. The algorithm therefore mishandles equal timestamps, and the proof of Theorem 1 does not address this case. Use a composite key (e.g., timestamp plus topic) or define a tie-breaking rule, and update the proof accordingly.","section":"Section 4.2, Algorithm 1 (lines 10-12 and 3-5)"},{"comment":"The paper acknowledges that the ordering mechanism can deadlock and works around it in the case study by keeping /status_change unordered and by interrupting the execution to release remaining messages. This means the delivered trace can be incomplete if a buffer remains empty; the correctness claim of Theorem 1 implicitly assumes that all relevant messages are eventually buffered. The theorem should state the liveness condition under which it applies, and the case study should be described as best-effort ordering rather than guaranteed complete ordering.","section":"Section 4.2 (deadlock discussion) and Section 5 (page 47)"}],"minor_comments":[{"comment":"The caption contains a typo: 'ans /battery_status' should be 'and /battery_status'.","section":"Figure 5 caption"},{"comment":"The description for /battery_status lists '0' as a possible status value, but Section 5 uses statuses 1, 2, and 3 only; clarify this inconsistency.","section":"Table 2"},{"comment":"The textual description 'Every /SetLED service request is followed by a /SetLED service request within 100 time steps' appears to be a typo; the formalization in Table 1 suggests the intended property concerns responses, not requests.","section":"Section 5, Property 3b description"},{"comment":"The accuracy comparison is based on 10 runs with no raw data or statistical significance test; please report the number of false negatives per run or provide the trace data to substantiate the qualitative claim.","section":"Section 5, Experimental evaluation"},{"comment":"The statement that ROSRV 'does not support the verification of services or the customisation of the order of topics' should be supported by a specific reference or a direct citation to [19] to avoid unsupported claims.","section":"Section 6, Related work"}],"recommendation":"major_revision","confidential_remarks":"The paper is a reasonable workshop contribution that extends a known framework. The main technical concern (unstated clock-domain assumption and equal-timestamp handling in Algorithm 1) is fixable but requires changes to the theorem statement and algorithm. The empirical evaluation is very limited, but for a workshop paper the case study may be acceptable if the correctness issues are addressed. I would encourage the authors to also clarify the exact semantics of the 'ordered' trace in the presence of the acknowledged deadlock workaround."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Short version: this is a useful extension of a known tool, with a simple reordering algorithm and a correct proof under two assumptions the paper forgets to state. The service-monitoring part is the most solid; the ordered-topics part has a clock-comparability gap that needs patching before the main theorem is trustworthy.\n\nWhat's actually new: ROSMonitoring 2.0 intercepts ROS services end-to-end, checking both request and response, and adds a buffered merge that releases messages to the oracle in publication order. The service mechanism mirrors topic filtering but with the extra step of invoking the real service after a positive verdict, and the sequence diagram is clear. The reordering algorithm is a standard merge by timestamp, but applying it to multi-topic ROS runtime verification is new for this tool, and the proof of Theorem 1 is valid given sequential arrival per topic and globally comparable, unique publication timestamps. The paper ships code and runs a case study, which earns real credit.\n\nSoft spots. The proof states the per-topic arrival assumption but not the cross-topic clock assumption. getTime(msg) is never defined: if publisher clocks drift, the 'smallest timestamp first' rule does not recover publication order and Theorem 1 fails. The messages dictionary is keyed by timestamp, so equal timestamps silently overwrite each other. Both are fixable, but as written the theorem overclaims. The case study is thin: ten runs, no raw data, and the accuracy claim is qualitative. The abstract's security, scalability, and interoperability claims look inherited from ROS2 marketing rather than measured.\n\nVerdict: the core extension is real, the service part is solid, and the ordering part is sound under assumptions likely true in the single-machine demo but not guaranteed in general ROS deployments. The paper deserves a serious referee, but I would want the theorem restated with explicit assumptions and a stronger evaluation before accepting it as is.","headline":"Useful tool extension with a correct reordering proof that silently depends on unstated clock-comparability and unique-timestamp assumptions; service monitoring is the solid part, the evaluation is thin.","tokens_in":14312,"tokens_out":1652,"would_cite":true,"duration_ms":17177,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"ROSMonitoring 2.0 verifies services and ordered message traces for ROS","keywords":["runtime verification","ROS","ROSMonitoring","service monitoring","message ordering","temporal logic","robotic software verification","UAV case study"],"falsifier":"Run two publisher nodes with known clock offsets (for instance, one clock set 10 seconds ahead) and record the true send order with an independent logger; if the oracle receives the cross-topic trace in a different order under Algorithm 1, then publication-order delivery depends on synchronized clocks. On the case-study side, replay the same recorded message trace through the monitor once with ordering enabled and once disabled and count verdict mismatches: the paper's claim is that the mismatch rate goes to zero for the properties in Table 1 when ordering is on.","tokens_in":13391,"feed_emoji":"🤖","tokens_out":7539,"duration_ms":67150,"temperature":0.7,"pith_summary":"ROSMonitoring 2.0 claims to close two gaps in the original ROSMonitoring framework: it can monitor ROS services as well as topics, and it can deliver monitored messages to the verification oracle in the order they were published rather than the order they happened to arrive. The service extension inserts the monitor as a proxy between client and server, checking each request with the oracle before forwarding it and each response before returning it. The ordering extension buffers messages per topic and releases the one with the earliest publication timestamp once every topic buffer is non-empty, with a proof that this yields true publication order under the assumption that each topic delivers messages in publish order. A battery-supervisor case study on a fire-fighting UAV shows that unordered monitoring produces frequent false-negative verdicts on properties linking battery status to percentage readings and to LED-set service calls, while ordered monitoring produces accurate verdicts at the cost of added latency. The paper argues the extensions preserve the framework's separation between message interception and formalism-agnostic oracles, so existing specifications carry over unchanged.","feed_headline":"ROSMonitoring 2.0 verifies services and ordered message traces for ROS","feed_subtitle":"A UAV battery case study shows unordered traces spawn false negatives; ordering removes them.","key_machinery":"The load-bearing mechanism is Algorithm 1, a timestamp-buffered release rule. Each monitored topic t has a buffer; addToBuffer(msg,t) appends the message's publication timestamp to buffers[t] and stores the message in a global dictionary keyed by that timestamp, all under a lock. A sendEarliestMessageToOracle step runs as soon as no topic buffer is empty, picks the smallest timestamp across buffers, sends that message to the oracle, publishes the verdict, and removes the entry. The proof of Theorem 1 rests on Assumption 1 (per-topic arrival order equals publication order) plus the observation that a larger-timestamp message from another topic cannot be selected while a smaller-timestamp message waits in a different buffer. The same buffering discipline applies to service requests and responses, and the paper warns that ordering mutually dependent topics and services together can deadlock, illustrating the workaround in the case study by keeping /status_change unordered and carrying a status_change flag inside the ordered /battery_status messages.","core_discovery":"The central claim is a framework extension: ROSMonitoring 2.0 makes service calls first-class citizens of runtime monitoring for ROS and gives the oracle a publication-ordered view across multiple topics and services. For services the monitor acts as an intermediary: it receives the client's request, sends it to the oracle for a verdict, invokes the real service only on a positive verdict, then sends the response back to the oracle before delivering it to the client; a negative verdict on either side triggers an error message and blocks the call. For ordering, Algorithm 1 keeps one FIFO buffer per monitored topic, tags each message with its publication timestamp, and only releases a message to the oracle when every topic buffer holds at least one message, always choosing the smallest timestamp. Theorem 1 states that this release rule propagates the complete event trace in publication order, relying on Assumption 1 that messages on a single topic arrive in publish order. The case study demonstrates the practical payoff: without ordering, messages on /battery_status can reach the monitor before the /battery_percentage or /input_accepted messages they depend on, producing false negatives; with ordering, the verdicts match the intended properties, and the measured overhead is concentrated in the time service requests wait while earlier messages drain from other buffers.","pith_inferences":["If the timestamps read by getTime(msg) come from unsynchronized clocks on different publishers, then comparing them across topics does not recover true publication order; Theorem 1's conclusion would need an explicit clock-synchronization or logical-clock assumption.","The deadlock workaround in the case study suggests a general design rule: order only channels whose dependency graph is acyclic, since ordered channels that wait on each other's messages must not feed each other; this could be turned into a static analysis.","In sparse or lossy topics, waiting until every buffer is non-empty may stall the trace indefinitely; a timeout-based variant that trades occasional mis-ordering for liveness would be a natural test, and the paper itself lists timeouts as future work.","The same buffering scheme could extend to ROS 2 actions or other asynchronous request-response patterns, where ordering goals and response matching would follow the same proxy-and-buffer structure."],"forward_implications":["Temporal properties ranging over both topics and services become checkable at runtime, so requirements like 'every LED update follows a legitimate battery-status change' can be verified automatically.","Existing ROSMonitoring oracles and formal specifications remain usable because the extension changes only monitor synthesis, not the oracle interface or the formalism-agnostic design.","Enabling ordering removes the false-negative verdicts observed on cross-topic and topic-service properties, making ordered monitoring the appropriate choice for safety-critical robotic applications.","The publication-ordered trace and the original receive-ordered trace can be compared to localize which node reordered events, supporting fault attribution rather than only violation detection.","The service-proxy pattern and the buffered-release ordering are reusable outside ROSMonitoring, as the paper notes, for other publish-subscribe systems with per-channel ordering guarantees."],"supporting_citations":[{"why":"The original ROSMonitoring framework that ROSMonitoring 2.0 extends; supplies the monitor-oracle architecture, instrumentation approach, and the baseline topic-only monitoring behavior.","marker":"[15]"},{"why":"ROS itself, the middleware whose publish-subscribe topics and synchronous services define the communication model the framework monitors.","marker":"[2]"},{"why":"Metric Temporal Logic, the formalism used to express the temporally quantified properties (such as 'within 100 time steps') checked by the oracle in the case study.","marker":"[22]"}],"fun_headline_variants":["ROSMonitoring 2.0 adds service and ordered-topic runtime checks","Ordered messages kill false negatives in ROS runtime verification","Service calls and ordered topics now verifiable in ROSMonitoring 2.0","ROSMonitoring 2.0: verifying services and publication order","Unordered traces mislead ROS monitors; ordering fixes the verdicts"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that every topic delivers its messages to the monitor in the order they were published, and that the timestamps used to compare messages across topics are mutually comparable; if either fails, the earliest-timestamp release rule may present the oracle with events that did not actually happen in that order.","fun_headline_variants_meta":{"raw":{"variants":["ROSMonitoring 2.0 adds service and ordered-topic runtime checks","Ordered messages kill false negatives in ROS runtime verification","Service calls and ordered topics now verifiable in ROSMonitoring 2.0","ROSMonitoring 2.0: verifying services and publication order","Unordered traces mislead ROS monitors; ordering fixes the verdicts"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000292,"raw_usage":{"total_tokens":1681,"prompt_tokens":899,"completion_tokens":782,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":515,"completion_tokens_details":{"reasoning_tokens":692}},"tokens_in":515,"tokens_out":782,"duration_ms":6837,"temperature":1.0,"reasoning_tokens":692,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T15:14:39.401450+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run two publisher nodes with known clock offsets (for instance, one clock set 10 seconds ahead) and record the true send order with an independent logger; if the oracle receives the cross-topic trace in a different order under Algorithm 1, then publication-order delivery depends on synchronized clocks. On the case-study side, replay the same recorded message trace through the monitor once with ordering enabled and once disabled and count verdict mismatches: the paper's claim is that the mismatch rate goes to zero for the properties in Table 1 when ordering is on.","supporting_citations":[{"cited_title":"https://www.ros.org/","cited_arxiv_id":null,"evidence_quote":"ROS itself, the middleware whose publish-subscribe topics and synchronous services define the communication model the framework monitors."}],"review_version":1}