Abstract We introduce a formal modeling methodology to analyze quantum communication protocols in the tool Uppaal . Our approach encodes quantum states, operations, and measurements into Uppaal timed automata with data extensions and external function calls, enabling both exhaustive verification in the ideal (noiseless) case and statistical model checking for realistic noisy scenarios. We apply our framework to the Beyond Superdense Coding protocol—a time-slotted variant of superdense coding—combined with quantum entanglement distillation, and demonstrate that Uppaal can deal with these protocols even under complex timing and decoherence constraints.

A real-time systems (RTS) typically consists of a set of real-time tasks that execute on a multicore platform following a scheduling policy. In an RTS, computing inter-core bounds, i.e., bounds separating events occurring on different cores, is crucial. While efficient techniques to over-approximate such bounds exist, little has been proposed to compute their exact values. Given an RTS with a set of cores$c$and a set of tasks$T$, under partitioned fixed-priority scheduling with limited preemption, a recent work by Foughali, Hladik and Zuepke (FHZ) models tasks with affinity$c$(i.e., allocated to core$c\in C$) as a Uppaaltimed automata (TA) network$N_{C}$. Through compositional model checking, FHZ achieved a substantial gain in scalability for bounds local to a core. However, computing inter-core bounds for some events of interest$E$, produced by a subset of tasks$T_{E}\subseteq T$with different affinities$C_{E}\subseteq C$, requires model checking$N_{E}=\Vert _{c\in C_{E}}N_{c}$, i.e., the parallel composition of all TA networks$N_{c}$for each$c\in C_{E}$, which often produces an intractable state space. In this paper, we present a new scalable approach based on exact abstractions to compute exact inter-core bounds in a schedulable RTS, under the assumption that tasks in$T_{E}$have distinct affinities. We develop a new Uppaalquery, and a novel algorithm that computes, for each TA network$N_{c}$in$N_{1\mathrm{i}}$, an abstraction$\mathcal{A}(N_{c})$preserving the exact intervals within which events occur on$c$. Then, we model check$\mathcal{A}(N_{E})=\Vert _{c\in C_{E}}\mathcal{A}(N_{c})$(instead of$N_{E}$), therefore drastically reducing the state space. We demonstrate the scalability of our approach as we efficiently compute inter-core bounds for the WATERS 2017 industrial challenge, where FHZ fails to scale.

Energy-driven computing is a recent paradigm that promotes energy harvesting as an alternative solution to conventional power supply systems. A crucial challenge in that context lies in the dimensioning of system resources w.r.t. energy harvesting conditions while meeting some given timing QoS requirements. Existing simulation and debugging tools do not make it possible to clearly address this issue. This paper defines a generic modeling and analysis framework to support the design exploration for energy-driven computing. It uses stochastic hybrid automata and statistical model-checking. It advocates a distributed system design, where heterogeneous nodes integrate computing and harvesting components and support inter-node energy transfer. Through a simple case-study, the paper shows how this framework addresses the aforementioned design challenge in a flexible manner and helps in reducing energy storage requirements.

Floor heating systems are important components of nowadays home-automation setups. The control of a floor heating system is a nontrivial task and the present solutions essentially implement variants of a simple bang-bang controller that opens for a hot water circulation in a room if its current temperature is below the user defined target temperature, otherwise it closes for the heating in the room. The disadvantage is that the heat exchange among the rooms, outside weather conditions, weather forecast and other factors are not considered. We propose a novel model-driven approach for intelligent floor heating control based on a chain of tools that allow us to gather the sensor readings from the actual hardware and use the state-of-the-art controller synthesis tool UPPAAL Stratego in order to synthesise abstract control strategies that are then executed on the real hardware platform provided by the company Seluxit. We have built a scaled demonstrator of the system and the experimental results document a 38% to 52 % increase in user satisfaction, moreover with additional energy savings between 2% to 12%.

The analysis of probabilistic schedulability explores all possible combinations of the probabilities of task attributes, which can easily lead to exponential computation time [24]. In this paper, we present a flexible schedulability analysis framework for periodic and sporadic tasks having probabilistic attributes where the computation time scales linearly in the size of analyzed systems. The framework is given in terms of a set of Parameterized Stopwatch Automata (PSA) models, which leads to a large degree of flexibility. Probability distributions for response time are generated using statistical model checking (UPPAAL SMC) while the overall schedulability can be checked using symbolic model checking (UPPAAL). We also define PoMD (percentage of missed deadlines) as a measure of the probabilistic schedulability of systems. To evaluate our approach, we compare the time used for computing response times and the analysis results using similar task models to that of a related analytical approach.

We present the concept of degree of schedulability for mixed-criticality scheduling systems. This concept is given in terms of the two factors 1) Percentage of Missed Deadlines (PoMD), and 2) Degradation of the Quality of Service (DoQoS). The novel aspect is that we consider task arrival patterns that follow user-defined continuous probability distributions. We determine the degree of schedulability of a single scheduling component which can contain both periodic and sporadic tasks using statistical model checking in the form of UPPAAL SMC. We support uniform, exponential, Gaussian and any user-defined probability distribution.

UPPAAL-TRON is a new tool for model based online black-box conformance testing of real-time embedded systems specified as timed automata. In this paper we present our experiences in applying our tool and technique on an industrial case study. We conclude that the tool and technique is applicable to practical systems, and that it has promising error detection potential and execution performance.