Abstract Digital twins couple computational models with physical systems to enable services such as predictive reasoning and runtime analysis that support decision–making for maintenance, optimisation and system evolution. They create a technically rich setting for applying formal methods throughout the system lifecycle beyond design-time. This tutorial introduces the elements of digital twin technology, identifying emerging opportunities for formal techniques, including the verification of evolving models under uncertainty, integration of heterogeneous models and rigorous composition of digital twin-enabled systems.

Abstract To enable the reuse of Digital Twins, in the form of simulation units or other forms of behavioral models, of single physical components, one must be able to connect and couple them. Current platform and architectures consider mostly monolithic digital twins and offer little support for coupling and checking the consistency of the coupling. The coupling must be internally consistent—satisfy constraints related to their co-simulation—and externally consistent—mirror the structure of the composed physical system. In this paper, we propose an extension to a behavior-extended Digital Twin architecture for individual Digital Twins to include co-simulation scenarios for coupled systems lifted from configuration files, which can be implemented along with a Digital-Twin-as-a-Service platform to make assets reusable in time. To monitor and query these connections, we introduce a semantic lifting service, which interprets the coupled Digital Twins as Knowledge Graphs and enables the use of queries to express internal and external consistency constraints. Two representative case studies for systems with coupled behavior are used for the demonstration of this approach and show that it indeed enables reusability of components and services between different Digital Twins.

This paper presents the FactoryML framework that simplifies the deployment and integration of Machine Learning (ML) models in manufacturing factory environments. FactoryML facilitates packaging of ML models into a portable format and it facilitates the communication of deployed ML models in factory environments via Programmable Logic Controllers. In general FactoryML reduces the barrier to take learned models from a research and development side into an operational setting. The value of FactoryML has been demonstrated in a case study with a Danish company as well.

When different simulation units are coupled together there are different choices to take, in particular regarding the granularity of such a co-simulation. When prototyping systems, it is typically favourable to get an initial idea of how a collection of simulation units work together without spending too much time setting up the orchestration. However, the granularity of such a simulation may be far away from what is needed in relation to the purpose of the simulation. In order to enable more flexibility and control over the co-simulation it is necessary to be able to steer the orchestration in a more detailed manner. This paper presents an open source co-simulation orchestration engine based on the Functional Mockup Interface standard but with a Domain Specific Language (DSL) enabling detailed control between the individual simulation units. The same tool can thus be used right out of the box for low-granularity co-simulation, and for high-granularity simulation the DSL enable a significant flexibility.

Abstract Digital twin (DT) technology has been a topic with academic and industrial coverage in recent years. DTs are intended to be a virtual high‐fidelity representation of a physical counterpart. Its complex nature requires several components to create and run a DT, and that is why many DT frameworks have been proposed in the literature. There are also many surveys of DTs, but none that is bottom‐up with concrete examples and focused on open‐source software. This survey analyzes 14 open‐source DT frameworks in 10 different dimensions, which are then categorized in six different groups according to their modeling and technological domain, to present the reader different options for creating and managing DT applications, and to understand potential combinations, uses, and limitations of the tools. It also presents a case study with five of the explored DT frameworks, describing the process on how the DT is set up and comparing their capabilities based on the services to be provided by the DT. Finally, it discusses advantages and limitations of the tools according to domain, requirements, and scope, relevant aspects regarding built‐in simulations and data analytics, theory‐to‐practice transition, and advantages/disadvantages of using open‐source software instead of commercial. Main limitations of the study due to its narrow niche, conclusions, and opportunities for future research regarding the potential room for improvement in terms of out‐of‐the‐box features and services for DTs, are also shown.

Digital Twin (DT) technology has gained a great deal of attention as an enabling technology, due to the benefits it can provide in relation to monitoring, optimization, efficiency, and decision-making of their physical counterparts. Developing DTs is however not an easy task, since it relies on several modeling methods and implementation aspects. Several DT platforms have emerged recently to cover the design and development of DTs, and most of them use an object-oriented paradigm.In this paper, we propose a modeling approach for DTs in cooperative systems that provides composition and reusability. This approach extends from information modeling approaches for DTs to include the representation of behavioral models and semantic relationships through an ontology. By including the semantic layer in the modeling approach, inferences are also enabled based on semantic rules and queries.The approach is translated into an object-oriented module and used in a case study composed of two cooperative robotic arms. The demonstration shows that this approach supports the modeling and functional aspects of DT systems and increases the reusability of developed DTs through composition.

Evaluating the product quality in an assembly machine is critical yet time-consuming since, in product assessment in batch manufacturing, a certain amount of products should be investigated in an invasive manner. However, continuous manufacturing ensures product quality assessment during assembly with high efficiency and traceability. This paper proposes a quality assessment method for an industrial use case. First, the data is prepared based on two indicators and expert knowledge. Then two data classification approaches (one-class classification and binary classification) are applied to evaluate the products’ quality by analysing the related data. Finally, the most efficient model is selected to predict the product labels and deviate anomalies from normal products. For the studied use case and the limited number of products, the binary classifier guarantees to detect 100% of defective products. The proposed approach can provide the engineers and operators with understandable extracted process knowledge, and can therefore be adapted to a high-speed manufacturing line where large data volume and process complexity can be problematic.

In today’s world, critical infrastructure is often controlled by computing systems. This introduces new risks for cyber attacks, which can compromise the security and disrupt the functionality of these systems. It is therefore necessary to build such systems with strong guarantees of resiliency against cyber attacks. One way to achieve this level of assurance is using formal verification, which provides proofs of system compliance with desired cyber security properties. The use of Formal Methods (FM) in aspects of cyber security and safety-critical systems are reviewed in this article. We split FM into the three main classes: theorem proving, model checking, and lightweight FM. To allow the different uses of FM to be compared, we define a common set of terms. We further develop categories based on the type of computing system FM are applied in. Solutions in each class and category are presented, discussed, compared, and summarised. We describe historical highlights and developments and present a state-of-the-art review in the area of FM in cyber security. This review is presented from the point of view of FM practitioners and researchers, commenting on the trends in each of the classes and categories. This is achieved by considering all types of FM, several types of security and safety-critical systems, and by structuring the taxonomy accordingly. The article hence provides a comprehensive overview of FM and techniques available to system designers of security-critical systems, simplifying the process of choosing the right tool for the task. The article concludes by summarising the discussion of the review, focusing on best practices, challenges, general future trends, and directions of research within this field.

This paper demonstrates a step on the transition towards a digital twin for a desktop version of an agricultural robot. This includes implementation of motor control and in-door localisation capabilities for the robot. Data from the physical twin is streamed to a co-simulation based on the Functional-Mockup Interface, in which a digital twin simulates the robot’s movement. Safety constraints are established inside the digital twin and a proof of concept communication is enabled when such constraints are violated.

Advances in sensing, communications and data analytics have made it possible to construct virtual replicas of Cyber-Physical Systems (CPSs). Such replicas, known as digital twins, can in principle inform decision making during operation and evolution of the systems they model. This short paper introduces the ISoLA 2020/21 series of papers on the technology and practice of engineering digital twins for CPSs. The focus is on the relationship between model-based design, machine learning, digital twins and CPSs.

In this work, we present the initial steps in the development of a digital twin of the agricultural autonomous vehicle, Robotti. A model of the vehicle dynamics is initially developed in the open-source multi-physics code, Chrono, and then wrapped as a Functional Mock-up Unit. We provide an overview of the envisioned digital twin system and a description of currently implemented features. The dynamic system of the vehicle chassis is characterised by the implementation of a revolute joint that ensures wheel–surface contact in uneven terrain. The vehicle dynamics model is applied for testing two scenarios describing the loads on the vehicle as a consequence of this mechanism. Finally, we give pointers to future work on modelling the Robotti and the establishment of a digital twin.

Civil engineering has only recently started the digitalisation journey by standardising around Building Information Models (BIMs). In the process of construction a dimension of time is added in what is called 4D BIM and this can serve as the basis for a digital twin. It is predicted that such a digital twin can enhance the overall overview of status of the construction of a new building by means of different types of sensors, and interpreting these in relation to a BIM. In the construction phase there are rules and regulations targeting the safety of the different kinds of construction workers at the construction site. In this paper we provide a vision of how digital twins can assist with spotting potential violations of the constraints stated by the rules and regulations, and empirically evaluate a proof-of-concept software tool on a large scale, real-world 4D BIM.

A digital twin for a Cyber-Physical System includes a simulation model that predicts how a physical system should behave. We show how to quantify and characterise violation events for a given safety property for the physical system. The analysis uses the digital twin to inform a runtime monitor that checks whether the noise and violations observed fall within expected statistical distributions. The results allow engineers to determine the best system configuration through what-if analysis. We illustrate our approach with a case study of an agricultural vehicle.

Businesses, particularly small and medium-sized enterprises, aiming to start up in Model-Based Design (MBD) face difficult choices from a wide range of methods, notations and tools before making the significant investments in planning, procurement and training necessary to deploy new approaches successfully. In the development of Cyber-Physical Systems (CPSs) this is exacerbated by the diversity of formalisms covering computation, physical and human processes. In this paper, we propose the use of a cloud-enabled and open collaboration platform that allows businesses to offer models, tools and other assets, and permits others to access these on a pay-per-use basis as a means of lowering barriers to the adoption of MBD technology, and to promote experimentation in a sandbox environment.

In modern software development, the practices of continuous integration and DevOps are widely used to increase delivery speed and reduce the time it takes to deploy software changes to production. If formal method tools cannot be efficiently integrated in a DevOps paradigm, then their impact on software development will be reduced. In this paper, we present work addressing this issue through a series of extensions for the Overture tool supporting the Vienna Development Method. These extensions enable Overture to be used in a DevOps setting, through continuous integration and validation of models and generated code via integration with the Jenkins automation server. We frame the integration of formal methods and DevOps in a series of principles, demonstrate the value of this integration through a case study, and reflect on our experiences using formal methods and DevOps in an industrial setting. We hope that this work can help other formal method practitioners integrate their tools with DevOps.

Industrial control systems are moving from monolithic to distributed and cloud-connected architectures, which increases system complexity and vulnerability, thus complicates security analysis. When exhaustive verification accounts for this complexity the state space being sought grows drastically as the system model evolves and more details are considered. Eventually this may lead to state space explosion, which makes exhaustive verification infeasible. To address this, we use VDM-SL's combinatorial testing feature to generate security attacks that are executed against the model to verify whether the system has the desired security properties. We demonstrate our approach using a cloud-connected industrial control system that is responsible for performing safety-critical tasks and handling client requests sent to the control network. Although the approach is not exhaustive it enables verification of mitigation strategies for a large number of attacks and complex systems within reasonable time.

Summary Development of distributed software systems is complex due to the distribution of resources, which complicates validation of system‐wide functionality. Such systems include various facets like functionality and distribution, each of which must be validated and integrated in the final software solution. Model‐based techniques advocate various abstraction approaches to cope with such challenges. To enhance model‐based development, this paper proposes (1) guidelines for development of distributed systems, where the different facets are introduced gradually through systematic modeling extensions, (2) code generation capabilities supporting technology specific realizations, and (3) demonstration of the applicability of our approach using an industrial case study involving the development of a harvest planning system, where the communication infrastructure paradigm changed late in the project. When developing this system, we spent most time validating system‐wide functionality. The model extensions allowed an easier change of the underlying communication paradigm and code generation supported realization of the different system representations.

Cyber-Physical Systems (CPSs) [ 1 ] connect the real world to software systems through a network of sensors and actuators in which physical and logical components interact in complex ways. There is a diverse range of application domains [ 2 ], including health [ 3 ], energy [ 4 ], transport [ 5 ], autonomous vehicles [ 6 ] and robotics [ 7 ]; and many of these include safety critical requirements [ 8 ]. Such systems are, by definition, characterised by both discrete and continuous components. The development and verification processes must, therefore, incorporate and integrate discrete and continuous models. The development of techniques and tools to handle the correct design of CPSs has drawn the attention of many researchers. Continuous modelling approaches are usually based on a formal mathematical expression of the problem using dense reals and differential equations to model the behaviour of the studied hybrid system. Then, models are simulated in order to check required properties. Discrete modelling approaches rely on formal methods, based on abstraction, model-checking and theorem proving. There is much ongoing research concerned with how best to combine these approaches in a more coherent and pragmatic fashion, in order to support more rigorous and automated hybrid-design verification. It is also possible to combine different discrete-event and continuous-time models using a technique called co-simulation. This has been supported by different tools and the underlying foundation for this has been analysed. Thus, the track will also look into these areas as well as the industrial usage of this kind of technology.

Engineering complex Cyber-Physical Systems, such as emission reduction control systems for large two-stroke engines, require advanced modelling of both the cyber and physical aspects. Different tools are specialised for each of these domains and a combination of tools validating different properties is often desirable. However, it is non-trivial to be able to combine such different models of different constituent elements. In order to reduce the need for expensive tests on the real system it is advantageous to be able to combine such heterogeneous models in a joint co-simulation in order to reduce the overall costs of validation. This paper demonstrates how this can be achieved for a commercial system developed by MAN Diesel & Turbo using a newly developed tool chain based on the Functional Mock-up Interface standard for co-simulation supporting different operating systems. The generality of the suggested approach also enables future scenarios incorporating constituent models supplied by sub-suppliers while protecting their Intellectual Property.

Abstract A model checker is an automatic tool that traverses a specific structure (normally a Kripke structure referred as the modelM) to check the satisfaction of some (temporal) logical propertyf. This is formally stated as M⊧f . For some formal notations, the modelMof a specificationS(written in a formal languageL) can be described as a labelled transition system (LTS). Specifically, it is not clear in general how usual tools such as SPIN, FDR, PAT, etc., create the LTS representation from a given process. Although one expects the coherence of the LTS generation with the semantics ofL, it is completely hidden inside the model checker itself. In this paper we show how to create a model checker forL, using a development approach based on its operational semantics. We use a systematic semantics embedding and the formal modeling using logic programming and analysis (FORMULA) framework to this end. We illustrate our strategy considering the formal language COMPASS modelling language (CML)—a new language that was based on CSP, VDM and the refinement calculus proposed for modelling and analysis of systems of systems. As FORMULA is based on satisfiability modulo theories solving, our model checker can handle communications and predicates involving data with infinite domains by building and manipulating a symbolic LTS. This goes beyond the capabilities of traditional CSP model checkers such as FDR and PAT. Moreover, we show how to reduce time and space complexities by simple semantic modifications in the embedding. This allows a more semantics-preserving tuning. Finally, we show a real implementation of our model checker in an integrated development platform for CML and its practical use on an industrial case study.

This paper introduces a generic solution for gradually moving from a model of an embedded system to include embedded hardware and software components into the simulation of the model. Our technique enables combined execution (co-execution) of system components models expressed in the VDM-RT formalism with actual hardware/software realizations through the application of Hardware In the Loop (HIL) simulation. Introducing such component realizations in the simulation increases the fidelity of the simulation outcome, thus enabling improved prediction of properties for the system realization.

The formal modelling of System of Systems (SoS) is challenged by the autonomy of the participating constituent systems, as system owners may not be willing to share executable models that precisely describe their system's internals. This paper describes an approach for using distributed simulation within a collaborative development environment to enable the analysis of the entire SoS, without the detailed models of the constituent systems being shared.

The effective use of model-based formal methods in the development of complex embedded systems requires the integration of discrete-event models of controllers with continuous-time models of their environments. This paper proposes a new approach to the development of such combined models (co-models), in which an initial discrete-event model may include approximations of continuous-time behaviour that can subsequently be replaced by couplings to continuous-time models. An operational semantics of co-simulation allows the discrete and continuous models to run on their respective simulators and managed by a coordinating co-simulation engine. This permits the exploration of the composite co-model's behaviour in a range of operational scenarios. The approach has been realised using the Vienna Development Method (VDM) as the discrete-event formalism, and 20-sim as the continuous-time framework, and has been applied successfully to a case study based on the distributed controller for a personal transporter device.

Combinatorial testing in VDM involves the automatic generation and execution of a large collection of test cases derived from templates provided in the form of trace definitions added to a VDM specification. The main value of this is the rapid detection of run-time errors caused by forgotten preconditions as well as broken invariants and post-conditions. Trace definitions are defined as regular expressions describing possible sequences of operation calls, and are conceptually similar to UML sequence diagrams. In this paper we present a tool enabling test automation based on VDM traces, and explain how it is possible to reduce large collections of test cases in different ways. Its use is illustrated with a small case study.

Abstract We describe the design and delivery of two courses that aim to develop skills of use to students in their subsequent professional practice, whether or not they apply formal methods directly. Both courses emphasise skills in model construction and analysis by testing rather than formal verification. The accessibility of the formalism is enhanced by the use of established notations (VDM-SL and VDM ++ ). Motivation is improved by using credible examples drawn from industrial projects, and by using an industrial-strength tool set. We present examples from the courses and discuss student evaluation and examination performance. We stress the need for exercises and tests to support the development of abstraction skills.

The Vienna development method (VDM) is one of the longest established and best known formal methods. Recent developments in VDM have included its extension to support object-oriented design and concurrency in VDM++ and providing a capability for modelling real-time distributed systems. VDM is model-oriented - the formal language is used to construct a model of the system of interest, given in terms of data and functionality. In this paper, we draw on experience in developing the semantics and tool support for VDM, and in applying VDM technology in industry, to identify achievements and challenges in providing lightweight but effective formal methods.

Abstract. This document gives a short overview of how VDMTools® can be used in different stages of the system/software development process. The application used is a cash dispensing machine, first introduced at the FM'99 Symposium as the basis for a competition amongst tool vendors. The document provides an overview of how we at IFAD envisage that a problem such as this one should be attacked using VDMTools®.

Abstract Some specification languages, such as VDM-SL, allow expressions whose values are not fully determined. This may be convenient in cases where the choice of value should be left to a later stage of development. We consider a simple functional language including such under-determined expressions and present a denotational semantics for the language along with a set of proof rules for reasoning about properties of under-determined expressions. One of the specific problems considered is the combination of under-determinedness and a least fixed point semantics of recursion. Soundness of the proof rules is also discussed.

Abstract This short communication is a response to [MuS93] investigating their ACS system specification. The main point in this paper is that executing specifications can be used as a feasible way of validating them. It is essential to have tool support which enables one to write a generally not executable specification, and then prototype (parts of) it directly in the specification language, without translating it into some other prototyping language.

Abstract This paper presents a formal semantics of data flow diagrams as used in Structured Analysis, based on an abstract model for data flow transformations. The semantics consists of a collection of VDM functions, transforming an abstract syntax representation of a data flow diagram into an abstract syntax representation of a VDM specification. Since this transformation is executable, it becomes possible to provide a software analyst/designer with two ‘views’ of the system being modelled: a graphical view in terms of a data flow diagram, and a textual view in terms of a VDM specification. In this paper emphasis is on the motivation for the choices made in the transformation. The main aspects of the transformation itself are described using annotated VDM functions with some examples.

This paper discusses the impact of the standardisation of (non-executable) specification languages; standardisation can increase the interest in, and acceptance of, a specification language, and it stimulates the development of tool support for such a language. It is argued that a specification language should preferably be formally defined. The ISO/VDM-SL standard (under construction) is used as an illustration. The fact that many specification languages are non-executable causes problems in the areas of conformance and compliance. These problems are touched upon.