Formal Methods meet Digital Twins: Challenges and Opportunities

Abstract

The advent of digital twins gives us an opportunity to reflect on the relationship between models and modelled systems. We may 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 between an ecosystem of models and 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 modelled system’s behaviour. In this paper, we discuss key concepts of digital twins from a formal methods perspective and suggest opportunities and challenges for formal methods in digital twin systems. In particular, we consider how formal techniques can be integral to the digital twin, both in terms of digital twin technology and in terms of digital twin models, as well as notions of correctness for the digital twin itself.