Keywords

1 Introduction

In Cyber-Physical Systems (CPSs), computing and physical processes interact closely. Their effective design therefore requires methods and tools that bring together the products of diverse engineering disciplines. Without such tools it would be difficult to gain confidence in the system-level consequences of design decisions made in any one domain, and it would be challenging to manage trade-offs between them. How, then, can we support such multidisciplinary design with semantically well-founded approaches in a cost-effective manner?

In the INTO-CPS project we start from the view that disciplines such as software, mechatronic and control engineering have evolved notations and theories that are tailored to their needs, and that it is undesirable to suppress this diversity by enforcing uniform general-purpose models [15, 31] Our goal is to achieve a practical integration of diverse formalisms at the semantic level, and to realise the benefits in integrated tool chains. In order to demonstrate that the technology works industrially it has been applied in very different application domains (e.g., [12, 17, 19, 30, 34, 38]).

To the CPS engineer, the system of interest includes both computational and physical elements, so the foundations, methods and tools of CPS engineering should incorporate both the Discrete-Event (DE) models of computational processes, and the continuous-value and Continuous-Time (CT) formalisms of physical dynamics engineering. Our approach is to support the development of collaborative models (co-models) containing DE and CT elements expressed in diverse notations, and to support their analysis by means of co-simulation based on a reconciled operational semantics of the individual notations’ simulators [18]. This enables exploration of the design space and allows relatively straightforward adoption in businesses already exposed to some of these tools and techniques. The idea is to enable co-simulation of extensible groups of semantically diverse models, and at the same time the semantic foundations are extended using Unifying Theories of Programming (UTP) to permit analysis using advanced meta-level tools that are primarily targeted towards academics and thus not considered as a part of the industrial INTO-CPS tool chain.

Given the considerable interest in model-based CPS engineering, we believe that it is useful to consider what the Unique Selling Points (USPs) are for integrated tool chains. In this paper, we first provide an overview of what we consider the main USPs of the INTO-CPS technology from the perspective of industry use (Sect. 2). We then describe the open INTO-CPS tool chain (Sect. 3). In order to realise the benefits of the tools it is important to develop guidance for their use in collaborative modelling, and this is described in Sect. 4. We discuss our approach to providing integrated semantic foundations needed to underpin such co-modelling (Sect. 5) before looking forward (Sect. 6).

2 The Unique Selling Points

In our work on INTO-CPS, we have sought to deliver the following distinctive features, relevant to the industrial use of co-modelling and co-simulation technology. We see the main USPs as:

  1. 1.

    Faster route to market for engineering CPSs: In a highly active CPS marketplace, getting the right solution first time is essential. We believe that the interoperability of tools in the INTO-CPS tool suite enables a more agile close collaboration between stakeholders with diverse disciplinary backgrounds.

  2. 2.

    Avoiding vendor lock-in by open tool chain: Some commercial solutions provide at least a part of the functionality provided by the INTO-CPS tool chain with a high level of interoperability. However, in particular for Small and Medium-sized Enterprises (SMEs), there is a risk of being restricted in the choice of specialist tools.

  3. 3.

    Exploring large design spaces efficiently: CPS design involves making design decisions in both the cyber and physical domains. Trade-off analysis can be challenging. Co-simulation enables the systematic exploration of large design spaces in the search for optimal solutions.

  4. 4.

    Limiting expensive physical tests: CPS development often relies on the expensive production and evaluation of a series of physical prototypes. Co-simulation enables users to focus on testing different models of CPS elements in a virtual setting, gaining early assessment of CPS-level consequences of design decisions.

  5. 5.

    Enabling traceability for all project artefacts: In both documenting the coverage and quality of analysis and in managing the consequences of design change, there is a need to support the maintenance of traceable links between the many diverse artifacts produced during CPS development. We have sought to provide a basis for delivering levels of design traceability.

Tools as described in Sect. 3 will not, on their own, deliver these features. Methods guidance is needed to ensure that users get the greatest benefit from integrating co-modelling in their own development contexts. Firm semantic foundations are required in order to build confidence in the analyses that they deliver. To these ends, we have worked on methodological and semantic integration, discussed in Sects. 4 and 5, respectively.

3 The INTO-CPS Tool Chain

We have developed an open integrated tool chain to allow n-ary co-simulation of a wider range of model types. In order to facilitate this, we have developed an extensible semantic foundation using UTP. Figure 1 gives a graphic overview of the tool chain, which has been developed in the INTO-CPS project.

In the INTO-CPS tool chain, requirements and CPS architectures may be expressed using SysML. We have defined a special CPS SysML profile that allows cyber and physical system elements to be identified such that each of these elements corresponds to a constituent model [1, 3]. From each element, we generate an interface following the Functional Mockup Interface (FMI) standardFootnote 1. In our approach the tools in which the constituent models are developed can then import these interfaces and export conformant executable Functional Mockup Units (FMUs) following version 2.0 of the FMI standard for co-simulation.

Heterogeneous system models can be built around the FMI interfaces, permitting these heterogeneous multi-models to be co-simulated, and to allow static analysis, including model checking (of appropriate abstractions). A Co-simulation Orchestration Engine (COE) manages the co-simulation of multi-models and is built by combining existing co-simulation solutions. The COE has also been used with FMUs produced with other tools including ModelonFootnote 2, DymolaFootnote 3, 4diacFootnote 4 and SimulationXFootnote 5. In addition a special 3D FMU capability has been enabled using the Unity game engineFootnote 6. This also enables incorporation of 3D glasses such as Oculus Rift enabling a special experience with new CPSs in a virtual setting, before the CPSs are implementedFootnote 7. The COE permits hardware-in-the-loop and software-in-the-loop analysis [19] and it is possible to use it in a distributed fashion. Thus, interoperability in relation to simulation of complex models of CPSs divided up in constituent models expressed using different formalisms and different tools is ensured. This is an important part of USP 1.

Results of multiple co-simulations can be collated, permitting systematic Design Space Exploration (DSE), and allowing test automation based on test cases generated from the SysML requirement diagrams [39]. The ability of both carrying out exploratory experiments as well as systematic testing a combination of constituent models leads to USP 3 since these features enable exploration of very large candidate design spaces. In particular the ability of visualising the results of co-simulations using the 3D FMU described above with the DSE capability (described further in Sect. 4.3) leads to USP 4 limiting the number of physical tests that needs to be carried out, which in particular is important whenever these are expensive to carry out or difficult to monitor the results of.

Fig. 1.
figure 1

The INTO-CPS Tool Chain

Full size image

CPS SysML profile has been demonstrated in ModelioFootnote 8. FMI-conformant constituent models have been produced in Overture from VDM-RT, and the Continuous-Time (CT) formalisms 20-sim and OpenModelica [23]Footnote 9. A graphical front-end for the entire INTO-CPS tool chain called the INTO-CPS Application has been developed based on the cross-platform Electron technology [14]. This is developed as a desktop application, but using web technologies to enable a smoother transition to delivering this as an on-line web service should this be desirable in the future.

Multidisciplinary co-modelling and co-simulation naturally generate many design artifacts, including co-models, co-simulation inputs and outputs, requirements, code, etc. Such large design sets are expected to evolve as smart systems are developed by gradual integration of existing elements, and as elements change. The interrelationships between them are vital for allowing validation and third-party assurance. We have used the PROVFootnote 10 model to record the temporal relations between activities, entities and agents within a process (which we term provenance), and traceability has been supplied based on the Open Services for Lifecycle Collaboration (OSLC) standardFootnote 11. In INTO-CPS, we have regarded it as a priority to lay foundations for provenance and traceability support in the tool chain; all the baseline tools have been extended with such OSLC support [32]. The openness resulting from the combination of FMI and OSLC contributes significantly to USP 2, giving freedom to choose the tools that best fit the purpose of each individual aspect of a CPS.

4 The INTO-CPS Methodology

Our work on methods aims to develop concrete guidelines, frameworks, and patterns for co-modelling and co-simulation that can be adapted to existing development processes, rather than defining a single workflow. Specifically, we focus on model-based CPS requirements engineering, architectural modelling in SysML, traceability and provenance, and DSE.

We support model-based systems engineering approaches because of their potential to enable early detection of potential bottlenecks and defects before commitment is made to physical prototypes (USPs 1 and 4). We advocate the use of architectural models that define the major elements of a system, their relationships and interactions. The bulk of our architectural modelling work uses SysML, which allows us to describe both digital interfaces between components in terms of the properties or functionality provided or required, and physical interfaces in terms of physical flows (e.g. material) between components.

An architecture diagram is a symbolic representation of part of an architectural model. An architectural view is typically an architecture diagram that includes specific system facets. An architectural framework is a set of architectural views defined to support a task, role, or industry [26]. A SysML profile is a collection of extensions to SysML that support a particular domain. We have developed a SysML profile consisting of diagrams for defining cyber, physical components, as well as components representing environment and visualisation elements (the delivering graphical presentation of co-simulation outputs).

4.1 Requirements Engineering

CPSs share important characteristics with Systems-of-Systems (SoSs) [35]. Cyber and physical elements can be independently owned and managed, evolve over time, and are distributed [40]. CPSs add the challenge of differing domain contexts [47]. In developing model-based requirements engineering approaches for CPSs, we have therefore extended a systematic approach to SoS requirements engineering, the SoS Approach to Context-based Requirements Engineering (SoS-ACRE) [27]. SoS-ACRE provides several views that encourage the systematic consideration of requirement context, sources and stakeholders.

A survey of our industry collaborators showed that a wide range of tools were used for requirements management and modelling, ranging from Microsoft Word to IBM Rational DOORS. It was therefore important to develop an approach that, while it could be supported by specialist notations like SysML, could also be adopted using document-based tools. This is a key facet of providing an open tool chain (USP 2). For example, SoS-ACRE can be adapted to these CPS needs as follows:

 

Source Element View (SEV):

which identifies the sources from which requirements are derived. This could be represented as a SysML block definition diagram, an Excel table or a Word document, or by simply referring to source documents using OSLC traces.

Requirement Description View (RDV):

defines the requirements. This could be a SysML requirements diagram, or in tabular form, or in DOORS.

Context Definition View (CDV):

identifies interested stakeholders and points of context, including customers, suppliers and system engineers themselves. These could be SysML block definition diagrams, Excel tables or Word documents, and can be used to identify the CT/DE elements of a system.

Requirement Context View (RCV):

defined for each constituent system context identified in CDVs. A Context Interaction View (CIV) is then defined to understand the overlap of contexts and any common/conflicted views on requirements. In SoS-ACRE, RCVs and CIVs are both defined with SysML use case diagrams. Excel could be used if unique identifiers are defined for contexts and requirements as described earlier.

Given that we aim to support the integration of co-simulation into established development processes, we realise the SoS-ACRE views using a range of combinations of SysML with other tools. For example, a single SysML model for both requirements engineering and architectural modelling will contain all SoS-ACRE views (SEV, RDV, CDV, RCV and CIV), in addition to diagrams defined using the INTO-CPS profile for the CPS composition and connections. Modelling in this way enables trace links to be defined inside a single SysML model, using <<trace>> relationships (e.g., Fig. 2). By contrast, one might combine URIs for the source elements with an Excel document for the RDV, CDV, RCV and CIV. As above, SysML can be used to define the architecture in a single model. Trace links using OSLC may then be used to link source elements, rows of Excel documents (with internal tracing using unique identifiers referenced between sheets), and architectural elements of the SysML architectural model. Figure 3 presents an example with URI, Excel and SysML models and OSLC links between the artifacts.

Fig. 2.
figure 2

Single SysML model – model overview

Full size image
Fig. 3.
figure 3

URI, Excel and SysML – model overview

Full size image

4.2 Traceability and Provenance

USP 5 deals with the need to support engineers navigating the complexities of CPS design sets. INTO-CPS considers two tool-supported methods for recording design rationale. Traceability associates one model element (e.g. requirements, design artifacts, activities, software code or hardware) to another. Requirements traceability “refers to the ability to describe and follow the life of a requirement, in both a forwards and backwards direction” [24]. Provenance “is information about entities, activities, and people involved in producing a piece of data or thing, which can be used to form assessments about its quality, reliability or trustworthiness” [33].

4.3 Design Space Exploration

USP 3 is the ability to sweep over the design space to identify optimal combinations of parameters with respect to evaluation criteria. A design parameter is a property of a model that varies the behaviour described, but remains constant during a simulation; a variable is a property that may change during a simulation. Where two or more models represent different solutions to the same problem, these are considered design alternatives. In INTO-CPS, design alternatives are defined using either a range of parameter values or different multi-models.

Designing DSE experiments can be complex and depends closely on the multi-model being analysed. Engineers need, therefore, to be able to model at an early stage of design how the experiments relate to the model architecture, and where possible trace from requirements to the analysis experiments. We have defined a SysML profile for modelling DSE experiments in a consistent and traceable way. The profile comprises five diagrams for defining parameters, objectives and rankings. Based on a requirements analysis (e.g. an RDV coming out of the processes described in Sect. 4.1), we identify objectives, and use the SysML profile for DSE to define the parameters, objectives and ranking function, traced to the requirements.

We use the INTO-CPS tool chain to simulate each design alternative. Whilst exhaustively seaching the design space, evaluating and ranking each design is acceptable on small-scale studies, it quickly becomes infeasible as the design space grows. For example, varying n parameters with m alternative values produces a design space of \(m^n\) alternatives. We have therefore implemented genetic approaches [16].

5 The Underlying Unified Semantic Approach

Since CPSs are networks of computational devices interacting with the world through their sensors and actuators, CPS models must combine discrete computational models with continuous physical environmental models. CPS engineering necessarily involves a wide range of modelling and programming paradigms [13], including concurrency, real-time, mobility, continuous variables, differential equations, object orientation, and diagrammatic languages. Practical CPS engineering uses a variety of domain-specific and general-purpose languages, such as Simulink, Modelica, SysML, Java, and C, and engineering trustworthy CPS requires that semantic models for these languages are integrated in a consistent way, which then enables reasoning about an entire CPSFootnote 12.

In practice, semantic integration is often achieved using the FMI standard [6], mentioned above, which describes a CPS using a network of FMUs to simulate components and their solvers and simulators. Each FMU has observable discrete and continuous variables that can be observed and modified, as well as an interface to drive the simulation engine in various ways. In a co-simulation a master algorithm manages stepping the individual FMUs forward, and distributing information in between time steps. In this way, FMI describes heterogeneous multi-models in different notations with different underlying semantics integrated through a common operational interfaceFootnote 13.

FMI provides a way of experimenting with the combined operational interfaces to heterogeneous models, and so it is useful for validation; but it does not provide the basis for verifying CPS properties. To do that, we need to be able to verify properties, both at the model level and at the multi-model level. One way of doing this is to explore the links between the different semantics. To do this, we use Hoare and He’s Unifying Theories of Programming (UTP) [10, 25, 48] to describe different computing paradigms and their formal connections. We treat the various semantic aspects of a heterogeneous multi-model as individual theories that characterise a particular abstract modelling paradigm. Hoare and Jifeng [25] show how the mathematics of the alphabetised relational calculus can be used to construct a hierarchy of such theories, including an assertional approach to hybrid imperative parallel programming and control of continuous physical phenomena. Within this hierarchy, there are theories of real-time programming [45], object-oriented programming [43], security and confidentiality [4], mobile processes [44], probabilistic modelling [7], and hybrid systems [20]. The FMI API itself has been given a UTP-based semantics [11, 49] that can be used as an interface to the semantic model of individual FMUs.

Our approach to practical CPS verification in the meta-tools is based on the theorem prover for UTP built on Isabelle/HOL [36], which we call Isabelle/UTP [21, 22]. Isabelle is a powerful automated proof assistant that was used, for example, in the seL4 microkernel verification project [29]. Isabelle include recent work on formalising the integral and differential calculus, real analysis, and Ordinary Differential Equations (ODEs) [28], work that we are applying to verification of hybrid systemsFootnote 14.

Crucial to all of these developments is the ability to integrate external tools into Isabelle that can provide decision procedures for specific classes of problems. Isabelle is well suited to such integrations due to its architecture based on the ML and Scala programming languages, both of which can be used to implement plugins. Isabelle is sometimes referred to as the Eclipse of theorem provers [46]. The sledgehammer tool [5], for example, integrates a host of first-order automated theorem provers and SMT solvers, which often shoulder the burden of proof effort. Sledgehammer has been used both at the theory engineering level, for constructing an algebraic hierarchy of verification logics (Kleene algebras), and also at the verification level, where it is used to discharge first-order proof obligations [2]. For verification of hybrid systems, it is necessary to integrate Isabelle with computer algebra systems like Mathematica, MATLAB, and SageMath, to provide solutions to differential equations, an approach that has been previously well used by the KeYmaera tool [41, 42].

Our vision is the use of Isabelle and UTP to provide the basis for CPS verification through formalisation of the fundamental building-block theories of CPS multi-modelling, and the integration of tools that implement these theories for coordinated verification.

6 Concluding Remarks

Integrated modelling such as that presented in this paper is essential to efficient engineering of CPSs. We believe that openness of the tool chain using different standards, the methodology supporting it and the underlying unified semantic approach jointly enable stakeholders with different disciplinary backgrounds to collaborate in the development of CPSs. This is by no means the only scientific approach by which such systems can be developed, but we think that it is a promising candidate that has future extension possibilities as well.

In the current version of the FMI standard there are a number of limitations. This includes that it is not able to cope with the modelling of the network communication in a natural manner and it is incapable of modelling dynamic reconfigurations. Thus, in a future extension it would be ideal if it would be possible to enable such capabilities for example to be able to appropriately model and develop constituents with their own independent behaviour. This could mean integration of machine learning capabilities as well as software agents including potentially incorporation of human-in-the-loop. Initial work with humans included have already started [37] but it is easy to imagine that it would be advantageous to combine this further in the future with human centered design ideas. We envisage great capabilities for the future that would bring additional USPs to the table.