figure a

1 Introduction

Many cyber-physical systems (CPSs) are virtually synchronous networks of hy brid components with continuous behaviors combined with sophisticated controllers. They should logically behave as if they were synchronous—in each iteration of the system, all components, in lockstep, read inputs and perform transitions which generate outputs for the next iteration—but have to be realized in a distributed setting, with clock skews and message passing communication. Examples of such CPSs include avionics and automotive systems [34, 42], networked medical devices [5, 30], and other distributed control systems such as the steam-boiler benchmark [1], where the underlying infrastructure often guarantees bounds on clock skews, network delays, and local execution times.

The uptake of automated formal analysis of such CPSs is challenging, since:

  1. 1.

    The combination of large “discrete” state spaces, caused by interleavings due to asynchronous communication, and continuous behaviors, taking into account clock skews, network delays, and sampling/actuation times (based on imprecise clocks) makes direct automatic model checking analysis infeasible.

  2. 2.

    To enable formal analysis to a large user base, the modeling language for such CPSs, with complex control programs, should be well-known for CPS developers, and should be integrated into mature modeling environments.

To confront these challenges, we present in this paper the \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\) modeling language and analysis tool, which address them as follows:

  1. 1.

    To dramatically reduce both the modeling complexity and the state space caused by asynchronous communication, we use the Hybrid PALS equivalence [8], which says that the underlying synchronous design—where all components execute in lockstep, and there is no asynchronous message passing—satisfies the same properties as the asynchronous distributed system.

  2. 2.

    The \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\) modeling language is a subset of the avionics modeling standard AADL [22] and its behavioral annex to model control programs, and captures a synchronous subset of AADL with continuous behaviors. We have also integrated modeling and formal analysis of \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\) models into the OSATE modeling environment for AADL.

Providing formal semantics and analysis for \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\), with its expressive control program formalism, continuous behaviors, and clock skews, and having to cover all possible continuous behaviors based on imprecise clocks, is challenging. We combine Maude [19] and the SMT solver Yices [21] to provide such a semantics, as well as symbolic reachability analysis of bounded invariant properties. To make the analysis feasible, our tool also implements a state-space reduction method that merges symbolic states for Maude-with-SMT to significantly improve the performance of symbolic reachability analysis. We illustrate the use of the \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\) language and tool—and compare its effectiveness with other state-of-the-art CPS analysis tools—on a number of hybrid CPS applications, including distributed drones that communicate to reach the “same” location, or fly in formation, without crashing into each other.

Our tool extends the SynchAADL tool [7, 9, 10] for distributed real-time systems without continuous behaviors, where the time when an event takes place can be abstracted away, so there is no need to consider clock skews, and any (sufficiently expressive) explicit-state model checker can be applied. In contrast, \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\) must model continuous behaviors and clock skews, and must analyze all possible behaviors based on when the continuous components are sampled and actuated, which depend on the imprecise local clocks. The tool is available at https://hybridsynchaadl.github.io.

2 Preliminaries

PALS and Hybrid PALS. When the infrastructure guarantees bounds \(\varGamma \) on clock skews, network delays, and execution times, the PALS pattern [4, 36] reduces the problems of designing and verifying virtually synchronous distributed real-time systems to the much simpler problems of designing and verifying their underlying synchronous designs: Given a synchronous system design \( SD \), bounds \(\varGamma \), and a period p of each round, the PALS transformation gives the asynchronous distributed real-time system \( PALS ( SD , \varGamma , p)\), which is stuttering bisimilar to \( SD \).

The synchronous design \( SD \) is formalized as the synchronous composition of state machines with input and output ports [36]. In each iteration, all machines simultaneously perform a transition, which includes reading inputs, changing the local state, and generating outputs (for the next iteration).

Hybrid PALS [8] extends PALS to virtually synchronous CPSs with physical environments that exhibit continuous behaviors. The physical environment \(E_M\) of a machine M has real-valued parameters \(\vec {x}=(x_1, \ldots , x_l)\). The continuous behaviors of \(\vec {x}\) are modeled by ordinary differential equations (ODEs) that specify different trajectories on \(\vec {x}\). \(E_M\) also defines which trajectory the environment follows, as a function of the last control command received by \(E_M\).

The local clock of a machine M can be seen as a function \(c_M:\mathbb {R}_{\ge 0} \rightarrow \mathbb {R}_{\ge 0}\), where \(c_M(t)\) is the value of the local clock at time t, with \(\forall t\in \mathbb {R}_{\ge 0}, \; |c_M(t)-t|< \epsilon \) for \(\epsilon >0\) the maximal clock skew [36]. In its ith iteration, a controller M samples the values of its environment at time \(c_M(i\cdot p)+t_s\), where \(t_s\) is the sampling time, and then executes a transition. As a result, the new control command is received by the environment at time \(c_M(i\cdot p)+t_a\), where \(t_a\) is the actuating time.

AADL. The Architecture Analysis & Design Language (AADL) [22] is an industrial modeling standard used in avionics, aerospace, automotive, medical devices, and robotics to describe an embedded real-time system. In AADL, a component type specifies the component’s interface (e.g., ports) and properties (e.g., periods), and a component implementation specifies its internal structure as a set of subcomponents and a set of connections linking their ports. An AADL construct may have properties describing its parameters, declared in property sets. The OSATE modeling environment provides a set of Eclipse plug-ins for AADL.

An AADL model describes a system of hardware and software components. Software components include threads that model the application software and data components representing data types. System components are the top-level components. A port is a data port, an event port, or an event data port. A component can have different modes and mode-specific property values, subcomponents, etc. Mode transitions are triggered by events.

Thread behavior is modeled as a guarded transition system with local variables using AADL’s Behavior Annex [23]. When a thread is activated, transitions are applied until a complete state is reached. The dispatch protocol determines when a thread is executed. A periodic thread is activated at fixed time intervals.

Maude with SMT. Maude [19] is a language and tool for formally specifying and analyzing distributed systems in rewriting logic. System states are specified as elements of algebraic data types, and transitions are specified using rewrite rules. In addition to its explicit-state analysis methods for concrete states, Maude provides SMT solving and symbolic reachability analysis for constrained terms \(\phi \parallel t\), which symbolically represent all instances of the term \(t(x_1, \ldots , x_n)\) satisfying the constraint \(\phi (x_1, \ldots , x_n)\) [40], using connections to Yices2 [21] and CVC4 [14].

3 The Hybrid SynchAADL Modeling Language

This section presents the \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\) language for modeling virtually synchronous CPSs in AADL. \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\) can specify environments with continuous dynamics, synchronous designs of distributed controllers, and nontrivial interactions between controllers and environments with respect to imprecise local clocks and sampling and actuation times.

The \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\) language is a subset of AADL extended with property set Hybrid_SynchAADL. We use a subset of AADL without changing the meaning of AADL constructs or adding a new annex—the subset has the same meaning for synchronous models and distributed implementations—so that AADL experts can easily develop and understand \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\) models.

figure b

Environment Components. An environment component models real-valued state variables that continuously change over time. State variables are specified using data subcomponents of type . Each environment component declares the property .

An environment component can have different modes to specify different continuous behaviors (trajectories). A controller command may change the mode of the environment or the value of a variable. The continuous dynamics in each mode is specified using either ODEs or continuous real functions as follows:

figure e

In \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\), a set of ODEs over n variables \(x_1, \ldots , x_n\), say, \(\frac{\mathrm {d}x_i}{\mathrm {d}t} = e_i(x_1, \ldots , x_n)\) for \(i = 1, \ldots , n\), is written as a semicolon-separated string:

figure f

If a closed-form solution of ODEs is known, we can directly specify concrete continuous functions, which are parameterized by a time parameter t and the initial values \(x_1(0), \ldots , x_n(0)\) of the variables \(x_1, \ldots , x_n\):

figure g

An environment component interacts with discrete controllers by sending its state values, and by receiving actuator commands that may update state variables or trigger mode (and hence trajectory) changes. This behavior is specified in \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\) using connections between ports and data subcomponents. A connection from a data subcomponent d inside the environment to an output data port o declares that the value of d is “sampled” by a controller. A connection from an environment’s input port i to d declares that a controller command arrived at i updates the value of the data subcomponent d.

Controller Components. Discrete controllers are usual software components in the Synchronous AADL subset [7, 9]. A controller component is specified using the behavioral and structural subset of AADL: hierarchical system, process, thread components, and thread behaviors defined by the Behavior Annex [23].

A controller receives the state of the environment at some sampling time, and sends a controller command to the environment at some actuation time. Sampling and actuation take place according to the local clock of the controller.

figure h

The top-level system component declares the following properties to state that the entire model is a synchronous design with a period T:

figure i

Communication. In \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\), connections are constrained for synchronous behaviors: no connection is allowed between environments, or between environments and the enclosing system components.

All (non-actuator) outputs of controller components generated in an iteration are available to the receiving controller components at the beginning of the next iteration. As explained in [7, 9], delayed connections between data ports meet this requirement. Therefore, two controller components can be connected only by data ports with delayed connections: .

Interactions between a controller and an environment occur instantaneously at the sampling and actuating times of the controller. Because an environment does not “actively” send data for sampling, every output port of an environment must be a data port, whereas its input ports could be of any kind.

4 The Hybrid SynchAADL Tool

This section introduces the \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\) tool supporting the modeling and formal analysis of \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\) models. The tool is an OSATE plugin which: (i) provides an intuitive language to specify properties of models, (ii) synthesizes a rewriting logic model from a \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\) model, and (iii) performs various formal analyses using Maude combined with SMT solving.

Specifying Properties. The tool’s property specification language allows the user to specify time-bounded invariant and reachability properties as propositional formulas whose atomic propositions are AADL Boolean expressions.

A “named” atomic proposition can be declared in \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\) as follows, where each identifier is fully qualified with its component path:

figure k

The following named invariant property holds if, for every (initial) state satisfying the initial condition \(\varphi _{ init }\), all states reachable within the time bound \(\tau _{ bound }\) satisfy the invariant condition \(\varphi _{ inv }\).

figure l

A reachability property (the dual of an invariant) holds if a state satisfying \(\varphi _{ goal }\) is reachable from some state satisfying \(\varphi _{ init }\) within the time bound \(\tau _{ bound }\).

figure m

Tool Interface. The tool first statically checks whether a given model is a valid model that satisfies the syntactic constraints of \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\).

\(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\) provides two analysis methods. Symbolic reachability analysis can verify that all possible behaviors satisfy a given requirement;Footnote 1 if not, a counterexample is generated. Randomized simulation repeatedly executes the model until a counterexample is found, by randomly choosing concrete sampling and actuating times, nondeterministic transitions, etc.

Fig. 1.
figure 1

Interface of the \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\) tool.

Full size image

Our tool also provides portfolio analysis that combines symbolic reachability analysis and randomized simulation. \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\) runs both methods in parallel using multithreading, and displays the result of the analysis that terminates first. Symbolic analysis can guarantee the absence of a counterexample, whereas randomized simulation is effective for finding “obvious” bugs.

Figure 1 shows the interface of our tool that is fully integrated into OSATE. The left editor shows the code of in Sect. 5, the bottom right editor shows its graphical representation, and the top right editor shows two properties in the property specification language. The \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\) menu contains three items for constraint checking, code generation, and formal analysis. The item has already been clicked, and the view at the bottom displays the analysis results in a readable format.

Tool Implementation. We have (in our report [33]) developed a Maude-with-SMT semantics for \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\) that formalizes our modeling language and implements our tool’s analysis commands. Maude is suitable to capture the expressive control program language, the hierarchical structure of systems, and communication. Symbolic rewriting with SMT allows us to analyze infinite states and all possible behaviors caused by sampling and actuation times with imprecise clocks, where continuous dynamics can be encoded in SMT [18, 26].

Nontrivial control programs with many conditional branches and guarded transitions typically involve a large number of symbolic states; to reduce the number of results of executing one iteration of the system, we have implemented a state merging optimization technique [11] that merges two symbolic states into one using disjunction and generalization. As shown in the report [33], this state merging dramatically improves the performance of symbolic analysis and makes the formal analysis feasible for such distributed hybrid systems.

The \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\) tool uses OSATE’s code generation facilities to synthesize a Maude model from the \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\) model. It then invokes Maude and an SMT solver to check whether the model satisfies given invariant and reachability requirements. Our tool is implemented in around 6,200 lines of Maude code and around 8,600 lines of Java and Xtend code.

5 Case Study: Collaborating Autonomous Drones

This section shows how virtually synchronous CPSs for controlling distributed drones—which collaborate to achieve common goals, such as rendezvous and formation control—can be modeled and analyzed in \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\).

Rendezvous of Multiple Drones. Consider N drones, where vectors \(\vec {x}_i\) and \(\vec {v}_i\), for \(1 \le i \le N\), denote the position and velocity of the i-th drone. The continuous dynamics of the i-th drone is specified by the ordinary differential equation \(\vec {\dot{x}}_i = \vec {v}_i\). The controller samples the drone’s position and velocity, and gives the new velocity value to the environment as a control command. The goal of rendezvous is for all drones to arrive near a common location simultaneously.

Figure 2 shows the AADL architecture of our rendezvous model for four drones. Each drone is connected to two other drones to exchange positions. A drone component consists of an environment (with the drone’s position and velocity) and its controller. Figure 3 shows the implementation of the top-level component, a system component, an system component, and a thread component for a drone controller in \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\).

In each round, the controller obtains the position \(\vec {x}\) from its environment at its sampling time. The position of the connected drone was sent in the previous round. The controller determines a new velocity to synchronize its movement with the other drones using a distributed consensus algorithm [39]. The environment changes its position according to the velocity indicated by its controller, where the new velocity \(\vec {v}\) becomes effective at its actuation time.

Fig. 2.
figure 2

The AADL architecture of four drones (left), and a drone component (right).

Full size image
Fig. 3.
figure 3

A \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\) model for four distributed drones.

Full size image

Verification. We analyze the following properties up to bound \(500~\mathrm {ms}\) using \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\) portfolio analysis: (i) drones do not collide ( ), and (ii) all drones can eventually gather together ( ).

figure u

We define three propositions: , defining the range of initial positions of the four drones , , , and ; , where two drones collide if the (horizontal and vertical) distance between them is less than 0.1; and , indicating that the distance between each pair of drones is less than 1. For example, and are defined as follows.

figure ae

The analysis result is shown in the view at the bottom of Fig. 1. There is a witness for , obtained by symbolic reachability analysis in 1.7 seconds. A counterexample for is found by randomized simulation in 1.5 seconds, since does not constrain the speed of the drones. In [33], we add initial velocity constraints, and verify that holds up to the time bound by symbolic reachability analysis in 15 minutes.

6 Experimental Evaluation

We compare the performance of \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\)’s symbolic analysis with four reachability analysis tools for hybrid automata, HyComp [18], SpaceEx [24], Flow* [17], and dReach [31], on models of rendezvous and formation control for distributed drones, and on networked thermostats (adapted from [6, 29]). We use simplified models with less complex control; otherwise, most of the other tools time out (see [33] for results on more complex models). We use two invariant properties for each model: \( Inv _\top \), which holds, and \( Inv _\bot \), which does not hold.

To use the other tools, we have “encoded” the synchronous designs of the \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\) models as networks of hybrid automata. Each component is modeled as a hybrid automaton with three modes: starting a new round, sampling, and controller transition/actuation. The behavior of a controller is encoded as single jumps. We use flat hybrid automata (obtained by HYST [12]) for Flow* and dReach, which do not support networks of hybrid automata.

We measure the execution times for analyzing the invariant properties up to bound \(500~\mathrm {ms}\), with a timeout of 60 minutes. For \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\), we use a specialized version of Maude with Yices 2.6 for polynomial arithmetic [44]. For SpaceEx, we use PHAVer for linear dynamics, and STC for nonlinear polynomial dynamics. For Flow*, we use adaptive steps, and TM orders 1 (for single) and 2 (for double). We use the default precision for dReach, and BMC for HyComp. We have run all experiments on Intel Xeon 2.8GHz with 256 GB memory.

Table 1. \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\) vs. HyComp, SpaceEx, dReach, and Flow*.
Full size table

The results are summarized in Table 1, as execution times (seconds) over time bounds (\(B \cdot 100\,\mathrm {ms}\)), with N the number of components. The results for “Rend (double)” (rendezvous with double-integrator dynamics, where control input is given by acceleration instead of velocity) do not include HyComp, which does not support nonlinear polynomial dynamics. For \( Inv _\top \), Table 1 shows the largest time bound for which the tool could prove the absence of counterexamples. Often, tools timed out when trying to verify that \( Inv _\top \) holds up to time bound 500.Footnote 2 For \( Inv _\bot \), the table shows the smallest bound for which the tool found counterexamples.Footnote 3 As seen, \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\) outperforms the other tools in most cases, in particular for complex models with larger N.

7 Related Work

Our tool can model check virtually synchronous CPSs with both complex control programs and continuous behaviors (and imprecise local clocks, etc.), whereas most formal tools are strong at analyzing either discrete or continuous behaviors. The latter includes analysis tools for hybrid automata [13, 18, 24], which do not deal well with the “discrete complexity” (e.g., control programs) of CPSs.

The Hybrid Annex  [2, 3] allows specifying continuous behaviors in AADL, but message delays, clock skews, etc., are not taken into account. Controllers are defined in Hybrid CSP instead of in AADL’s convenient Behavioral Annex. Another hybrid annex is proposed in [38], and an AADL sublanguage, AADL+, in [35]. None of these languages support automated formal correctness analysis.

Hybrid PALS models with simple controllers are encoded as logical formulas and analyzed by dReal in [8]. However, there is no tool support, and so CPSs must be manually modeled as SMT formulas in [8]. In contrast, we provide a tool for modeling Hybrid PALS models using a well-known modeling standard.

Our work is also related to almost-synchronous systems, including approximate synchrony [20], quasi-synchrony [15, 16, 28, 32], GALS [27, 37], time-triggered architectures [41, 43], etc. Our method makes it possible to verify such systems with continuous behaviors, which are typically not considered in related work.

8 Concluding Remarks

We have presented the \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\) modeling language and formal analysis tool for modeling and analyzing the synchronous designs—and, by the Hybrid PALS equivalence, also the corresponding asynchronous distributed real-time system with bounded clock skews, network delays, and execution times—of virtually synchronous networks of hybrid systems with potentially complex control programs in the modeling standard AADL. Our tool provides randomized simulation and symbolic reachability analysis, and is fully integrated into the OSATE modeling environment for AADL. We have shown that in most cases, \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\)’s symbolic analysis outperforms state-of-the-art hybrid systems reachability analysis tools on a number of distributed hybrid systems.

Currently, \(\textsc {Hybrid}\textsc {Synch}\textsc {AADL}\)’s symbolic analysis is restricted to systems with (nonlinear) polynomial continuous dynamics, because the underlying SMT solver, Yices2, cannot deal with general classes of ODEs. We should therefore integrate Maude with ODE solvers such as dReal [25] and Flow* [17].