Defined as the ability for a system to exchange data with another system and consume data from another system, interoperability is a property that most distributed system developers tend to satisfy when designing new systems. In the IoT domain, the WoT W3C standard has been proposed to enable interoperability between devices and platforms.The Arrowhead framework has been implemented to ease IoT automation with the objective to enable IoT interoperability in this domain.This paper discusses how the W3C Web of Things standard can help the IoT automation framework Arrowhead in achieving the interoperability.

This paper presents how the ICT infrastructure developed in the European ENCOURAGE project, centered around a message oriented middleware, enabled energy savings in buildings and households. The components of the middleware, as well as the supervisory control strategy, are overviewed, to support the presentation of the results and how they could be achieved. The main results are presented on three of the pilots of the project, a first one consisting of a single household, a second one of a residential neighborhood, and a third one in a university campus.

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%.

A smart house is a complex system, and configuring it to act as desired is difficult and error prone. In this paper we extend a previously developed framework based on timed automata for designing safe and reliable home automation scenarios to make it easier to use. To do so we abstract it with an Event-Condition-Action language to create intelligent scenarios, and constraints that prevent scenarios with undesirable behaviours to be applied. This language is itself abstracted by a graphical user interface that enables the creation of scenarios by manipulating graphical blocks representing elements of the language. We have designed and implemented a prototype system to test our approach, and we report on a qualitative user study that was conducted.

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.

Industrial processes use energy to transform raw materials and intermediate goods into final products. Many efforts have been done on the minimization of energy costs in industrial plants. Apart from working on “how” an industrial process is implemented, it is possible to reduce the energy costs by focusing on “when” it is performed. Although, some manufacturing plants (e.g. refining or petrochemical plants) can be inflexible with respect to time due to interdependencies in processes that must be respected for performance and safety reasons, there are other industrial segments, such as alumina plants or discrete manufacturing, with more degrees of flexibility. These manufacturing plants can consider a more flexible scheduling of the most energy-intensive processes in response to dynamic prices and overall condition of the electricity market. In this scenario, requests for energy can be encoded by means of a formal structure called flex-offers, then aggregated (joining several flex-offers into a bigger one) and sent to the market, scheduled, disaggregated and transformed into consumption plans, and eventually, into production schedules for given industrial plant. In this paper, we describe the flex-offer concept and how it can be applied to industrial and home automation scenarios. The architecture proposed in this paper aims to be adaptable to multiples scenarios (industrial, home and building automation, etc.), thus providing the foundations for different concept implementations using multiple technologies or supporting various kinds of devices.

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.

Residential gateways for home automation are prerequisites to obtain optimal exploitation of energy resources, and they also have the potential to provide a unified operation of various home devices and appliances. Although a number of protocol standards have been proposed, the number of commercially available systems is still very limited. One reason for this is the diversity of device manufacturing standards; another is the lack of efficient and expressive middleware for defining control algorithms and usage scenarios. In this paper we present the architectural design of a distributed middleware system for residential gateways including a simple composition language. Also, we present the initial experiences obtained from a prototype implementation of the system.

Models of embedded systems with communicating actors and deadlines offer abstraction and encapsulation of related functionality, but their behavior is complex. Verification is therefore difficult and requires a combination of simulation, model checking and testing tools. In order to rely on the results, these tools must use consistent semantics for the model. Yet, a monolithic semantic model is just as complex as the entity it describes. In order to circumvent this issue, we define a three level semantics giving independent definitions of the functionality of actors, the temporal properties of communications, and finally imposing deadlines on the timing of dependent actors. With this approach the semantics is used directly in developing a simulator supporting the nondeterminism of the abstract semantics such that e.g. potential race conditions can be detected. The layers are also planned to underpin independent specialized verification tools. The verification task for timed, hybrid systems can thus be divided into the continuous, discrete, and timing domains with automated translation to specialized tools, and this promises better scalability than simulation or model checking of one complex model.

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.

Generating timed test sequences by hand is error-prone and time consuming, and it is easy to overlook important scenarios. The paper presents a tool based on formal methods that automatically computes a test suite for conformance testing of time critical systems. The generated tests are selected on the basis of a coverage criterion of the specification. The tool guarantees production of sound test cases only, and is able to produce a complete covering test suite. We demonstrate the tool by generating test cases for the Philips Audio Protocol.

A formal and automatic verification of a real-life protocol is presented. The protocol, about 2800 lines of assembler code, has been used in products from the audio/video company Bang & Olufsen throughout more than a decade, and its purpose is to control the transmission of messages between audio/video components over a single bus. Such communications may collide, and one essential purpose of the protocol is to detect such collisions. The functioning is highly dependent on real-time considerations. Though the protocol was known to be faulty in that messages were lost occasionally, the protocol was too complicated in order for Bang & Olufsen to locate the bug using normal testing. However using the real-time verification tool UPPAAL, an error trace was automatically generated, which caused the detection of "the error" in the implementation. The error was corrected and the correction was automatically proven correct, again using UPPAAL. A future, and more automated, version of the protocol, where this error is fatal, will incorporate the correction. Hence, this work is an elegant demonstration of how model checking has had an impact on practical software development. The effort of modeling this protocol has in addition generated a number of suggestions for enriching the UPPAAL language. Hence, it's also an excellent example of the reverse impact.

We propose a language for testing concurrent processes and examine its strength in terms of the processes that are distinguished by a test. By using probabilistic transition systems as the underlying semantic model, we show how a testing algorithm with a probability arbitrary close to 1 can distinguish processes that are not bisimulation equivalent. We also show a similar result (in a slightly stronger form) for a new process relation called 2/3-bisimulation — lying strictly between that of simulation and bisimulation. Finally, the ultimately strength of the testing language is shown to identify an even stronger process relation, called probabilistic bisimulation.