Abstract
The advent of digital twins gives us an opportunity to reflect on the relationship between models and modelled systems. When is there a beautiful, formal model lurking in the shadows of some messy real-world behaviour? We should think of digital twins not merely as models, but as systems for model management, integration and composition. In fact, digital twins are model-centric systems that maintain a two-way connection with the modelled system, realised through streams of observations and streams of interventions. This connection introduces agility as the digital twin can typically both adapt its models on-the-fly to changes in a modelled system and influence the system’s behavior. In this talk, we will explore key concepts of digital twins from a formal methods perspective and discuss opportunities and challenges for formal methods in digital twin systems. In particular, we consider notions of correctness for digital twins, as well as how formal techniques can be an integral part of the digital twin itself, both in terms of digital twin technology and in terms of digital twin models.
