Asymmetric Timed Refinement for Correct Post-Deployment Updates in Real-Time Systems
ACM/IEEE International Symposium on Formal Methods and Models for System Design (MEMOCODE 2026), Barcelona, Spain
Best Paper Award
- Status
- Accepted — Presented at MEMOCODE 2026. A proceedings DOI is not yet listed here; the paper is openly available on Zenodo.
- Date
- (MEMOCODE 2026 conference date)
- Zenodo
- 10.5281/zenodo.22746507
- License
- CC BY 4.0
- Download PDF (Authors' version (CC BY 4.0))
- Zenodo record
Abstract
Model-based systems engineering is a well-established framework for developing post-deployment updates in cyber-physical systems. In real-time and safety-critical settings in particular, these updates must be shown to preserve previously verified properties. Refinement relations over timed models provide an attractive alternative to full model checking, as they establish correctness by behavioral inclusion and can be checked efficiently and compositionally. However, traditional relations enforce symmetric timing preservation for all observable events, rejecting adaptations such as buffering or asynchronous communication, which preserve all safety-critical output deadlines but would require relaxed reception timing. We address this limitation by introducing Relaxed Weak Timed Bisimulation (RWTBS), a novel refinement relation that strictly preserves output timing while permitting controlled relaxation of input reception timing. We prove key property preservation and present a symbolic algorithm to decide RWTBS. Our evaluation demonstrates that RWTBS accepts updates rejected by classical refinement, can be used to correctly identify the operating boundary beyond which updates become unsafe, and achieves speedups of up to five orders of magnitude over model-checking with memory savings of three orders of magnitude.
Summary
Research question
Cyber-physical systems are increasingly updated after deployment, and in real-time and safety-critical settings every update has to preserve the guarantees that were verified before. Refinement relations over timed models are an attractive way to show this, because they establish correctness by behavioural inclusion and can be checked component by component instead of model-checking the whole system again. The problem is that classical timed refinement relations, such as timed bisimulation and its variants, demand the same timing for every observable event. They therefore reject perfectly reasonable updates — buffering an input, or communicating asynchronously — that keep every output deadline but receive inputs slightly later. The paper asks how to formalise this natural asymmetry between what a component must deliver on time and what it may consume with some flexibility.
Approach
The paper introduces Relaxed Weak Timed Bisimulation (RWTBS). Emitted events are treated as real-time obligations whose timing must be preserved exactly, while the reception of input events may be relaxed in a controlled way. The model grounds this in explicitly buffered input ports, separating the arrival of an event from its processing; an alternating send/receive constraint bounds buffer occupancy so that the admissible reception delay stays finite.
RWTBS is placed inside a multi-view evolution framework that relates the deployed system, a candidate update derived from a virtual or simulation-based model, and the system specification. The authors prove that RWTBS preserves key properties across updates — including output deadlines and compositional contract preservation — and give a zone-based symbolic algorithm to decide the relation, implemented in C++ with an OpenMP-parallel variant.
A motivating example is a field-survey drone whose GPS-driven position controller gains a GPS–IMU sensor-fusion filter after deployment: the 100 ms waypoint deadline is unchanged, but a GPS fix may now be consumed up to 50 ms after it arrives. Classical timed refinement rejects this update; RWTBS accepts it.
Results
The evaluation compares compositional RWTBS checking against full model checking with UPPAAL on 20 generated timed-automata configurations representative of smart-farming models. RWTBS accepts updates that classical refinement rejects and identifies the operating boundary beyond which an update becomes unsafe. From around three components onwards, compositional checking avoids building the global product automaton: for five- and seven-component systems, RWTBS completes in well under a second where UPPAAL exceeded the ten-hour limit, a speedup of up to five orders of magnitude, with memory use about three orders of magnitude lower.
Why it matters
RWTBS gives engineers working on real-time and cyber-physical systems a formally grounded way to validate post-deployment updates that relax input timing without touching output timing, and to do so compositionally. The relation also underpins the correct-by-construction digital-twin evolution work presented at ASYDE 2026. The paper received the Best Paper Award at MEMOCODE 2026.
Keywords
Relaxed Weak Timed Bisimulation (RWTBS); timed refinement; real-time systems; post-deployment updates; model-based design; timed automata; compositional verification; cyber-physical systems
Cite
Citation for the openly available version on Zenodo. Replace it with the proceedings entry once the MEMOCODE 2026 DOI is available.
@misc{brodo2026rwtbs,
author = {Brodo, Luca and Scalora, Giuseppe and Henkler, Stefan},
title = {Asymmetric Timed Refinement for Correct Post-Deployment Updates in Real-Time Systems},
year = {2026},
howpublished = {ACM/IEEE International Symposium on Formal Methods and Models for System Design (MEMOCODE 2026)},
note = {Best Paper Award. Authors' version available on Zenodo},
publisher = {Zenodo},
doi = {10.5281/zenodo.22746507},
url = {https://doi.org/10.5281/zenodo.22746507}
}