Contract-based Verification of Digital Twins
Authors:
Muhammad Naeem,
Cristina Seceleanu
Abstract:
Digital twins are becoming powerful tools in industrial applications, offering virtual representations of cyber-physical systems. However, verification of these models remains a significant challenge due to the potentially large datasets used by the digital twin. This paper introduces an innovative methodology for verifying neural network-based digital twin models, in a black-box fashion, by integ…
▽ More
Digital twins are becoming powerful tools in industrial applications, offering virtual representations of cyber-physical systems. However, verification of these models remains a significant challenge due to the potentially large datasets used by the digital twin. This paper introduces an innovative methodology for verifying neural network-based digital twin models, in a black-box fashion, by integrating model checking into the process. The latter relies on defining and applying system-level contracts that capture the system's requirements, to verify the behavior of digital twin models, implemented in Simulink. We develop an automated solution that simulates the digital twin model for certain inputs, and feeds the predicted outputs together with the inputs to the contract model described as a network of timed automata in the UPPAAL model checker. The latter verifies whether the predicted outputs fulfill the specified contracts. This approach allows us to identify scenarios where the digital twin's behavior fails to meet the contracts, without requiring the digital twin's design technicalities. We apply our method to a boiler system case study for which we identify prediction errors via contract verification. Our work demonstrates the effectiveness of integrating model checking with digital twin models for continuous improvement.
△ Less
Submitted 7 April, 2025;
originally announced June 2025.
An Energy-aware Mutation Testing Framework for EAST-ADL Architectural Models
Authors:
Raluca Marinescu,
Predrag Filipovikj,
Eduard Paul Enoiu,
Jonatan Larsson,
Cristina Seceleanu
Abstract:
Early design artifacts of embedded systems, such as architectural models, represent convenient abstractions for reasoning about a system's structure and functionality. One such example is the Electronic Architecture and Software Tools-Architecture Description Language (EAST-ADL), a domain-specific architectural language that targets the automotive industry. EAST-ADL is used to represent both hardw…
▽ More
Early design artifacts of embedded systems, such as architectural models, represent convenient abstractions for reasoning about a system's structure and functionality. One such example is the Electronic Architecture and Software Tools-Architecture Description Language (EAST-ADL), a domain-specific architectural language that targets the automotive industry. EAST-ADL is used to represent both hardware and software elements, as well as related extra-functional information (e.g., timing properties, triggering information, resource consumption). Testing architectural models is an important activity in engineering large-scale industrial systems, which sparks a growing research interest. The main contributions of this paper are: (i) an approach for creating energy-related mutants for EAST-ADL architectural models, (ii) a method for overcoming the equivalent mutant problem (i.e., the problem of finding a test case which can distinguish the observable behavior of a mutant from the original one), (iii) a test generation approach based on UPPAAL Statistical Model Checker (SMC), and (iv) a test selection criteria based on mutation analysis using our MATS tool.
△ Less
Submitted 4 February, 2018;
originally announced February 2018.
