A Component-Based Approach to Hybrid Systems Safety Verification

Abstract

We study a component-based approach to simplify the challenges of verifying large-scale hybrid systems. Component-based modeling can be used to split large models into partial models to reduce modeling complexity. Yet, verification results also need to transfer from components to composites. In this paper, we propose a component-based hybrid system verification approach that combines the advantages of component-based modeling (e.g., reduced model complexity) with the advantages of formal verification (e.g., guaranteed contract compliance). Our strategy is to decompose the system into components, verify their local safety individually and compose them to form an overall system that provably satisfies a global contract, without proving the whole system. We introduce the necessary formalism to define the structure and behavior of components and a technique how to compose components such that safety properties provably emerge from component safety.

Work partly funded by BMVIT grant FFG BRIDGE 838526, OeAD Marietta Blau grant ICM-2014-08600, FWF P28187-N31, and ERC PIOF-GA-2012-328378.

1 Introduction

The hybrid dynamics of computation and physics in safety-critical cyber-physical systems (CPS), such as driver assistance systems, self-driving cars, autonomous robots, and airplanes, are almost impossible to get right without proper formal analysis. To enable this analysis, CPS are modeled using so called hybrid system models. At larger scales of realistic hybrid system models, formal verification of monolithic models becomes quite challenging. Therefore, component-based modeling approaches split large models into partial models, i.e., co-existing or interacting components (e.g., multiple airplanes in a collision avoidance maneuver). Even though this can lead to component-based models with improved structure and reduced modeling complexity, component verification results do not always transfer to composite systems without appropriate care.

This paper generalizes our previous work [18], which was limited to traffic flow models (i.e., port conditions limited to maximum values, contracts limited to load restrictions, components limited to interfaces and predefined behavior), to a more generic approach to make hybrid system theorem proving modular on a component level. The approach exploits component contracts to compose verified components and their safety proofs to a verified CPS. Differential dynamic logic $\textsf {d}\!\mathcal {L}$ [21, 22], the hybrid systems specification and verification logic we are working with, is already compositional for each of its operators and, thus, a helpful basis for our approach. Reasoning in $\textsf {d}\!\mathcal {L}$ splits models along the $\textsf {d}\!\mathcal {L}$ operators into smaller pieces. In this paper, we build compositionality for a notion of components and interfaces on top of $\textsf {d}\!\mathcal {L}$. We focus on modeling a system in terms of components that each capture only a part of the system’s behavior (as opposed to monolithic models) and a way to compose components by connecting their interfaces (as opposed to basic program composition with $\textsf {d}\!\mathcal {L}$ operators). Component-based hybrid systems verification is challenging because both local component behavior (e.g., decisions and motion of a robot) and inherently global phenomena (e.g., time) co-occur, because components can interact virtually (e.g., robots communicate) and physically (e.g., a robot manipulates an object), and because their interaction is subject to communication delays, measurement uncertainty, and actuation disturbance. Typically, our components are open systems [11], which are described and verified in isolation from other components, separated by interfaces with assumptions about the environment that provide guarantees about the behavior of components. If needed, they can be turned into a closed system [11] by including a model of a specific environment.

This paper focuses on (i) lossless and instantaneous interaction between components (allows uncertainty and delay in dedicated “ether” components, e.g., sense the speed of a car precisely without measurement error), (ii) components without physical entanglement (allows separated continuous dynamics, e.g., robots drive on their own, but do not push each other), and (iii) components without synchronized communication (parallel composition of continuous dynamics, simplification to any sequential interleaving for discrete dynamics, e.g., robots can sense their environment, but not negotiate with each other).

With this focus in mind, we define the structure and behavior of a notion of components and a technique how to compose components such that safety properties about the whole system emerge from component safety proofs (e.g., robots will not collide when staying in disjoint spatial regions). We illustrate our approach with a vehicle cruise control case study.

2 Preliminaries: Differential Dynamic Logic

For specifying and verifying correctness statements about hybrid systems, we use differential dynamic logic ($\textsf {d}\!\mathcal {L}$) [21, 22], which supports hybrid programs as a program notation for hybrid systems. $\textsf {d}\!\mathcal {L}$ models can be verified using KeYmaera  X [8], which is open source and has been applied for verification of several case studies.¹ The syntax of hybrid programs is generated by the following EBNF grammar:

$$ \begin{aligned} \alpha :\,\!:= \alpha ;\beta \mid {\alpha }\cup {\beta } \mid {\alpha }^{*} \mid x\mathrel {{:}{=}}\theta \mid x\mathrel {{:}{=}}* \mid \{x^{\prime }_1=\theta _1,\ldots ,x^{\prime }_n=\theta _n ~ \& ~ H\} \mid ~?\phi . \end{aligned}$$

The sequential composition $\alpha ;\beta$ expresses that $\beta$ starts after $\alpha$ finishes. The non-deterministic choice ${\alpha }\cup {\beta }$ follows either $\alpha$ or $\beta$. The non-deterministic repetition operator ${\alpha }^{*}$ repeats $\alpha$ zero or more times. Discrete assignment $x\mathrel {{:}{=}}\theta$ instantaneously assigns the value of the term $\theta$ to the variable x, while $x\mathrel {{:}{=}}*$ assigns an arbitrary value to x. $\{x^{\prime }=\theta ~ \& ~ H\}$ describes a continuous evolution of x ($x^{\prime }$ denotes derivation with respect to time) within the evolution domain $H$. The test $?\phi$ checks that a condition expressed by $\phi$ holds, and aborts if it does not. A typical pattern $x\mathrel {{:}{=}}*; ?a \le x \le b$, which involves assignment and tests, is to limit the assignment of arbitrary values to known bounds.

To specify safety properties about hybrid programs, $\textsf {d}\!\mathcal {L}$ provides a modal operator $[\alpha ]$. When $\phi$ is a $\textsf {d}\!\mathcal {L}$ formula describing a state and $\alpha$ is a hybrid program, then the $\textsf {d}\!\mathcal {L}$ formula $[\alpha ]{\phi }$ expresses that all states reachable by $\alpha$ satisfy $\phi$. The set of $\textsf {d}\!\mathcal {L}$ formulas relevant for this paper is generated by the following EBNF grammar (where ${\sim }\in \{<,\le ,=,\ge ,>\}$ and $\theta _1,\theta _2$ are arithmetic expressions in $+,-,\cdot ,/$ over the reals):

Notation: Variables. In $\textsf {d}\!\mathcal {L}$ (and thus throughout the paper) all variables are real-valued. We use $V$ to denote a set of variables. $FV(.)$ is used as an operator on terms, formulas and hybrid programs returning only their free variables, whereas $BV(.)$ is an operator returning only their bound variables.² Similarly, $V(.)=FV(.)\cup BV(.)$ returns all variables (free as well as bound).

Notation: Indices. Throughout this paper, subscript indices represent enumerations (e.g., $x_i$). Superscript indices are used to further specify the kinds of items described by the respective variables (e.g., $v^{out}$ represents an output variable). If needed, a double (super- and subscript) one-letter index is used for double numeration (e.g., $x_i^j$ represents element $j$ of the vector $x_i$).

3 Modeling and Verification Steps

In this section we present the modeling and verification steps in our component-based verification approach (cf. Fig. 1). To illustrate the steps, we will use an example of a vehicle cruise control system, which consists of an actuator component adapting the vehicle speed according to a target speed chosen by a cruise control component. The vehicle moves continuously, while the control behavior is described by a discrete control part (e.g., choose velocity and acceleration). The goal is to keep the actual velocity in some range $\left[ 0,V\right]$, where $V$ denotes a maximum velocity. Note that we model components fully symbolically, which means that each component represents actually a family of concrete components.

Fig. 1.

Steps for component-based modeling and verification

The approach consists of the following steps:

• (1) identify global contract: Before decomposing the system, it is important to learn what properties the system as a whole should fulfill (e.g., supported by domain experts). The global contract specifies the initial state of the whole system ($\varPhi$, e.g., initially the velocity is 0) as well as its overall safety property ($\varPsi$, e.g., the velocity will stay in the desired range).

• (2) model components and interfaces: Find recurring parts or natural splitting points for implementations (e.g., we split our cruise control system in a cruise controller and an actuator). The number of different components should be kept small, so that the verification effort remains low; still, there have to be sufficiently many components that can be instantiated to assemble the system. Modeling components and their interfaces is a manual effort (e.g., by modeling experts). A component has a behavior, while its interface defines public input ports and output ports, see Definitions 2 and 3 later.

• (3) identify contracts: For each component and its interface, we identify initial states (e.g., initial target velocity is 0), a safety property (e.g., actual velocity does not exceed $V$), as well as an output contract (e.g., target velocity is always in the desired range), see Definition 4 later. These properties have to be chosen such that the global contract follows by refinement or dominance [4]: and .

• (4) verify contract compliance: Verify that components satisfy their contracts formally, in our case (hybrid programs and $\textsf {d}\!\mathcal {L}$), with KeYmaera  X.

• (5) compose and check compatibility: Construct the system by connecting component ports to compose verified components in parallel, see Definition 5 later. Any component can be instantiated multiple times in the whole system (e.g., instantiate maximum velocity parameters of a cruise control with actual values; connect the controller with the actuator). In order to transfer proofs about components to a global system proof, the compatibility of the components must be checked (see Theorem 1 in Sect. 4.2, which is proved under these compatibility assumptions). Intuitively, the compatibility check ensures that the values provided for symbolic parameters of an output port of one component instance are compatible with the values required on a connected input port of the next instance, see Definition 6 later (e.g., the controller cannot demand target speeds outside the target range).

The main result of this process is that the component safety proofs—done for compatible components in isolation—transfer to an arbitrarily large system built by instantiating these components (cf. Theorem 1).

4 Component-Based Modeling

In this section we introduce essential modeling idioms and definitions for the presented steps. Section 4.1 introduces components (cf. step (2)) and their contracts (cf. step (3)). Similarly, Bauer et al. [3] show how a contract framework can be built generically. Section 4.2 introduces composition (cf. step (5)) and ensures that the local properties transfer to the overall system.

4.1 Components and Contracts

Components can observe a shared global state, and modify their internal state.

Definition 1

(Global Variables). The global variables are a set of variables shared by all components. It contains the variable $t$, which represents the system time, is initially set to $0$, and increases linearly with rate $1$. None of the global variables can ever be bound in any part of any component.

In the following paragraphs, we define components, which have a behavior (e.g., how a cruise controller chooses a target velocity), and interfaces, which consist of input ports (e.g., the current velocity received by cruise control) and output ports (e.g., the new target velocity as provided by cruise control). We define the behavior of a component in the canonical order of a control part followed by a plant, which enables the definition of a structured composition operation for components and interfaces.

Definition 2

(Component). A component $C$ is defined as a tuple

$$\begin{aligned} C=\left( \mathrm{ctrl},\mathrm{plant}\right) ,~{where} \end{aligned}$$

• $ctrl$ is the discrete control part of a hybrid program (HP) and does not contain continuous parts (i.e., differential equations), and

• $plant$ is the continuous part of the form $\left\{ x'_1=\theta _1,...,x'_n=\theta _n \& H\right\}$ for $n\in \mathbb {N}$ i.e., an ordinary differential equation with evolution domain constraint $H$.

The interface of a component consists of input and output ports, which can have contracts (i.e., and , e.g., value range for the target velocity).

Definition 3

(Interface). An interface $I$ is defined as a tuple

• is a set of input variables, is a set of output variables,

• specifies an input predicate ($\mathcal {P}$ represents the set of all logical formulas) representing input requirements and assumptions, exactly one per input variable (i.e., input port), accordingly for ,

• , i.e., no input predicate can mention other input variables, which lets us reshuffle port ordering.

An interface $I$ is called admissible for a component $C$, if , i.e., none of the input variables are bound in $ctrl$ or $plant$.

Fig. 2.

Actuator component/interface example $(C_\text {ac },I_\text {ac })$

Consider our running example of the vehicle cruise control, where the actuator component chooses the acceleration according to a target velocity (cf. Fig. 2). As illustrated in Fig. 2a, the component has a single input port to receive a target velocity and a single output port to provide the current velocity.

Figure 2b describes this component and interface formally: The actuator receives a target speed between 0 and $V$ on its single input port $v^{\textit{tr}}_\text {ac }$, cf. (3). It is a time-triggered controller with sampling period $\varepsilon$. The controller chooses the acceleration of the vehicle such that it will not exceed the target velocity until the next run and stores the current system time, cf. (1). The plant adapts the velocity accordingly and runs for at most $\varepsilon$ time to enforce the sampling period, cf. (2). The single output port yields the resulting actual velocity, which still has to be in range between 0 and $V$, cf. (4).

Definition 4

(Contract). Let $C$ be a component, $I$ be an admissible interface for $C$, and $\phi$ be a formula over the component’s variables $\text {V }$, which determines the component’s initial state. Let be a predicate over the component’s variables $\text {V }$, i.e., a property describing the desirable target system state (i.e., a safety property). We define , where is the conjunction of all output guarantees. The contract of a component $C$ with its interface $I$ is defined as

with input

As the input predicates are not allowed to mention other inputs, the order of inputs in $in$ is irrelevant. We call a component with an admissible interface that provably satisfies its contract to be contract compliant. This means, if started in a state satisfying $\phi$, the component only reaches states that satisfy safety and all output guarantees when all inputs satisfy .

In our running example of Fig. 2, the actuator component has an output guarantee (i.e., the speed must always be in range), and when starting from the initial conditions $\phi \equiv (v_\text {ac }=0 \wedge \varepsilon> 0 \wedge V>0)$ (i.e., vehicle initially stopped) it can provably guarantee safety³ .

4.2 Composition of Components

Now that we have defined the structure and behavior of single components and their interfaces, we specify how to compose a number of those components by defining a syntactic composition operator for components. Differential dynamic logic follows the common assumption in hybrid systems that discrete actions do not consume time, i.e., multiple discrete actions of a program can happen instantaneously at the same real point in time. Time only passes during continuous evolution measured through ${t}^{\prime }$ in $plant$. Hence, if we disallow direct interaction between the controllers of components,⁴ we can compose the discrete $ctrl$ of multiple components in parallel by executing them sequentially in any order, while keeping their plants truly parallel through $\left\{ {x}^{\prime }_1=\theta _1,\ldots ,{x}^{\prime }_n=\theta _n~ \& ~H\right\}$. Interaction between components is then possible by observing plant output.

Such interaction, which exchanges information between components, will be defined by connecting ports when composing components through their interfaces. The port connections are represented by a mapping function $\mathcal {X}$, which assigns an output port to an input port for some number of input ports. In this paper, we focus on instantaneous lossless interaction, where the input variable $v$ instantaneously takes on the value of the output port it is connected to, cf. $v\mathrel {{:}{=}}\mathcal {X}(v)$ in Definition 5. Other interaction patterns can be modeled by adapting Definition 5. For example, measurement with sensor uncertainty $\varDelta$ is $v\mathrel {{:}{=}}*;~?\left( \mathcal {X}(v)-\varDelta \le v \le \mathcal {X}(v)+\varDelta \right)$, which yields a modified compatibility check.

As we do not require all ports to be connected, the mapping function is a partial function. Ports which are not connected become ports of the composite, while ports which are connected become internal variables.

Definition 5

(Parallel Composition). Let $C_i$ denote one of $n$ components

$$ C_i=\left( ctrl _i,plant _i\right) ~\text {for}~i\in \{1,...,n\} $$

with their corresponding admissible interfaces

where for $i \ne j$, i.e., only variables in are shared between components, and let

be a partial (i.e., not every input must be mapped), injective (i.e., every output is only mapped to one input) function, connecting inputs to outputs. We define $\mathcal {I}^{\mathcal {X}}$ as the domain of $\mathcal {X}$ (i.e., all variables such that $\mathcal {X}(x)$ is defined) and $\mathcal {O}^{\mathcal {X}}$ as the the image of $\mathcal {X}$ (i.e., all variables such that $y=\mathcal {X}(x)$ holds for some ).

is defined as the composite of $n$ components and their interfaces (with respect to $\mathcal {X}$), where

• the sensing for non-connected inputs remains unchanged

  

• the order in which the control parts (and the respective port mappings) are executed is chosen non-deterministically (considering all the $n!$ possible permutations of $\{1,...,n\}$), so that connected ports become internal behavior of the composite component

  $$\begin{aligned} ctrl \equiv&\left( ports _1;ctrl _1;ports _2;ctrl _2;...;ports _n;ctrl _n\right) \cup \\&\left( ports _2;ctrl _2;ports _1;ctrl _1;...;ports _n;ctrl _n\right) \cup \\&...\\&\left( ports _n;ctrl _n;...;ports _2;ctrl _{2},ports _1;ctrl _1\right) \end{aligned}$$

  with

• continuous parts are executed in parallel, staying inside all evolution domains

  $$ \begin{aligned} plant \equiv \bigl \{ \underbrace{x_{1}^{(1)\prime } = \theta _{1}^{(1)}, \ldots , x_{1}^{(k)\prime } = \theta _{1}^{(k)}}_{\text {component}~C_1}, \ldots , \underbrace{x_{n}^{(1)\prime } = \theta _{n}^{(1)}, \ldots , x_{n}^{(m)\prime } = \theta _{n}^{(m)}}_{\text {component}~C_n} \\ \& ~ H_1 \wedge \ldots \wedge H_n \bigr \}, \end{aligned}$$

• the respective sets of variables are merged, where , , i.e., ports not connected within the composite component remain input and output variables of the resulting interface,

• input port requirements of all interfaces are preserved, except for connected inputs, i.e., becomes , accordingly for :

Fig. 3.

Cruise controller component/interface example $(C_\text {cc },I_\text {cc })$

To demonstrate parallel composition in our running example, we first introduce a cruise controller component (cf. Fig. 3). The cruise control selects a target velocity from the interval, but keeps the difference between the current (received) velocity and the chosen target velocity below $\delta _V$ (cf. (5) and (6)). That way, the acceleration set by the actuator component is bounded by $\delta _V/\varepsilon$ (i.e., the vehicle does not accelerate too fiercely). We connect this cruise controller component to the actuator component (cf. Fig. 2), as illustrated in Fig. 4.

Remark 1

Note that verifying the hybrid program for a composite according to Definition 5 would require a proof of each of the $n!$ branches of $ctrl$ individually, as they all differ slightly. For a large number of components, this entails a huge proof effort. Previous non-component-based case studies (e.g., [13, 16, 17]), therefore, chose only one specific ordering. Our component-based approach verifies all possible orderings at once, because the permutations are all proven correct as part of proving Theorem 1 below in this paper.

Remark 2

This definition of parallel composition uses a conjunction of all evolution domains, which resembles synchronization on the most restrictive component (i.e., as soon as the first and most restrictive condition is no longer fulfilled all plants have to stop and hand over to $ctrl$). A more liberal component might be forced to execute its control part because the evolution domain of a more restrictive component did no longer hold. For example a component increasing a counter on every run of its control is then forced to count although its own evolution domain might have allowed it to postpone control. If this is undesired, a component’s control can be defined as ${ctrl _i}\cup {?\text {true}}$, which would allow the component to skip when forced to run its control part.

Remark 3

We define this composition operation for any number of components, since it is not associative, because the composition of three components results in $3!=6$ possible execution orders, whereas composing two components and adding a third yields only $2!+2!=4$ of the possible 6 execution orders.

Fig. 4.

Cruise control composed of a cruise controller and an actuator by Definition 5. The port connections $\mathcal {X}=\left\{ (v_\text {cc },v_\text {ac }),~(v^{\textit{tr}}_\text {ac },v^{\textit{tr}}_\text {cc }) \right\}$ replace the input port $v^{\textit{tr}}_\text {ac }\mathrel {{:}{=}}*;~?(0 \le v^{\textit{tr}}_\text {ac }\le V)$ with an internal port assignment $v^{\textit{tr}}_\text {ac }\mathrel {{:}{=}}v^{\textit{tr}}_\text {cc }$, provided the compatibility check succeeds, cf. Definition 6, and accordingly for the second port.

Note that Definition 5 replaces the non-deterministic input guarded by a test from Definition 2 with a deterministic assignment that represents instantaneous and lossless interaction between components (i.e., $ports _i$), as illustrated in Fig. 4. Hence, the respective output guarantees and input assumptions must match. For instance, a cruise controller component demanding velocities $0 \le v^{\textit{tr}}_\text {cc }\le 70$ is compatible with an actuator $0 \le v^{\textit{tr}}_\text {ac }\le 100$, but not the other way around.

Definition 6

(Compatible Composite). The composite of $n$ components with interfaces is a compatible composite iff

is valid for all input ports , for all interfaces $I_i$ and where $I_j$ is the interface containing the port that is connected to the input port $v$ of $I_i$. We call the compatibility proof obligation for the interfaces $I_i$ and say the interfaces $I_i$ are compatible (with respect to $\mathcal {X}$) if holds.

In other words, is a compatible composite if all internal port connections are appropriate, i.e., if the guarantee of the output port implies the requirements of the respective input port to which it is connected.

Composite Contracts. Now that we have defined components and interfaces, their contracts, and how to compose them to form larger composites, we prove that the contracts of single components transfer to composites if compatible.

Theorem 1

(Composition Retains Contracts). Let $C_1$ and $C_2$ be components with admissible interfaces $I_1$ and $I_2$ that are contract compliant (i.e., their contracts are valid)

(9)

(10)

and compatible with respect to $\mathcal {X}$ (i.e., compatibility proof obligations are valid)

(11)

(12)

Then, the parallel composition satisfies the contract

(13)

with $in _3$, $ctrl _3$, and $plant _3$ according to Definition 5.

The proof for Theorem 1 can be found in [19], along with a generalization to $n$ components. This central theorem allows us to infer how properties from single components transfer to their composition. As such, it suffices to prove the properties for the components and conclude that a similar property holds for the composite, without explicitly having to verify it. The composite contract states that, considering both pre-conditions hold (i.e., $\phi _1\wedge \phi _2$), all states reached by the parallel execution of the components, both post-conditions hold (i.e., ).

5 Case Study: Vehicle Cruise Control

To illustrate our approach, we used a running example of a simple vehicle cruise control system. The overall system requirement was to keep the velocity $v_\text {ac }$ in a desired range $\left[ 0,V\right]$ at all times, i.e., . We split the system into two components, cf. Fig. 4: an actuator component adapts velocity according to a target $v^{\textit{tr}}_\text {ac }$ provided by a cruise control component as $v^{\textit{tr}}_\text {cc }$. If the cruise control component (Fig. 3) provides a valid target velocity to the actuator (i.e., $0\le v^{\textit{tr}}_\text {ac }\le V$), the actuator component (Fig. 2) ensures to keep the actual velocity in the desired range (i.e., $0\le v_\text {ac }\le V$), thus ensuring the overall system property. Additionally, the actuator provides the current velocity on an output port that is read by the controller, acting as a feedback loop.

Following Definition 4, we derive contracts for each component, which consists of initial conditions $\phi$ (cf. (14) and (15)), safety conditions (cf. (16)) and the port conditions (cf. (4) and (8)). Maximum speed $V>0$ and cycle time $\varepsilon >0$ must be known. Additionally, the controller initializes $v^{\textit{tr}}_\text {cc }=0$ and $\delta _V>0$. The actuator restricts the initial velocity to $0 \le v_\text {ac }\le V$.

(14)

(15)

(16)

The set of global variables follows accordingly (cf. Definition 1): .

After verifying⁵ both contracts and , we want to compose the components to get the overall system, using the mapping function $\mathcal {X}=\left\{ (v_\text {cc },v_\text {ac }),~(v^{\textit{tr}}_\text {ac },v^{\textit{tr}}_\text {cc }) \right\}$. Therefore, we have to check the compatibility proof obligations for both connected ports (cf. Fig. 4). Then the overall system property directly follows from the contract of the actuator component.

Splitting a system into components reduces the model complexity considerably, since a component needs to know neither about the differential equation systems of other components, nor about their control choices. In combined models, we have to analyze all the possible permutations of control choices, while in the component-based approach, by Theorem 1 we can guarantee correctness for all possible sequential orderings, without the proof effort entailed by listing them explicitly.

The benefit of component-based verification becomes even larger when replacing components in a system. For example, we can easily replace the cruise control from Fig. 3 with a more sophisticated controller that takes the target velocity as user input from an additional input port. After verifying the user guided cruise control component, we only have to re-check the compatibility proof obligations. In a monolithic model, in contrast, the whole system including the actuator component must be re-verified.

6 Related Work

CPS Verification. Hybrid automata [2] are popular for modeling CPS, and mainly verified using reachability analysis. Unlike hybrid programs, hybrid automata are not compositional, i.e., for a hybrid automaton it is not sufficient to establish a property about its parts in order to establish a property about the automaton. Techniques such as assume-guarantee reasoning or hybrid I/O automata [14], which are an extension of hybrid automata with input- and output-ports, address this issue. Our approach here shares some of the goals with hybrid I/O automata and also uses I/O ports. But we target compositional reasoning for hybrid programs, where the execution order of statements is relevant, so that our approach defines how parallel composition results in interleaving of hybrid programs. Furthermore, we define compositional modeling for hybrid programs such that theorem proving of the entire system is reduced to proving properties about the components and simple composition checks. Hybrid process algebras (e.g., Hybrid $\chi$ [24], HyPA [20]) are specifically developed as compositional modeling formalisms to describe behavior and interaction of processes using algebraic equations. For verification purposes by simulation or reachability analysis, translations from Hybrid $\chi$ into hybrid automata and timed automata exist, so even though modeling is compositional, verification still falls back to monolithic analysis. We, in contrast, focus on exploiting compositionality in the proof.

Component-Based CPS Modeling. Damm et al. [5] present a component-based design framework for controllers of hybrid systems with a focus on reaction times. The framework checks connections when interconnecting components: alarms propagated by an out-port must be handled by the connected in-ports. We, too, check component compatibility, but for contracts, and we focus on transferring proofs from components to the system level.

Focusing on architectural properties, Ruchkin et al. [26] propose a component-based modeling approach for hybrid-systems. Although they do not transfer verification results from components to composites, their definitions have been an inspiration for our notion of components. Ringert et al. [25] model CPS as Component and Connector (C&C) architectures using automata to describe solely the discrete behavior. They verify the translated models of single components, but do not provide guarantees about verified compositions.

Interface algebras (cf. [1, 9]) are formalisms that separate component-based models into interface models and component models. Similar to our approach, the component model describes what a component does, while the interface model defines how the component can be used. It is often distinguished between interfaces with and without state, where stateful interfaces are usually viewed as concurrent games. Our approach is similar to a stateless interface algebra [1]. Similarly, Bauer et al. [3] show how a contract framework can be built generically. While useful for inspiration, these approaches focus on modeling aspects and do not consider verification.

Verification. Madl et al. [15] model real-time event-driven systems. Their models can be transformed to UPPAAL (cf. [12]) timed automata, restricting the continuous part of their models to time instead of arbitrary physical behavior (e.g., movement). Moreover, their analysis targets the entire composition of timed automata, thus defeating the advantages of components for verification.

A field closely related to component-based verification is assume-guarantee reasoning (AGR, e.g., [7, 10]), which was originally developed as a device to counteract the state explosion problem in model checking by decomposing a verification task into subtasks. In AGR, individual components are analyzed together with assumptions about their context and guarantees about their behavior (i.e., a component’s contract). AGR rules need to exercise care for circularity in the sense that the approaches verify one component in the context of the other and vice-versa, like Frehse et al. [7] (using Hybrid Labeled Transition Systems as abstraction for Hybrid I/O-Automata) and Henzinger et al. [10] (using hierarchical hybrid systems based on hybrid automata). However, existing approaches are often limited to linear dynamics, cannot handle continuity or use corresponding reachability analysis or model checking techniques. In $\textsf {d}\!\mathcal {L}$, in contrast, we can handle non-linear dynamics and focus on theorem proving.

In summary, only few component-based approaches handle generic CPS with both discrete and continuous aspects (e.g., [5, 15, 26]), but those do not yet focus on the impact on formal verification. Related techniques for CPS and hybrid systems verification focus mainly on timed automata, hybrid process algebras, and hybrid automata with linear dynamics or end up in monolithical verification.

7 Conclusion and Future Work

We presented an approach for component-based modeling and verification of CPS that (i) splits a CPS into components, (ii) verifies a contract for each of these components and (iii) composes component instances in a way that transfers the component contracts to a composite contract. Our approach makes hybrid system verification more modular at the scale of components, and combines the advantages of component-based modeling approaches (e.g., well structured models, reduced model complexity, simplified model evolution) with the advantages of formal verification (e.g., guaranteed contract compliance).

Currently, our approach is limited to global properties that are stated relative to the initial system state. Port conditions are only allowed to mention global variables and the port variable itself, which prevents conditions on the change of a port since the last measurement (e.g., how far has a vehicle moved since the beginning vs. how far has it moved since the last measurement). This restriction can be removed with ports that remember their previous value and relate measurements over time. Additionally, we plan to (i) introduce further composition operations (e.g., sensing with measurement errors), (ii) provide further component extensions (e.g., multi-cast ports), and (iii) provide tool support to instantiate and compose components, and to generate their hybrid programs.