Correct-by-Construction Evolution of Digital Twins for Real-Time Autonomous Systems

Abstract

Safety-critical cyber-physical systems must evolve---through adaptation and post-deployment updates---without forfeiting the guarantees on which their certification rests. Yet digital-twin (DT)--based model-based systems engineering (MBSE) lacks a formal mechanism for preserving correctness as the physical twin (PT) and its DT co-evolve. We argue that refinement can play this role twice: as a correctness guarantee and as a constructive device that automates deployment. We present a refinement-based paradigm for DT-based MBSE that organizes correctness into a small set of locally verifiable obligations over a multi-view decomposition and two flows for design and evolution. The central evolution obligation is instantiated by Relaxed Weak Timed Bisimulation (RWTBS), which allows a DT to propose updates to its PT that preserve output-timing while tolerating bounded input-timing flexibility. The same discipline then compiles timed automata into FreeRTOS and ROS~2 code that refines its model up to a single bounded relaxation---correct by construction.