1 Introduction

Many technological achievements have been enabled by the field of feedback control systems, which deals with the process of controlling a physical system through a feedback controller. If the feedback controller is implemented as a real-time computer system, the resulting configuration of the feedback control system is referred to as embedded control system. Some prime examples of embedded control systems are automotive systems, avionics systems, and smart grid. The typical development process of an embedded control system can be partitioned into two distinct stages: controller design and controller implementation. During the controller design stage, a control systems engineer models the physical plant, derives the feedback control law, and validates the controller design through mathematical analysis and simulation. During the controller implementation stage, a computer systems engineer implements the feedback controller as a real-time computer system.

The field of embedded control systems brings together the fields of control theory and real-time computer systems. However, as noted in [15], the fields of control theory and real-time computer systems typically employ two completely different types of models: analytical models and computational models. As a result, two vastly different design processes are currently popular for the two stages of embedded control system development process: feedback controller design and feedback controller implementation as real-time computer system. Due to the inherent differences between the abovementioned two stages, currently popular development methodologies for embedded control systems support very few correct-by-construction properties and depend heavily on testing the final implementation for creating confidence in the correct operation of an embedded control system under various runtime operating conditions. Therefore, current development techniques for embedded control systems are not capable of efficiently handling the ever-increasing complexity of these systems.

These limitations of the traditional embedded control system development techniques have created interest in taking a fresh look at the abstractions used in the traditional embedded control systems development process, resulting in a new field, cyber-physical systems (CPS) [39, 40]. The aim of CPS research is to develop an integrated theory as well as an integrated development toolset for controller design and controller implementation phases of the embedded control system development process. The hope is that this CPS research will enable the cost-effective development and maintenance of more complex versions of embedded control systems.

Recent CPS research efforts can be divided into two major categories: platform-imperfection-aware feedback controller design and CPS-friendly computing platform design. Under the category of platform-imperfection-aware feedback controller design, theoretical developments from the fields of hybrid systems [3], switched systems [21], time-delay systems [7], networked control systems [41], multi-agent networked systems [29], and game theory [16] are leveraged to develop a feedback controller design that takes into account the imperfections of the runtime computing platform (such as communication delays or failures caused by communication network congestion or cyber security attacks) at the design time [37]. The resulting “platform-imperfection-aware” feedback controller is either robust against the imperfections of runtime computing platform or possesses the capability to switch between different control modes to overcome the imperfections of runtime computing platform. Under the category of CPS-friendly computing platform design, CPS research has focused on specialized runtime computing platforms that have more predictable timing performance or provide correct-by-construction composition of software components. Some examples of this approach are provided in [17, 19, 22].

Model-based development (or model-driven development) of cyber-physical systems has the potential to bind the abovementioned CPS research efforts into an integrated, cross-layer CPS development methodology. In model-based development paradigm, high-level or platform-independent models (PIM) are transformed into lower-level or platform-specific models (PSM) through the process of model transformation. Both high-level and lower-level models are described using their own domain-specific modeling languages (DSMLs) [32]. In this chapter, we propose an approach to model-based development of networked cyber-physical systems (CPS) that is centered on the notion of a standardized design specification language. The proposed design specification language can be used to build a CPS design specification model that can serve as a CPS-aware interface between control systems engineer and embedded systems engineer.

The proposed approach is inspired by the hourglass-shaped architecture of Internet, illustrated in Fig. 3.1. The narrow waist of hourglass-shaped architecture suggests that there is less diversity of protocols at this layer of Internet [2]. Any application that can operate based on the services of IP layer can be deployed on the Internet, and any underlying technology that can transport bytes from one point to another according to IP services can be used in the Internet. Similarly, according to the proposed approach to the model-based development of networked CPS (Fig. 3.2), a wide range of DSMLs (and associated analysis tools) can be utilized to develop a platform-imperfection-aware feedback controller design, which is then specified using a standardized CPS design specification language. The proposed feedback controller design can then be analyzed for mapping on to wide range of runtime CPS computing platforms by utilizing their corresponding DSMLs (and associated analysis tools). This approach can support the goals of an integrated CPS theory and development methodology while still taking into account the differences between the domain-specific skillset that control systems engineers and embedded system engineers typically possess.

Fig. 3.1
figure 1

Illustration of hourglass-shaped architecture of Internet; adapted from [2]

Full size image
Fig. 3.2
figure 2

Illustration of hourglass-shaped model of CPS design and analysis process

Full size image

The rest of the chapter is organized as follows. In Sect. 3.2, we present some related work. In Sect. 3.3, we present the details of the proposed hourglass-shaped architecture for model-based development of networked cyber-physical systems. In Sect. 3.4, we document a number of requirements that any standardized CPS design specification language must satisfy. In Sect. 3.5, we present the overview of a proposed CPS design specification language. In Sects. 3.6–3.8, we discuss the concrete syntax, abstract syntax, and semantics of the proposed CPS design specification language, respectively. In Sect. 3.9, we present the conclusion.

2 Related Work

Figure 3.3 presents a summary of specification languages and analysis tools used in the different stages of a typical embedded control system development process. Simulink [27] (combined with auxiliary tools such as Stateflow [28] and Simscape [26]) has become a de facto standard in the field of embedded control systems for specification and refinement (through simulation) of the feedback controller design, developed by a control engineer through the application of various analytical controller design strategies available in the literature for the field of control theory [5]. Once a feedback controller design has shown acceptable performance in the Simulink-based simulation environment, a computer system engineer takes on the task of implementing this feedback controller design as a real-time computer system. Various tools have been developed over the years to help a computer systems engineer in this process of converting a feedback controller design from a Simulink-based specification to a real-time computer system implementation. Specialized modeling languages, such as UML (combined with MARTE profile) [30], SysML [10], and AADL [8], help in the process of designing the system and software architecture of the required real-time computer system. Specialized programming languages, such as Lustre [12], Esterel [4], Signal [20], and Giotto [14], help in the development of real-time computer system whose timing performance can be formally guaranteed.

Fig. 3.3
figure 3

Embedded control systems: development steps, specification languages, and analysis tools; adapted from [36]

Full size image

Model-based development (MBD) paradigm has also been successfully employed in the domain of embedded control system in order to improve the productivity of a computer systems engineer during the process of conversion of a feedback controller design into a real-time computer system. In MBD paradigm, high-level or platform-independent models (PIM) are transformed into lower-level or platform-specific models (PSM) through the process of model transformation. Both high-level and lower-level models are described using their own domain-specific modeling languages (DSMLs) [32]. A DSML is first defined through a meta-modeling step. A meta-model of a DSML defines the basic constructs (along with their relationships and constraints) that can be used in a DSML. Model transformation step of MBD paradigm uses the meta-models of DSMLs to define transformation rules from higher-level (platform-independent) models to lower-level (platform-specific) models. Model-driven architecture (MDA) [9], model integrated computing (MIC) [18], and eclipse modeling framework (EMF) [11, 33] initiatives represent three popular MBD efforts.

In the domain of embedded control systems, various model transformation (code generation) tools have been developed to automatically generate executable code from Simulink models for various real-time computing platforms. Embedded Coder [25], from Mathworks, Inc., is a commercially available example of such a code generation tool. Another example of a Simulink-based MBD toolset for a more specialized real-time computing platform has been reported in [6].

Building on the MBD paradigm, Sztipanovits et al. [35] describe a methodology for cyber-physical system integration and illustrate their methods on the design of a network of quadrotor UAVs. They identify three design layers: physical, platform, and computation/communication. Their methodology emphasizes component-based design and its associated requirement, compositionality. They identify passivity as a key characteristic that enables composition of control systems. They identify network characteristics required to compositionally analyze the UAV network.

In a later paper, Sztipanovits et al. [34] describe a CPS methodology and tool suite used for vehicle design. Their tool suite embodies two design platforms: the model integration platform describes the semantic relationships between the models used in design; the tool integration platform describes translations between tools in the flow. Their framework allows them to construct design spaces and analyze the characteristics of those design spaces. Their modeling language CyPhyML includes sublanguages to describe components, system architectures, architectural parameters, analysis models, and testbenches.

However, the CPS model-based development community has not been as successful as some other communities in identifying a design flow which promotes the reuse of tools and can support a range of application domains and implementation targets. For instance, the classic text on compilers [1] identifies several steps in the classical compilation process which are common to a broad class of programming languages: lexical analysis, syntactic analysis, semantic analysis, intermediate code generation, code optimization, and code generation. In this classical compilation process, the intermediate code (developed in an intermediate language such as three-address code) plays a pivotal role by providing an independent narrow interface between a set of source code languages and a set of target machines. Similarly, as illustrated in Fig. 3.1 and detailed in [2], the IP layer can be considered the narrow waist of an hourglass-shaped architecture of Internet. Any application that can operate based on the services of IP layer can be deployed on the Internet, and any underlying technology that can transport bytes from one point to another according to IP services can be used in the Internet.

While model-based development of networked cyber-physical systems is a challenging problem, we believe that abovementioned observations from the domains of software compilation and Internet architecture can be leveraged to improve the model-based development process for networked cyber-physical systems. Therefore, in this chapter, we propose an approach to model-based development of networked cyber-physical systems (CPS) that is centered on the notion of a standardized CPS design specification language, capable of playing an analogous role to the intermediate language and the IP layer from the domains of software compilation and Internet architecture.

3 Hourglass-Shaped Architecture for Model-Based CPS Development

Two major categories of CPS research are platform-imperfection-aware feedback controller design and CPS-friendly computing platform design. Model-based development of cyber-physical systems has the potential to bind the abovementioned CPS research efforts into an integrated, cross-layer CPS development methodology. This section presents an approach to model-based development of networked cyber-physical systems (CPS) that is centered on the notion of a standardized design specification language. The proposed design specification language can be used to build a CPS design specification model that can serve as a CPS-aware interface between control systems engineer and embedded systems engineer. The proposed approach is inspired by the hourglass-shaped architecture of Internet, illustrated in Fig. 3.1. The narrow waist of hourglass-shaped architecture suggests that there is less diversity of protocols at this middle layer of Internet [2], while many different protocols can be employed at top and bottom layers of Internet.

According to the proposed hourglass-shaped architecture for model-based networked CPS development, illustrated in Fig. 3.2, a wide range of DSMLs (and associated analysis tools) can be utilized to develop a platform-imperfection-aware feedback controller design, which is then specified using a standardized DSML for CPS design specification. Furthermore, according to the proposed hourglass-shaped architecture, the platform-imperfection-aware feedback controller design (specified using the standardized DSML) can then be analyzed for mapping on to various runtime CPS computing platforms by utilizing corresponding DSMLs (and associated analysis tools).

The proposed hourglass-shaped architecture can enable effective coordination between control systems engineer and embedded systems engineer during model-based development of networked cyber-physical system, while still allowing them to concentrate and specialize in the CPS-aware, model-based tools developed in their respective domains. This approach can support the goals of an integrated CPS theory and development methodology while taking into account the differences between the domain-specific skillset that control systems engineer and embedded system engineer must acquire during their respective academic training.

The proposed hourglass-shaped architecture for model-based development of networked CPS consists of three explicit phases: (1) platform-imperfection-aware feedback controller design, (2) CPS design specification, and (3) constraints-aware platform mapping.

3.1 Platform-Imperfection-Aware Feedback Controller Design

In this phase, control systems engineer designs a feedback controller that takes into account the imperfections of the runtime computing platform (such as communication delays or failures caused by communication network congestion) at the design time. The resulting “platform-imperfection-aware” feedback controller is either robust against the imperfections of runtime computing platform or possesses the capability to switch between different control modes to overcome the imperfections of runtime computing platform. In this phase, control systems engineer utilizes various results from CPS research [37] that have been achieved over the recent years by leveraging the theoretical advances from the fields of hybrid systems [3], switched systems [21], time-delay systems [7], networked control systems [41], multi-agent networked systems [29], and game theory [16].

During this phase, a control systems engineer can utilize any model-based tool from the following three categories: (a) various DSMLs (and associated analysis tools) that were used in the traditional control system design process [26,27,28], (b) recently proposed DSMLs (and associated analysis tools) that are employed by the numerous cyber-physical co-design CPS research efforts [13, 31], and (c) any DSMLs (and associated analysis tools) that are proposed by any future CPS research into integrated cyber-physical design.

3.2 CPS Design Specification

In this phase, the results of the platform-imperfection-aware feedback controller design process are captured using a standardized DSML for CPS design specification. This CPS design specification must capture the sensed and actuated-upon physical plant parameters as well as the networked controller aspects of a CPS design. However, the networked controller aspects of CPS design should not be described by specifying the runtime computing infrastructure, instead networked controller aspects of CPS design should be described at an abstract level by specifying various control nodes and sensor ports, actuator ports, input message ports, and output message ports associated with these control nodes.

This CPS design specification must also capture the feedback control adaptation strategy to handle the imperfect performance of runtime computing and communication platform. This element of CPS design can also be captured at an abstract level by specifying various controller modes of a control node and a mode switching logic based on QoS violations associated with sensor ports, actuator ports, input message ports, and output message ports of the control node. A CPS design specification can also declare some QoS constraints of sensor ports, actuator ports, input message ports, and output message ports to be hard. This will indicate that these QoS properties must be satisfied by runtime computing platform, because there is no safe backup mode of operation in case of violation of these QoS properties.

3.3 Constraints-Aware Platform Mapping

In this phase, the mapping of the CPS design specification (described using standardized DSML) onto various runtime computing platform is analyzed to either choose the most appropriate mapping or figure out the appropriate parameter settings for a runtime computing platform so that the platform can meet the QoS constraints of CPS design (and minimize the time that the system has to spend in a backup mode of operation). During this process, various model transformations can also be applied to translate the CPS design specification model into appropriate models that can be used as input for corresponding analysis tools (simulation or formal verification) associated with each of the candidate runtime computing platform technologies. Some specialized examples of these runtime computing platforms are Lustre [12], Esterel [4], Signal [20], and Giotto [14] with their own formal computing semantics. More traditional RTOS-based computing platforms can be captured and analyzed through UML (MARTE Profile) or AADL-based models and analysis tools [8, 30].

4 Requirements for Standardized CPS Design Specification Language

Following are some of the major requirements that a CPS design specification language (CPS-DSL) must meet:

4.1 Physical Plant Parameter Specification

A CPS-DSL must clearly identify the physical plant parameters that are sensed or actuated upon by the feedback controller.

4.2 Networked Controller Specification

An appropriate CPS-DSL must also describe the various elements of a networked controller design. These elements include topology of sensors, actuators, and control nodes, local control law for each control node, and information exchanged between different control nodes.

4.3 Specification of Controller Adaptation Strategies

For the emerging wide-area CPS application domains, such as smart grid, the performance of communication subsystem cannot be guaranteed. Therefore, CPS-DSL must also define the timing constraints on the information exchange among different control nodes and the control adaptation strategies in case of violation of these timing constraints.

4.4 Interface Between Control Systems Engineer and Real-Time Computer Systems Engineer

A CPS design specification captures the output of platform-imperfection-aware feedback controller design process, and it also serves as input to the process of developing a functionally equivalent embedded implementation of the feedback controller design. Therefore, the CPS-DSL should be designed in such a way that it can serve as an effective communication interface between control systems engineer and real-time computer systems engineer.

4.5 Formal Semantics

A CPS design specification language must support formal semantics. The existence of formal semantics of a CPS design specification language (CPS-DSL) opens up the possibility to prove formal equivalence properties between a CPS-DSL-based CPS design specification and the corresponding CPS deployment on a computing platform.

5 A Proposed CPS Design Specification Language: Overview

This section presents the summary of a proposed CPS-DSL that can meet the requirements identified in Sect. 3.4. Various aspects (such as concrete syntax, abstract syntax, and semantics) of the definition of proposed CPS-DSL are described in detail in Sects. 3.6–3.8.

The individual language elements of the proposed CPS-DSL can be divided into three categories: physical system elements, cyber system elements, and cyber-physical interface elements. Table 3.1 provides a list of the language elements in each of the abovementioned three categories.

Table 3.1 Language elements of the proposed CPS-DSL
Full size table

5.1 Physical System Elements

CompoundPhysicalPlant and PhysicalSystemParameter elements belong to the category of physical system elements. CompoundPhysicalPlant element is used to represent the physical plant of a CPS. A CompoundPhysicalPlant element contains a set of PhysicalSystemParameter elements. PhysicalSystemParameter elements of the proposed CPS-DSL are used to identify the parameters of a physical plant that are to be sensed and actuated upon by the cyber subsystem of a CPS.

5.2 Cyber-Physical Interface Elements

Sensor and Actuator elements make up the category of cyber-physical interface elements. Cyber-physical interface of a CPS design is captured by a set of Sensor and Actuator elements. Each Sensor and Actuator element is associated with a corresponding PhysicalSystemParameter element.

5.3 Cyber System Elements

ComputingNode, CommunicationNetwork, ControlApp, SensorPort, ActuatorPort, InputMsgPort, OutputMsgPort, Mode, ModeSwitchLogic, ControllerFunction, ControllerFunctionMemory, PeriodicControllerInput, and PeriodicControllerOutput make up the category of cyber system elements. Cyber aspects of a CPS design include the topology of computing nodes, the controller application executing on each computing node, and the message exchange among computing nodes. The topology of controller computing nodes is captured by connecting a set of ComputingNode elements to a CommunicationNetwork element. Each ComputingNode element includes a ControlApp element and a set of SensorPort, ActuatorPort, InputMsgPort, and OutputMsgPort elements. SensorPort, ActuatorPort, and ControlApp elements combine to capture the local control application executing on a computing node.

InputMsgPort and OutputMsgPort elements of proposed CPS-DSL are intended to capture the message exchange among computing nodes of a CPS. However, in a generic cyber-physical system, perfect behavior of communication subsystem cannot be guaranteed. As a result, a CPS design must specify the timing constraints on information exchange among computing nodes and different modes of operation for local feedback control law that are used in case of violation of these timing constraints. In the proposed CPS-DSL, InputMsgPort and OutputMsgPort elements capture the timing constraints on the information exchange among computing node.

Each ControlApp element includes a ModeSwitchLogic element and a set of Mode elements to capture the different modes of operation of feedback control law for handling QoS fault scenarios. Each Mode element specifies the control action taken by the feedback controller in that mode of operation through a set of ControllerFunction, PeriodicControllerInput, and PeriodicControllerOutput elements.

6 Proposed CPS Design Specification Language: Concrete Syntax

Since Simulink [27] (combined with auxiliary Stateflow [28] and Simscape [26] blocks) has become a de facto standard in the domain of embedded control systems, concrete syntax of the proposed CPS-DSL has been implemented as an extension to standard blocks available in Simulink. In particular, a new Simulink library [36] has been developed that provides a Simulink block for each element of the proposed CPS-DSL, described in Sect. 3.5. Moreover, Simulink’s mask interface capability has been used to provide each new Simulink block with a custom look, and a dialog box for entering element-specific parameters, such as the timing constraints associated with an InputMsgPort element.

Figure 3.4 shows a Simulink model that specifies a CPS design using the Simulink-based concrete syntax of the proposed CPS-DSL. Figure 3.5 shows the internal details of a ComputingNode block, which contains a ControlApp block and a set of SensorPort, ActuatorPort, InputMsgPort, and OutputMsgPort blocks. Figure 3.6 shows the internal details of ControlApp block, which consists of a set of Mode blocks and a ModeSwitchLogic block. Figure 3.7 shows the internal details of Mode block, which contains a set of ControllerFunction, PeriodicControllerInput, and PeriodicControllerOutput blocks. Figure 3.8 shows the internal details of ControllerFuncton block, which contains a description of feedback control law using standard Simulink computation blocks.

Fig. 3.4
figure 4

A CPS design, specified as Simulink model with the proposed CPS-DSL

Full size image
Fig. 3.5
figure 5

Internal details of ComputingNode block, named CompNodeB, in Fig. 3.4

Full size image
Fig. 3.6
figure 6

Internal details of ControlApp block, named DemandResponseB, in Fig. 3.5

Full size image
Fig. 3.7
figure 7

Internal details of Mode block, named NormalMode, in Fig. 3.6

Full size image
Fig. 3.8
figure 8

Internal details of ControllerFunction block, named NormalControllerFunction, in Fig. 3.7

Full size image

7 Proposed CPS Design Specification Language: Abstract Syntax

Abstract syntax of the proposed CPS-DSL has been implemented as an Ecore-based meta-model [11], combined with a set of object constraint language (OCL)-based constraints. Ecore meta-modeling language was originally developed as a part of Eclipse Modeling Framework (EMF) project [33], while OCL was developed as a part of the UML standardization effort [38]. Figure 3.9 shows a simplified version of the Ecore-based meta-model for the proposed CPS-DSL. Table 3.2 provides some examples of OCL-based constraints that are part of the abstract syntax definition of the proposed CPS-DSL.

Fig. 3.9
figure 9

Ecore-based meta-model of proposed CPS-DSL

Full size image
Table 3.2 Abstract syntax definition of proposed CPS-DSL: examples of OCL-based constraints
Full size table

8 Proposed CPS Design Specification Language: Semantics

According to the semantics of the proposed CPS-DSL, at a given time, only one Mode element inside a ControlApp is active. ModeSwitchLogic element is evaluated at specific time instants, defined by the following two properties of the currently-active mode: mode period and switch frequency from active mode to mode j (the number of equally-distant time instants in a single mode period at which the mode switch condition from active mode to mode j is evaluated).

As long as a certain Mode element is active, its constituent PeriodicControllerInput and PeriodicControllerOutput elements periodically sample the values at their inputs and store them at the output until the next sampling time instant. A ControllerFunction element contains the specification of feedback control law computation and is always sandwiched between a pair of PeriodicControllerInput and PeriodicControllerOutput elements with same sampling period T and synchronized sampling instants. The sampling period T, associated with a ControllerFunction, is defined in terms of the following two properties: mode period and controller function frequency (the number of equally-distant time instants in a single mode period at which the controller function is evaluated). Moreover, a ControllerFunction element takes time Δt to transfer any change in its input to its output where 0 < Δt < T. A ControllerFunction element may also contain one or more ControllerFunctionMemory elements.

By design, the proposed CPS-DSL leaves its exact semantics dependent on the language used to define the control law computation inside a ControllerFunction element. This capability makes the proposed CPS-DSL more flexible. However, for the rest of this chapter, it will be assumed that Simulink computation blocks are used to define the control law computation inside a ControllerFunction element.

As outlined in Sect. 3.4.5, semantics of the proposed CPS-DSL should ideally be formally defined. In their seminal work on the application of linear temporal logic (LTL) for formal verification of reactive computer systems, Manna and Pnueli [23, 24] presented a generic model of a reactive computer system in the form of a transition system. (This transition system will be referred to as Manna–Pnueli Transition System in the rest of this chapter.) They showed that various existing programming languages and specification formalisms for reactive computer systems can be mapped into this generic model. They also observed that their generic model of reactive computer systems is designed to be capable of capturing any programming language or specification formalism for reactive computer system, proposed in the future. In Sect. 3.8.1, we summarize the abovementioned Manna–Pnueli Transition System. In Sect. 3.8.2, we describe the semantics of the proposed CPS-DSL in terms of Manna–Pnueli Transition System.

8.1 Manna-Pnueli Transition System

Manna–Pnueli Transition System < Π, Σ, T, Θ > , intended to serve as a generic model for reactive computer systems, consists of the following components:

  • Π = {u 1, …, u n}—A finite set of state variables.

    Each state variable is a typed variable, whose type indicates the domain from which the values of that variable can be assigned. Some of these state variables are data variables, which represent the data elements that are declared and manipulated by the program of a reactive computer system. Other state variables are control variables, which keep track of the progress in the execution of a reactive computer system’s program.

  • Σ—A set of states.

    Each state s in Σ is an interpretation of Π. An interpretation of a set of typed variables is a mapping that assigns to each variable a value in its domain. Therefore, each state s in Σ assigns each variable u in Π a value over its domain, which is denoted by s[u].

  • T—A finite set of transitions.

    Each transition τ in T represents a state-changing action of the reactive computer system and is defined as a function τ : Σ → 2Σ that maps a state s in Σ into the (possibly empty) set of states τ(s) that can be obtained by applying action τ to state s. Each state s′ in τ(s) is defined to be a τ-successor of s. A transition τ is said to be enabled on s if τ(s) ≠ ϕ, that is, s has a τ-successor. It is required that one of the transitions, τ I, called the idling transition, is an identity transition, i.e., τ I(s) = {s} for every state s. The transitions other than the idling transition are called diligent transitions.

  • Θ—An initial condition.

    Initial condition is an assertion (Boolean expression) that characterizes the states at which the execution of reactive computer system’s program can begin. A state s satisfying Θ is called an initial state.

Each transition τ can be characterized by an assertion ρ τ(Π, Π ′), called the transition relation, of the following form:

$$\displaystyle \begin{aligned}\rho_{\tau}(\varPi, \varPi^{\prime}): C_{\tau}(\varPi) \wedge (y_{1}^{\prime} = e_{1}) \wedge \dots \wedge (y_{k}^{\prime} = e_{k})\end{aligned}$$

This transition relation consists of the following elements:

  • An enabling condition C τ(Π), which is an assertion, describing the condition under which the state s may have a τ-successor.

  • A conjunction of modification statements

    $$\displaystyle \begin{aligned}(y_{1}^{\prime} = e_{1}) \wedge \dots \wedge (y_{k}^{\prime} = e_{k}),\end{aligned}$$

    which relate the values of the state variables in a state s to their values in a successor state s′ obtained by applying τ to s. Each modification statement y i = e i describes the value of a state variable in state s′ as an expression consisting of the state variable values in state s.

As an example, for a transition system with Π = {x, y, z},

$$\displaystyle \begin{aligned}\rho_{\tau}: (x > 0) \wedge (z' = x - y)\end{aligned}$$

describes a transition τ that is enabled only when x is positive and this transition assigns the value of z in state s′ equal to the value of x − y in state s.

8.1.1 Computations

A computation of Manna–Pnueli Transition System < Π, Σ, T, Θ >  is defined to be an infinite sequence of states

$$\displaystyle \begin{aligned}\sigma: s_{0}, s_{1}, s_{2}, \dots\end{aligned}$$

satisfying the following requirements:

  • Initiation: The first state s 0 is an initial state, i.e., it satisfies the initial condition of the transition system.

  • Consecution: For each pair of consecutive states s i, s i+1 in σ, s i+1 ∈ τ(s i) for some transition τ in T. The pair s i, s i+1 is referred to as a τ-step. It is possible for a given pair to be both a τ-step and a τ′-step for τ ≠ τ′.

  • Diligence: Either the sequence contains infinitely many diligent steps or it contains a terminal state (defined as a state to which only idling transitions can be applied). This requirement excludes the sequences in which, even though some diligent transition is enabled, only idling steps are taken beyond some point. A computation that contains a terminal state is called a terminating computation.

Indices i of states in a computation σ are referred to as positions. If τ(s i) ≠ ϕ (τ enabled on s i), it is said that the transition τ is enabled at position i of computation σ. If s i+1 ∈ τ(s i), it is said that transition τ is taken at position i. Several transitions may be enabled at a single position. Moreover, one or more transitions may be considered to be taken at the same position. A state s is called reachable in a transition system if it appears in some computation of the system.

8.2 Manna–Pnueli Transition System-Based Representation of CPS-DSL

According to the proposed CPS design specification language (CPS-DSL), a ComputingNode block contains a ConrolApp block and a set of SensorPort, ActuatorPort, InputMsgPort, and OutputMsgPort blocks. Furthermore, the ControlApp block contains a set of Mode blocks and a ModeSwitchLogic block. Based on these constituent blocks, a ComputingNode block, CompNode1, of CPS-DSL can be represented as the Manna–Pnueli Transition System, \(P_{CompNode}<\varPi _{P_{CompNode}}\), \(\varSigma _{P_{CompNode}}\), \(T_{P_{CompNode}}\), \(\varTheta _{P_{CompNode}}>\), outlined below, where:

  • \(\varPi _{P_{CompNode}}\)—A finite set of state variables.

    $$\displaystyle \begin{aligned} \varPi_{P_{CompNode1}} &= \{t, t^{switch}_{CompNode1}, mode_{CompNode1}, t^{next}_{CompNode1},\\ &\quad sensePort^{1}_{CompNode1}, sensePort^{2}_{CompNode1},\\&\qquad \dots, sensePort^{p}_{CompNode1},\\ &\quad inMsgPort^{1}_{CompNode1}, inMsgPort^{2}_{CompNode1},\\&\qquad \dots,inMsgPort^{r}_{CompNode1},\\ &\quad actPort^{1}_{CompNode1}, actPort^{2}_{CompNode1}, \dots,actPort^{q}_{CompNode1},\\ &\quad outMsgPort^{1}_{CompNode1}, outMsgPort^{2}_{CompNode1}, \\ &\qquad \dots, outMsgPort^{l}_{CompNode1},\\ &\quad periodicControllerIn^{1}_{CompNode1},\\&\quad periodicControllerIn^{2}_{CompNode1},\\&\qquad \dots, periodicControllerIn^{a}_{CompNode1},\\ &\quad periodicControllerOut^{1}_{CompNode1},\\&\quad periodicControllerOut^{2}_{CompNode1},\\&\qquad \dots, periodicControllerOut^{b}_{CompNode1},\\ &\quad controllerFunctionMemory^{1}_{CompNode1},\\ &\quad controllerFunctionMemory^{2}_{CompNode1},\\ &\qquad \dots, controllerFunctionMemory^{c}_{CompNode1}\} \end{aligned} $$

    where

    t :

    = time,

    \(t^{switch}_{CompNode1}\) :

    = latest mode switch time of ControlApp block, associated with ComputingNode block CompNode1,

    mode CompNode1 :

    = current mode of ControlApp block, associated with ComputingNode block CompNode1,

    \(t^{next}_{CompNode1}\) :

    = next relevant time instant (actuator update, output message update) during the current mode of operation of ControlApp block, associated with ComputingNode block CompNode1,

    \(sensePort^{i}_{CompNode1}\) :

    = A SensorPort block, contained in the ComputingNode block CompNode1,

    \(inMsgPort^{i}_{CompNode1}\) :

    = An InputMsgPort block, contained in the ComputingNode block CompNode1,

    \(actPort^{i}_{CompNode1}\) :

    = An ActuatorPort block, contained in the ComputingNode block CompNode1,,

    \(outMsgPort^{i}_{CompNode1}\) :

    = An OutputMsgPort block, contained in the ComputingNode block CompNode1,

    \(peridoicControllerIn^{i}_{CompNode1}\) :

    = A PeriodicControllerInput block that is contained in a mode of the ControlApp block, associated with ComputingNode block CompNode1,

    \(peridoicControllerOut^{i}_{CompNode1}\) :

    = A PeriodicControllerOutput block that is contained in a mode of the ControlApp block, associated with ComputingNode block CompNode1,

    \(controllerFunctionMemory^{i}_{CompNode1}\) :

    = A ControllerFunctionMemory block that is contained in the ControllerFuction block of a mode of the ControlApp block, associated with ComputingNode block CompNode1,

  • \(\varSigma _{P_{CompNode}}\)—A set of states.

    Each state s in Σ is an interpretation of Π. An interpretation of a set of typed variables is a mapping that assigns to each variable a value in its domain. The domain of state variables t, \(t^{switch}_{CompNode1}\), and \(t^{next}_{CompNode1}\) is R ≥0. The domain of state variable mode CompNode1 is Modes CompNode1 = {Set of modes of ControlApp block, contained in the ComputingNode block CompNode1}. Given the following definitions of Π α and D, all the state variables in Π α have the domain D:

    $$\displaystyle \begin{aligned} \varPi_{\alpha} &= \{sensePort^{i}_{CompNode1}, actPort^{i}_{CompNode1}, outMsgPort^{i}_{CompNode1},\\ &\quad periodicControllerIn^{i}_{CompNode1}, periodicControllerOut^{i}_{CompNode1},\\ &\quad controllerFunctionMemory^{i}_{CompNode1}\}\end{aligned} $$
    $$\displaystyle \begin{aligned} \mathbf{D} &= \{x \mid (x\in\mathbf{R}) \\ &\quad \wedge~(x~{\mathrm{can~be~represented~by~type}}~double~{\mathrm{of~computer~system}})\} \end{aligned} $$

    The state variable \(inMsgPort^{i}_{CompNode1}\) has the following domain:

    $$\displaystyle \begin{aligned} \mathbf{P} = \{(x,y) \mid (x\in\mathbf{R}) \wedge (y\in\mathbf{D})\} \end{aligned}$$

  • \(T_{P_{CompNode}}\)—A finite set of transitions.

    $$\displaystyle \begin{aligned} T_{P_{CompNode1}} = \tau_{I} \cup T^{ModeSwitches}_{CompNode1} \cup T^{TimeIncrement}_{CompNode1} \end{aligned}$$

    where

    τ I :

    = Idling Transition

    \(T^{ModeSwitches}_{CompNode1}\) :

    = \(\{ \tau ^{mode_imode_j}_{CompNode1} \mid \exists \) a mode switch from mode i to mode j in the ModeSwitchLogic block of ControlApp block, associated with ComputingNode block CompNode1}

    \(T^{TimeIncrement}_{CompNode1}\) :

    = \(\{\tau ^{mode_1}_{CompNode1}, \tau ^{mode_2}_{CompNode1}, \dots , \tau ^{mode_M}_{CompNode1}\}\)

    As outlined in the summary of Manna–Pnueli Transition System approach, presented in Sect. 3.8.1, each transition τ can be characterized by an enabling condition and a set of modification statements. Based on the abovementioned set of transitions \(T_{P_{CompNode1}}\) of P CompNode1, all the diligent transitions of P CompNode1 can be completely described through the enabling conditions and modification statements of the following generic transitions: \(\tau ^{mode_imode_j}_{CompNode1}\) and \(\tau ^{mode_i}_{CompNode1}\).

    (a) \(\tau ^{mode_imode_j}_{CompNode1}\) : Enabling Condition

    $$\displaystyle \begin{aligned} C_{\tau^{mode_imode_j}_{CompNode1}} &= (mode_{CompNode1} == mode_i)\\ &\quad \wedge ModeSwitchCondition_{CompNode1}(t, mode_i, mode_j)\\ & \quad \wedge ModeSwitchCheckTime_{CompNode1}\\ & \qquad (t, t^{switch}_{CompNode1}, mode_i, mode_j) \end{aligned} $$

    where

    ModeSwitchCondition CompNode1 (t,  mode i ,  mode j ):

    = An assertion that returns true if the mode switch condition associated with mode switch from mode i to mode j in the ModeSwitchLogic block, contained in the ComputingNode block CompNode1, is true at time t.

    \(ModeSwitchCheckTime_{CompNode1}(t, t^{switch}_{CompNode1},mode_i, mode_j)\) :

    = An assertion that returns true if \(t - t^{switch}_{CompNode1} = a\{\frac {Period_{mode_i}}{SwitchFreq_{mode_imode_j}}\}\), for some a ∈ \(\{1, 2, \dots , SwitchFreq_{mode_imode_j}\}\).

    (b) \(\tau ^{mode_imode_j}_{CompNode1}\) : Modification Statements

    1. 1.

      mode CompNode1 ′ = mode j

    2. 2.

      \({t^{switch}_{CompNode1}}^\prime = t\)

    3. 3.

      \({t^{next}_{CompNode1}}^\prime = t + t_{jump}\)

      where

      $$\displaystyle \begin{aligned} t_{jump} &= \min \Big\{t_j \mid (t_j > 0) \wedge (t + t_j = {t^{switch}_{CompNode1}}^\prime\\ &\qquad + a\{\frac{Period_{mode_j}}{ControllerFunctionFreq_{controllerFucntion_d}}\}),\\&\quad {\mathrm{for\, some}}\\&\quad a \in \{1, 2,\dots, ControllerFunctionFreq_{controllerFunction_d}\}\\&\quad {\mathrm{and \, for \, some}}\\&\quad controllerFunction_d \in ControllerFunctions^{mode_j}_{CompNode1} \Big\} \end{aligned} $$
    4. 4.
      $$\displaystyle \begin{aligned} {periodicControllerOuts^{mode_j}_{CompNode1}}^\prime &=ModeSwitchFunction^{mode_imode_j}_{CompNode1}\\&\quad \ (periodicControllerOuts^{mode_i}_{CompNode1}) \end{aligned} $$

      where

      \(ModeSwitchFunction^{mode_imode_j}_{CompNode1}\) :

      = A function that produces the values to which \(periodicControllerOuts^{mode_j}_{CompNode1}\) are initialized after the mode switch from mode i to mode j of ControlApp, associated with CompNode1

    5. 5.
      $$\displaystyle \begin{aligned} {actPorts^{mode_j}_{CompNode1}}^\prime &= ControllerOutsToActs^{mode_j}_{CompNode1}\\&\quad \ ({periodicControllerOuts^{mode_j}_{CompNode1}}^\prime) \end{aligned} $$

      where

      \(ControllerOutsToActs^{mode_j}_{CompNode1}\) :

      = A function that captures the input–output relationship (produced by the combined effect) of all the connections between PeriodicControllerOutput blocks and ActuatorPort blocks in mode j of CompNode1.

    6. 6.
      $$\displaystyle \begin{aligned} {outMsgPorts^{mode_j}_{CompNode1}}^\prime &= ControllerOutsToOutMsgs^{mode_j}_{CompNode1}\\&\quad \ ({periodicControllerOuts^{mode_j}_{CompNode1}}^\prime) \end{aligned} $$

      where

      \(ControllerOutsToOutMsgs^{mode_j}_{CompNode1}\) :

      = A function that captures the input–output relationship (produced by the combined effect) of all the connections between PeriodicControllerOutput blocks and OutputMsgPort blocks in mode j of CompNode1.

    7. 7.
      $$\displaystyle \begin{aligned} &{periodicControllerIns_{controllerFucntion_b}}^\prime\\&\quad =LoadControllerInputs_{controllerFunction_b}^{mode_j} ({sensePorts^{mode_j}_{CompNode1}}^\prime,\\&\qquad {inMsgPorts^{mode_j}_{CompNode1}}^\prime, {periodicControllerOuts^{mode_j}_{CompNode1}}^\prime)\\& {\mathrm{for\quad every\quad }} controllerFunction_b \in ControllerFunctions^{mode_j}_{CompNode1} \end{aligned} $$

      where

      \(LoadControllerInputs_{controllerFunction_b}^{mode_j}\) :

      = A function that captures the input–output relationship (produced by the combined effect) of all the connections between PeriodicControllerInput blocks, associated with ControllerFunction block controllerFunction b in mode j, and SensorPorts, InputMsgPorts, and PeriodicControllerOutput blocks in mode j of CompNode1.

    (c) \(\tau ^{mode_i}_{CompNode1}\) : Enabling Condition

    $$\displaystyle \begin{aligned} C_{\tau^{mode_i}_{CompNode1}} &= (mode_{CompNode1} == mode_i)\\ & \quad \wedge \neg(ModeSwitchCondition_{CompNode1}(t, mode_i, mode_c)\\ & \quad \wedge ModeSwitchCheckTime_{CompNode1}(t, t^{switch}_{CompNode1},mode_i,mode_c))\\ \forall mode_c &\in \{mode_c \mid \exists\ a\ mode\ switch\ from\ modei\ to\ modec\ of\ ControlApp\\&\quad associated\ with\ ComputingNode\ block\ CompNode1\} \end{aligned} $$

    (d) \(\tau ^{mode_i}_{CompNode1}\) : Modification Statements

    1. 1.

      \(t^\prime = t^{next}_{CompNode1}\)

    2. 2.

      \({t^{next}_{CompNode1}}^\prime = t^\prime + t_{jump}\)

      where

      $$\displaystyle \begin{aligned} t_{jump} &= \min \Big\{t_j \mid (t_j > 0) \wedge (t^\prime + t_j = t^{switch}_{CompNode1} \\&\qquad +a\{\frac{Period_{mode_i}}{ControllerFucntionFreq_{controllerFunction_d}}\}) \end{aligned} $$

      • for some a ∈ \(\{1, 2, \dots , ControllerFunctionFreq_{controllerFunction_d}\}\)

      • and

      • for some \(controllerFunction_d \in ControllerFunctions^{mode_i}_{CompNode1}\) }

    3. 3.
      $$\displaystyle \begin{aligned} &({periodicControllerOuts_{controllerFunction_e}}^\prime,\\ &\quad {controllerFunctionMemory_{controllerFunction_e}}^\prime) =\\ &\qquad f^{controllerFunction_e}(periodicControllerIns_{controllerFunction_e}, \\ &\qquad controllerFuctionMemory_{controllerFunction_e})\\ &\forall controllerFunction_e \in \Big\{ controllerFunction_e \mid\\ &\quad (controllerFunction_e \in ControllerFunctions^{mode_i}_{CompNode1})\\ &\quad \wedge (t^\prime = t^{switch}_{CompNode1} + a\{\frac{Period_{mode_i}}{ControllerFunctionFreq_{controllerFunction_e}}\})\\ &\quad {\mathrm{for~some}}~a~\in~\{1, 2, \dots, ControllerFunctionFreq_{controllerFunction_e}\}\Big\} \end{aligned} $$

      where

      \(f^{controllerFunction_e}\) :

      = The function implemented by the internal components (Simulink blocks) of ControllerFunction block controller Fucntion e.

    4. 4.
      $$\displaystyle \begin{aligned} &{periodicControllerIns_{controllerFunction_f}}^\prime =\\ &\quad LoadControllerInputs_{controllerFunction_f}^{mode_i}({sensePorts^{mode_i}_{CompNode1}}^\prime, \\ &\qquad {inMsgPorts^{mode_i}_{CompNode1}}^\prime,{periodicControllerOuts^{mode_i}_{CompNode1}}^\prime)\\ &\forall controllerFunction_f \in \Big\{ controllerFunction_f \mid\\ &\quad (controllerFunction_f \in ControllerFunctions^{mode_i}_{CompNode1})\\ &\quad \wedge (t^\prime = t^{switch}_{CompNode1} + a\{\frac{Period_{mode_i}}{ControllerFunctionFreq_{controllerFunction_f}}\})\\ &\quad {\mathrm{for~some}}~a~\in \{1, 2, \dots, ControllerFunctionFreq_{controllerFunction_f}\}\Big\} \end{aligned} $$
    5. 5.
      $$\displaystyle \begin{aligned} &{actPorts^{mode_i}_{CompNode1}}^\prime =\\ &ControllerOutsToActs^{mode_i}_{CompNode1}({periodicControllerOuts^{mode_i}_{CompNode1}}^\prime) \end{aligned} $$
    6. 6.
      $$\displaystyle \begin{aligned} &{outMsgPorts^{mode_i}_{CompNode1}}^\prime = \\ &ControllerOutsToOutMsgs^{mode_i}_{CompNode1}\\ &\quad ({periodicControllerOuts^{mode_i}_{CompNode1}}^\prime) \end{aligned} $$

  • \(\varTheta _{P_{CompNode}}\)—An initial condition. Any initial state s of transition system P CompNode must satisfy the following initial conditions:

    • \({-4pt}t = 0\)

    • \({-4pt}t^{switch}_{CompNode1} = 0\)

    • \({-4pt}mode_{CompNode1} = mode_1\)

    • \({-4pt}t^{next}_{CompNode1}{\,=\,}\min \Big \{t_j \mid (t_j > 0) \wedge (t_j{\,=\,}a\{\frac {Period_{mode_1}}{ControllerFunctionFreq_{controllerFunction_d}}\})\) for some a ∈ \(\{1, 2, \dots ,ControllerFunctionFreq_{controllerFunction_d}\}\) and for some \(controllerFunction_d \in ControllerFunctions^{mode_1}_{CompNode1}\) }

9 Conclusion

Taking inspiration from the hourglass-shaped architecture of the Internet, this chapter has proposed an hourglass-shaped architecture for model-based development of networked cyber-physical systems. Similar to the central role played by TCP/IP protocols in the Internet architecture, the proposed architecture for model-based networked CPS development is centered on the notion of a standardized CPS design specification language.

The proposed hourglass-shaped architecture can enable effective coordination between control systems engineers and embedded systems engineers during a model-based CPS development process, while still acknowledging the differences between the domain-specific skillset that control systems engineer and embedded system engineer typically possess. The chapter has also proposed a version of the abovementioned CPS design specification language and discussed its various aspects such as concrete syntax, abstract syntax, and semantics.