Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Cyber-Physical Systems

The term Cyber-Physical Systems (CPS) describes systems that combine computing elements with dedicated hardware and software having to monitor and control a particular physical environment. This combination of the physical with a virtual world provides the digital foundation for smart solutions throughout society and within all sectors. The constant demand for increased functionality and performance that needs to be produced with tight time schedules and cost budges without compromising dependability of the final products constitutes a significant software engineering challenge.

What is needed are mathematically well-founded, scalable methods, tools and techniques that support the development of CPS. For this we have over more than 20 years pursued a model-based approach for the design of dependable and optimal CPS, supported by tools that are based on efficient algorithms and datastructures for analysis of semantically well-founded models. This has been the guiding pricinple behind the Uppaal suite (www.uppaal.org) [54] which by now have been applied to a wide range of industrial applications from the domains of Embedded Systems and Cyber-Physical Systems.

The first version of the Uppaal tool was presented at the very first TACAS conference in 1995 in Aarhus, Denmark. During the first several years the tool was developed in tight collaboration between Uppsala University, Sweden and Aalborg University, Denmark. Over the years a number branches has been developed, some of which will be described in the following sections.

1 The UPPAAL Tool Suite

Uppaal. The underlying formalism of Uppaal is that of timed automata with the tool providing support for model checking of hard real-time properties. Since the introduction of the tool in 1995, significant effort have been put into development and implementation of improved datastructures and algorithms for the analysis of timed automata. This includes guided search algorithms using heuristics from AI [6, 40, 46, 47], fully symbolic datastructures [9], minimal constraint normal forms [50], as well as a new symblistic DART datastructure [43, 45] making usefull tradeoffs between the effectiveness of discrete and symbolic semantics. Also, this research has included the development of a series of exact abstractions (or extrapolation) that not only ensures finiteness of the symbolic semantics, but also provide significant performance improvements [3, 4, 42]. Besides these advance with respect to the verification engine, significant effort has over the years been put on the graphical interface of the tool (e.g. [7]), and on the modelling side the introduction of user-defined, structured datatypes and procedures has undoubtedly made the tool significantly more usable in modeling real control programs and communication protocols [6].

Uppaal Cora. Motivated by the need for addressing (optimal) usage of resource, extension of priced timed automata was introduced in 2001 with [2, 8] (independently) demonstrating decidability of cost-optimal reachability. Soon after efficient priced extension of the symbolic zone datastructures was implemented in the branch Uppaal Cora, which combined with a symbolic A* algorithm providing a new generic tool for cost-optimal planning competetive to traditional OR methods such as Mixed-Integer Linear Programming [49]. Most recently new efficient extrapolation methods for priced timed automata has been introduced [17] and Uppaal Cora has been used for the optimal planning of missions for battery-powered nano-satelittes [12].

Uppaal Tron. In 2004 the branch Uppaal Tron was introduced offering the possibility of performing on-line conformance testing of real real-time systems with respect to timed input-output automata [51, 56]. Uppaal Tron implements a sound and (theoretically) complete randomized testing algorithm, and uses a formally defined notion of correctness to assign verdicts: i.e. relativized timed input/output conformance providing a timed extension of Jan Tretmans ioco [58]. Using online testing, events are generated and simultaneously executed on the system under test. Uppaal Tron has been succesfully applied to a number of industrial case studies including an advanced electronic thermostat regulator sold world-wide in high volume by the Danish company Danfoss [52].

Uppaal Tiga. In 2005 - encouraged by suggestions from Tom Henzinger – the branch Uppaal Tiga was released, allowing for control strategies to be synthesized from timed games, i.e. two-player games played on a timed automata [5, 24]. The branch implements an efficient symbolic on-the-fly algorithm for synthesizing winning strategies for reachability, safety as well as Büchi objectives and taking possible partial observability into account [25]. The branch marks a disruptive direction with respect to development of control programs for embedded systems: rather than manually developing the control program with subsequent model checking (and correction), Uppaal Tiga provides a fully automatic method for deriving a correct-by-construction control program. In particular, this method allows for easy personalization of control program simply by modification of the objective. The branch has so far been industrially applied to the automatic synthesis of control strategies for zone-base climate control in pigsties [44] and safe and optimal operation of hydralic pumps [26].

Uppaal Ecdar. In 2010 the branch Uppaal Ecdar was introduced supporting a scalable methodology for compositional development and stepwise refinenemet of real-time systems [36, 38]. The underlying specification theory is that of timed I/O automata being essentially timed games (with inputs being controllable, and outputs being uncontrollable) equipped with suitable methods for refinement checking (in terms of an alternating simulation between two timed game specifications), consistency checking, logical as well as structural composition. The Uppaal Ecdar branch uses heavily the Uppaal Tiga engine to solve various games that arise in the computing the various composition operators and refinements. For a full account of Uppaal Ecdar we refer the reader to the tutorial [35].

2 UPPAAL SMC

One of most recent branches of the Uppaal tool suite – Uppaal  SMC introduced in 2011 – allows for performance evaluation the much richer formalisms of stochastic hybrid automata and games [33, 34] and has by now been widely applied to analysis of a variety of case studies ranging from biological examples [32], schedulability for mixed-critical systems [13, 37], evaluation of controllers for energy-aware buildings [28], social-technical attacks in security [39] as well as performance evaluation of a variety of wireless communication protocols [59]. Also the statistical model checking engine of Uppaal  SMC is supported by a distributed implementation [23], and allows for the statistical model checking of a large subset of MITL [21, 22]. For a full account of Uppaal  SMC we refer the reader to the recent tutorial [31].

The modeling formalism of Uppaal  SMC is based on a stochastic interpretation and extension of the timed automata formalism used in the classical model checking version of Uppaal. For individual components the stochastic interpretation replaces the nondeterministic choices between multiple enabled transitions by probabilistic choices (that may or may not be user-defined). Similarly, the non-deterministic choices of time-delays are refined by probability distributions, which at the component level are given either uniform distributions in cases with time-bounded delays or exponential distributions (with user-defined rates) in cases of unbounded delays.

To illustrate the features of Uppaal  SMC let us consider the example in Fig. 1, providing an “extended” timed automata based model of a car, that needs to make it from its initial position to the final position . In the model the driver of the car twice needs to make a choice between using a high road ( and ) or a low road ( and ). The four roads differ in their travel-times between 0 and 100 min (respective 0 and 50 min) as reflected by the invariants on the clock x). Also the roads differ in fuel-consumption reflected by the difference in the rate of the continuous variable fc (representing the total amount of fuel consumed). The model is in fact a priced timed automaton (as supported by the branch Uppaal Cora) with the total time that it will take to make it to ranging between 0 and 200, and total fuel-consumption ranging between 0 and 900. However, interpreted as a stochastic priced timed automaton, the discrete choice betweeen the high and the low roads are made based on a (uniform) random choice. Similary, the travel times of the 4 roads are resolved using uniform distributions of the respect travel-time intervals.

Fig. 1.
figure 1

The stochastic route model for a car

Full size image

Now assume that we are interested in the expected fuel-consumption before reaching the goal . Given the described stochastic semantics of the priced timed automaton in Fig. 1 this is easily seen to be the value of the following expression:

$$\begin{aligned}&\Big (0.5\cdot \int _{t=0}^{100}3t\cdot 0.01 dt + 0.5\cdot \int _{t=0}^{50}10t\cdot 0.02 dt\Big ) +\\&\Big (0.5\cdot \int _{t=0}^{100}1t\cdot 0.01 dt + 0.5\cdot \int _{t=0}^{50}8t\cdot 0.02 dt\Big ) = 325 \end{aligned}$$

For this model the above expression giving the desired expectation was particularly easy as the clock \(\mathtt{x}\) is reset. In general – and formally – the stochastic semantics of a stochastic (priced) timed automata is given by a probability measure assigning probabilities to (certain) sets of runs, being countable unions or complements of so-called cylinder-sets, i.e. sets of runs that follow the same prefix of edges in the automaton. In general, the probability of such a cylinder will be a nested integral (the nesting depth being the length of the path in the automaton). When considering networks of stochastic timed automata, the probability measure will moreover reflect a repeated race between components (for who is to perform the next discrete action) of the networks. Decidability (and undecidability) results for the stochastic interpretation of timed automata have so far – despite significant research – only given few conclusive results, e.g. that qualitative reachability (i.e. probability of reachability is 0 or 1) is decidable for one-clock stochastic timed automata [11, 14], or for acyclic models [55]. Instead, the statistical model checking engine of Uppaal  SMC resorts to simulation in order to settle a large range of quantitative questions, e.g. reachability probability or expectations. Being based on simulation, the results are however approximate (e.g. confidence intervals) but come with a statistically assured level of confidence. As an example, the Uppaal  SMC query

will after some 7382 random runs of the model (made according to the stochastic semantic described) return the 95% confidence interval [0.735636, 0.755635] as the probability that the location is reached within 100 minutes. Addressing our original problem the query

will return the value \(322.565\pm 4.70747\) as an estimate of the expected fuel-comsumption based on 5000 random runs of the model. In Fig. 2 we see the additional plots offered by Uppaal  SMC for the cumulative probability of the time for reaching and the frequency count of the fuel-consumption over 5000 random runs.

Fig. 2.
figure 2

Performance evaluation of stochastic car model.

Full size image

3 UPPAAL Stratego

Uppaal Stratego from 2014 [29, 30] is the most recent branch of the Uppaal tool suite that allows to generate, optimize, compare and explore consequences and performance of strategies synthesized for stochastic priced timed games (SPTG) in a user-friendly manner. In particular, Uppaal Stratego comes with an extended query language (see Table 1), where strategies are first class objects that may be constructed, compared, optimized and used when performing (statistical) model checking of a game under the constraints of a given synthesized strategy. As such Uppaal Stratego may be seen as a superset of Uppaal Tiga and Uppaal  SMC.

Table 1. Various types of Uppaal Stratego queries: “strategy S =” means strategy assignment and “under S” is strategy usage via strategy identifier S. Here the variables NS, DS and SS correspond to non-deterministic, deterministic and stochastic strategies respectively; bound is a bound expression on time or cost like and n is the number of simulations.
Full size table

To illustrate the features of Uppaal Stratego, let us revise our running example of the car-route-problem as illustrated in in Fig. 3. Again there are four different roads with their individual required travel-times.

Fig. 3.
figure 3

The stochastic decision model for a car.

Full size image

However, whereas the choice of road is up to the driver of the car to control (indicated by the solid transitions), the actual travel-time of the road is uncontrollable (indicated by the dashed transitions) reflecting the uncertainty of the amount of traffic on the particular day. In one scenario, the objective of the car it to choose the combination of roads that will ensure the shortest overall travel-time even in the most hostile traffic situation on the four roads. Under this interpretation, Fig. 3 represents a timed game. Clearly the strategy that would ensure the smallest worst-case travel-time is to take the two low roads, giving a guaranteed arrival time in 100 min. Taking the rates for the cost variable fc into account, makes Fig. 3 describe a priced time game, where the problem is to determine the best strategy in terms of minimizing the worst-case fuel-consumption. For our model this best strategy clearly consists in consistently choosing the high roads. Unfortunaltely, cost-optimal winning strategies for priced games is undecidable in general when the underlying timed automata has three or more clocks [20]. Decidability results have been provided for one-clock priced timed games [19] and for so-called strongly cost-non-zeno priced timed games [15, 16]; also approximate algorithms have been proposed [18].

However in Uppaal Stratego, the model of Fig. 3 is interpreted as a stochastic priced timed game (SPTG), assuming that the travel-times of the four roads are chosen by uniform distributions, and the objective of the control strategy is to minimize the expected overall travel-time, or the expected overall fuel-consumption (e.g. the rate or fuel-consumption on the first high road indicates that the cost variable fc grows with rate 3 in this location).

We are interested in synthesizing strategies for various objectives. Being primarily concerned with fuel-consumption we may want to determine the strategy that will minimize the expected fuel-consumption. For our simple decision model Fig. 3 this is clearly given by the following expression:

$$\begin{aligned}&min\Big \{\int _{t=0}^{100}3t\cdot 0.01 dt\, , \, \int _{t=0}^{50}10t\cdot 0.02 dt\Big \} +\\&min \Big \{\int _{t=0}^{100}1t\cdot 0.01 dt\, , \, \int _{t=0}^{50}8t\cdot 0.02 dt\Big \} = 200 \end{aligned}$$
Fig. 4.
figure 4

Evaluation of strategy via simulation.

Full size image

However, possing the Uppaal Stratego query

will provide (by reinforcement learningFootnote 1) the strategy Opt, that minimizes the expected total fuel-consumption, learning from runs which are maximally 200 time units long. The relativized query , generates 1000 runs of length 200 time units and then averages the maximum value of fc from each run. this is used to estimate the expected cost to be . Figure 4a summarizes 10 random runs according Opt illustrating fuel-consumption. None of the runs had a fuel consumption of 400 indicating that we always choose the energy-efficient roads. In Fig. 4b we see that this is actually the case as the simulations always choose to go to locations and , which models the energy-efficient roads.

Now, assume that the task must be completed before 150 time-units. From Fig. 4 it can be seen that the strategy Opt unfortunately does not guarantee this, as there are a few runs which exceeds 150 before reaching . However, the query

will generate the most permissive (non-deterministic) strategy Safe that guarantees this bound but unfortunately with a high expected total fuel-consumption of 342.19. However, the relativized learning query

will provide a sub-strategy OptSafe that minimizes the expected total fuel-consumption – here found to be 279.87 – subject to the constraints of Safe. Figure 5 summarizes 10 random runs according to SafeOpt, incidating that only road is never choosen. Also, the failed model checking of reveals that the high road H2 may only be choosen in case the first phase is completed before 50 time-units, confirming the observations from the simulations.

Fig. 5.
figure 5

Evaluation of strategy OptSafe via simulation.

Full size image
Fig. 6.
figure 6

Total fuel-consumption versus time at mid-location for runs 1000 runs choosing between and towards learning the strategy OptSafe.

Full size image
Fig. 7.
figure 7

Overview of Uppaal Stratego

Full size image

For learning the strategy OptSafe the reinforcement learning method required 5 iterations each with 1000 runs. We illustrate in Fig. 6 the outcome of the runs in the last 3 iterations focusing on the choice, time and resulting fuel-consumption at the choice-point between and . As can be seen the method correctly learns to take the low road whenever the choice point is reached before a total time of 50 min (leaving enough time to guarantee that will be reached within 150 min.

In general, as shown in the overview Fig. 7, Uppaal Stratego will start from a SPTG \(\mathcal {P}\). It can then abstract \(\mathcal {P}\) into a timed game (TGA) \(\mathcal {G}\) by simply ignoring prices and stochasticity in the model. Using \(\mathcal {G}\), Uppaal Tiga [5] may now be used to (symbolically) synthesize a (most permissive) strategy \(\sigma \) meeting a required safety or (time-bounded) liveness constraint \(\phi \). The TGA \(\mathcal {G}\) under \(\sigma \) (denoted \(\mathcal {G}|\sigma \)) may now be subject to additional (statistical) model checking using classical Uppaal [54] and Uppaal  SMC [31, 34]. Similarly, the original STGA \(\mathcal {P}\) under \(\sigma \) may be subject to statistical model checking. Now using reinforcement learning [29], we may synthesize near-optimal strategies that minimizes (maximizes) the expectation of a given cost-expression cost. In case the learning is performed from \(\mathcal {P}|\sigma \), we obtain a sub-strategy \(\sigma ^o\) of \(\sigma \) that optimizes the expected value of cost subject to the hard constraints guaranteed by \(\sigma \). Finally, given \(\sigma ^o\), one may perform additional statistical model checking of \(\mathcal {P}|\sigma ^o\).

4 Applications

The importance of CPS is clear within the domains of energy and transport with the emergence Smart Grid, Home Automation, Autonomous Driving, Advanced Driver Assistance and Intelligent Traffic Control where optimizing critical functionality is provided by intelligent and flexible software components. Uppaal stratego has already been applied to a number of case studies including synthesis of a safe and optimal adaptive cruice control [53], synthesis of optimal floor heating system [48], and most recently synthesis of optimal control of traffic lights in intersections as described in the following sub-sections.

Adaptive Cruice Control. These days the Google Self-Driving car is about to become a reality: legislation has been passed in several U.S. states allowing driverless cars, in April 2014, Google announced that their vehicles had been logging nearly 1.1 million km, and it is forecast that Google’s self-driving cars will hit the roads this summer. Also, in Europe driverless cars have been actively pursued, both by the automotive industry itself and within a number of national and European research projects (e.g. FP7 and Horizon2020). With more and more traffic, European roads are becoming increasingly congested, polluted and unsafe. One potential solution to this growing problem is seen to be the use of small, automated, low-polluting vehicles for driverless transport in (and between) cities. Within the last decade, a number of European projects have been launched for making transport systems capable of fully automated driving, energy efficient and environmentally friendly while performing. In addition, many individual driving assistant systems based on suitable sensors have been developed for cars.

Fig. 8.
figure 8

Smallest distance possible under the safe strategy as a function of speed difference computed using for each v value. Connecting lines are from linear regression analysis.

Full size image

In [53], we have considered a small part of lane-change manoeuvres, namely the existence of a safe-distance controller (assumed in the above work of Olderog et al.). In particular, we demonstrated how Uppaal Stratego may be applied to automatically obtain a safe yet optimal adaptive strategy safe for the cruice control. Modelling the cruice control as a game with a car in front a safe strategy was synthezed ensuring that the distance to the front care would never get below 5 meters. In fact utilizing the distinct feature of Uppaal Stratego – allowing additional properties to be verified of a synthesized strategy – we may verify the smallest distance possible to the front care which will not violate the safe as shown in Fig. 8.

Now asking for a sub-strategy safeFast of safe that will minimize the expected accumulated distance to the front care yields a substantial improvement as seen in Fig. 9.

Fig. 9.
figure 9

The probability density distribution over rDistance at thus after 100 time units under the strategies safe and safeFast. The (dark) red bars for safe and the (light) green bars for safeFast. (Color figure online)

Full size image

Home Automation. Home automation includes the centralized control of a number of functionalities in a house such as lighting, HVAC (heating, ventilation and air conditioning), appliances, security locks of gates and doors as well as other systems. The overall goal is to achieve improved convenience, comfort, energy efficiency as well as security. The popularity of home automation has increased significantly in recent years through affordable smartphone and tablet connectivity. Also the emergence of “Internet of Things” has tied in closely with the popularization of home automation.

In [48] we collaborated with the Danish company Seluxit within the European project CASSTINGFootnote 2. The focus was on the floorheating system of a family house, where each room of the house has its own hot-water pipe circuit. These are controlled through a number of valves based on information about room temperatures communicated wirelessly (periodically due to energy considerations) from a number of temperature sensors. In the existing system, a simple “Bang-Bang”-like strategy is applied, however, there are though several problems with this strategy, as experienced by the house owner: it completely disregards the interaction between rooms in terms of heat-exchange, the impact of the outside temperature and weather forecast as well as information about movements in the house. Taking this knowledge into account should potentially enable the synthesis of significantly improved control strategies. Unfortunately, direct application of Uppaal Stratego does not scale: due to the enormous number of control modes it is virtually impossible to learn optimal control. Instead, we proposed a novel on-line synthesis methodology, where we periodically—and on-line—learn the optimal controller for the near future based on the current sensor readings. For additional scalability, we proposed and applied a novel compositional synthesis approach.

In particular, the strategy provided by Uppaal Stratego takes weather information into account, as illustrated by Fig. 10 showing the spring stability scenario. From points of time between 0 and 500 min, the outside temperature increases and exceeds the target temperature. We observe that since the controller synthesized by Uppaal Stratego is able to look at the weather forecast for the next 45 min, it shuts down the valves much earlier than the other controllers. This results in energy savings and increased comfort.

Fig. 10.
figure 10

Room temperatures in the spring stability scenario

Full size image

Intelligent Control of Trafic Light. The Danish Congestion Commission calls in its recent report for improved traffic signal control in order to reduce congestion, travel time and energy consumption. This project has been formulated to contribute to a more efficient utilisation of the existing infrastructure by improving traffic signal control. However, modern traffic lights use information from induction loops and to some extend radar information. Recent developments in radar technology has made it possible to obtain more detailed information relevant to the control mechanism of the traffic light. Unfortunately much of the current controllers do not profit from this additional information. Using this information could minimize waiting times and energy waste.

Fig. 11.
figure 11

Intersection between Nylandsvej and Værkstedvej at Køge municipality. Layout of loops and radar area.

Full size image

Within the Innovation Center DiCyPSFootnote 3 we have collaborated with researchers in traffic control to apply Uppaal Stratego to the synthesis of an efficient traffic signal control strategy that takes advantage of the continuous traffic monitoring made available by radar detectors. The purpose of the strategy is to optimize the total traffic flow in the junction, i.e. to reduce the total delay, queue length and the number of stops. The synthesis of Uppaal Stratego is done on-line offering every 5 s a new updated optimal strategy for the next operation of a signalized intersection in the municiplaity of Køge, Denmark, Fig. 11. In doing so the Uppaal Stratego model takes into account the random generation of traffic in the various directions. The on-line strategy generated is fed to a richer simulation engine in SUMO, an open source tool which allows to model and simulate traffic systems. SUMO also provides a number of supporting tools which allow for visualization, network transformation, waiting time calculations, traffic light performance, etc.

Table 2. Results of the experiments. We show the mean and the 95 percentile for respectively the waiting time of the cars and the queue length. This is done for each controller in all scenarios.
Full size table

In the resulting evaluation shown in Fig. 2 we have compared the performance of a so-called Static controller, the Loop Controller and the Uppaal Stratego controller. In the most demanding MAX scenario – with highest intenty of traffic – it is clear that the Uppaal Stratego controller is performining significantly better than any of the others. For MID scenario the findings are similar and for the LOW scenario all the controllers perform quite similar, but the Loop controller is in general the best (Table 2).