A SysML v2 Based Modeling Language and Tool for Task Planning and Runtime Verification with Digital Twins

Digital Twins (DTs) are key enablers for autonomous and adaptive systems, providing a virtual counterpart that mirrors, predicts, and verifies the behavior of a physical asset. In space applications, where communication latency and uncertainty are significant, DTs enable support for automated task planning and runtime verification with formal methods. This paper presents the model-based design approach developed within the ExploDTwin project, introducing the Digital Twin Formal Modeling Language (DTFML), a SysML v2-based modeling language for specifying and analyzing planning and monitoring problems on top of a DT. DTFML extends SysML v2 with constructs for plannable durative activities, observable variables that can be read from telemetries, external functions used to simulate the resource consumption of activities. In this way, the DTFML enables rigorous definition of planning, plan monitoring, and runtime verification problems. The associated SAWS2 (Safety Analysis, Validation and Verification for SysML v2) tool enables automated validation and model checking through integration with formal verification engines. The approach is demonstrated on a space-exploration rover case study, showing its applicability to industrial applications.