Digital Twins are a trend topic in the industry today to either manage runtime information or forecast properties of devices and products. The techniques for Digitial Twins are already employed in several disciplines of formal methods, in particular, formal verification, runtime verification and specification inference. In this paper, we connect the Digital Twin concept and existing research areas in the field of formal methods. We sketch how digital twins for software-centric systems can be forged from existing formal methods.
System (Physical Domain)
Digital Twin Generic Model
Configuration
Update
Prediction Contribution In this paper, we apply several formal methods and tools to establish a framework for Digital Twins of reactive systems using formal software contracts. Therefore, we focus on twinning the software behavior of a reactive system operation according to its formal model, which we define through contracts.
The Digital Twin allows forecasting properties that depend on the behavior of the system. However, forecasting is not limited to the specific instance to which it is twinned. Moreover, knowledge learned from observation can be shared between Digital Twins, and What-if analyses are available. To achieve this, we show how existing formal methods, in particular formal verification, runtime verification, specification mining and program repair, can be combined for a Digital Twin.
A meta-model for Digital Twin For this paper, we assume a simple meta-model of Digital Twins, sketched in Figure 1. This meta-model consists of the original system that exists in the real world. Such systems can be cyber-physical systems, like cars, automated production systems, or energy systems. For the purposes of this discussion, we only consider pure software systems.
The Digital Twin is then a digital representation of an instance of a system. In case of a
cyber-physical system, this can be a specific car or an individual transformer in the energy
system. Coming from the domain of formal methods, we build the Digital Twin by using
symbolic logic based models. We will later use contract-languages to represent the system.
For software systems, the Digital Twin can be split into a generic part that is valid for
all instances of the system parameters, and instance-specific configuration. For example,
the generic consists of the classes and their contracts, but their use and composition is
determined by the instance’s configuration. Note that the Digital Twin also contains
information about the environment. This is similar to the distinction between ABox and
TBox in description logics. The TBox, the generic part, holds the axioms that are valid
for all instances. The ABox, on the other hand, contains the information for the specific
instance [
tions:
The representation of a system as a Digital Twin should enable two opera• Prediction of selected properties. Prediction means reasoning whether a property holds for a specific instance or, due to the symbolic representation, for a family of instances. Moreover, we can perform “What-If” analyses: assuming a diferent configuration, we can predict properties on diferent instances, after change on the system. We can also model a transfer to a diferent environment. Prediction can lead to efects on the system, e.g., only configurations with a good predicted performance are deployed. • The Update process consists of collecting and aggregating information from the (real-world) instance and transferring these into the configuration part of the model. Desired Properties A Digital Twin also has to fulfill some properties. First, it should be faithful in the sense that the derived predictions are precise. If precision is too hard to achieve, we claim at least soundness: The prediction should be a pessimistic (or conservative) evaluation with respect to the safety analysis. The reasoning based on the Digital Twin should never attest safety falsely; if in doubt, it should rather predict non-existing safety issues.
Additionally, compositionality of a Digital Twin brings the same advantages as for the system. Systems can be built up by composition of multiple systems. The same is desirable for the Digital Twins: the Digital Twin of the top system is, ideally, a composition of the Digital Twins of the sub systems.
In the following, we instantiate the Digital Twin meta-model for reactive software systems. For this, we define the individual components: the system and the formal model as well as the prediction and update processes.
A reactive system is characterized by the following properties (cf. [
Reactive systems can be constructed via composition from smaller systems. For example,
Lingua Franca [
Cimatti et al. [
Using the OCRA model, the Digital Twin of a system is its contract, which consists of two properties given in Linear Temporal Logic (LTL). The first property is an assumption on the system inputs. The second one is a guarantee of the system outputs under the given assumptions. Note that LTL is just the language we use for describing sets of traces. It can be replaced by any logic on traces (see below). The advantage of LTL is acceptance by a wide range of tools.
In addition to the contract, the Digital Twin is also aware of the structural architecture of the software given by the composition of subsystems and the information flow between them. Parameterization (or configuration) of a system is established via its input variables and by the selection of the sub-system during the composition.
The contract is a syntactical notion that describe the set of allowed behaviors of a system under a specified set of input traces. The behavior of a correct system is a subset of the allowed behavior. Often, due to the determinism in the system and the indeterminism (or abstraction) in the contract, the allowed behavior is indeed a strict superset of the actual actual behavior. Additionally, a system composition gives a refinement obligation, in which the composition, i.e., the collective of sub-systems, needs to conjointly fulfill the super system’s contracts. Furthermore, the systems within a composition also need to be compatible with each other. Due to the over-approximating character of contracts, the Digital Twin tends to be imprecise, but sound for safety analyses. However, it is not possible to predict liveness properties. Note that proving the correctness of the system is sometimes infeasible, e.g., due to unavailability of the source code, complexity of the system (floating point, state explosion) or lack of knowledge of the environment. Additionally, we do not assume that the system is always compliant with the contract, especially, when the contracts are automatically mined from observation, or extracted from natural language and not carefully designed by the system creator and operators. This increases the need for a robust update that incrementally tighten the coupling between the instance of the system and Digital Twin built from contracts.
There are several update operations. The most simple one is detecting the parameterization of the instance, i.e., determining the values of the diferent inputs.
Moreover, the assumptions and guarantees in the contracts at the top-level and
subsystems needs to be validated during operation to ensure that the system operates in
its expected boundaries. In particular, we check whether a system is correctly invoked
by its outer context or environment, and whether it behaves as specified. To achieve
this, Runtime Verification, such as [
Normally, we want to establish the correctness of a system statically, but some properties
are too hard to be established in advance. In the best case, unexpected
specificationviolating runtime traces are recorded to enable specification mining. Specification mining
is the discipline to extract LTL properties from traces. For example, Tuxedo [
The prediction operation of our Digital Twin can be reduced to the well-established model-checking problem which allows us to verify the validity of a (LTL) property in a given Kripke structure. This covers the validation that each contract is adhered to by the associated system, and that systems are composed in a valid fashion.
But we benefit from the information learned during the Update operation: We can testify the contract adherence specifically in the used system configuration, and thus, we can save verification run-time without sufering a loss of verification validity for a specific instance. Furthermore, it may be beneficial to limit the verification process only to the recorded and mined environment of the instance to be validated.
Of course, the Digital Twin allows to conduct “What-If” analyses by altering the parameter of a system, or implementing it into a diferent environment. The latter simply requires changing the mined properties. This also requires tracking the origin of the formulas within the contracts.
But we are not limited to model-checking. Testing or simulation are also in reach by
using the contracts. In particular, formal contracts enable testing and simulation even for
software which is not executable in a simulation environment (e.g., due to inaccessible
resources). There are also more sophisticated techniques. For example, Program Repair
considers altering programs such that the program fulfills its contract. For this, the source
code of the program is mutated until a suitable candidate is found [
Limitations By using assume-guarantee contracts and LTL as the specification language, we focus on describing behavior on a certain abstraction level. This allows us to reason well on the possibility to reach bad system states, but other properties are not predictable. For example, security properties that are expressible as reachability are covered, i.e., integrity of the system, but confidentiality (e.g., secure information flow), and availability (liveness properties) are not. Moreover, runtime predictions, e.g., worst case execution time (WCET), are also not in our setup, due to the abstraction of time in LTL.
Note that OCRA uses LTL, but its approach is not limited to a particular contract
grammar. There are many variants of temporal logics. For example, Metric Temporal
Logic (MTL) extends LTL to include real-time capabilities [
Temporal logic formulas tend to be very hard to understand. Therefore, an additional
goal is comprehensibility of the contracts and thus the Digital Twin. For example,
Generalized Test Tables (GTTs) [
In this paper, we present the idea of using formal contracts – existing in current
designby-contract approaches – for the representation of Digital Twins. Due to tool support, we
focus on reactive systems and LTL, but the principle is also applicable to batch systems.
For example, the Java Modeling Language (JML) [
Software and its refinement. When we fade out the physical environment and
concentrate on the software, we can state that the software, as it is digital, is itself the most
precise definition of its behavior, and can also been seen as its own contract. Every other
contract for a system over-approximates. But the abstraction of contracts is needed,
as it allows us to hide the complexity of the implementation. Indeed, more abstract
software models are often used in software engineering: For example, the buildability of
a user-configurable product is defined by a feature model. Feature models reflect the
compatibility of software modules, which also depends on the behavior of the software.
Evolution of Digital Twins with Relational Verification. For our framework, we have
only considered the classical specification and verification of single traces. A possible
extension is the verification of relational properties [
This work was supported by funding of the Helmholtz Association (HGF) through the Competence Center for Applied Security Technology (KASTEL) and by the research project SofDCar (19S21002), which is funded by the German Federal Ministry for Economic Afairs and Climate Action