Colored Petri nets offer a compact and user friendly representation of the traditional Place/Transition (P/T) nets and colored nets with finite color ranges can be unfolded into the underlying P/T nets, however, at the expense of an exponential explosion in size. We present two novel techniques based on static analysis in order to reduce the size of unfolded colored nets. The first method identifies colors that behave equivalently and groups them into equivalence classes, potentially reducing the number of used colors. The second method overapproximates the sets of colors that can appear in places and excludes colors that can never be present in a given place. Both methods are complementary and the combined approach allows us to significantly reduce the size of multiple colored Petri nets from the Model Checking Contest benchmark. We compare the performance of our unfolder with state-of-the-art techniques implemented in the tools MCC, Spike and ITS-Tools, and while our approach is competitive w.r.t. unfolding time, it also outperforms the existing approaches both in the size of unfolded nets as well as in the number of answered model checking queries from the 2021 Model Checking Contest.

Colored Petri nets offer a compact and user friendly representation of the traditional P/T nets and colored nets with finite color ranges can be unfolded into the underlying P/T nets, however, at the expense of an exponential explosion in size. We present two novel techniques based on static analyses in order to reduce the size of unfolded colored nets. The first method identifies colors that behave equivalently and groups them into equivalence classes, potentially reducing the number of used colors. The second method overapproximates the sets of colors that can appear in places and excludes colors that can never be present in a given place. Both methods are complementary and the combined approach allows us to significantly reduce the size of multiple colored Petri nets from the Model Checking Contest benchmark. We compare the performance of our unfolder with state-of-the-art techniques implemented in the tools MCC, Spike and ITS-Tools, and while our approach remains competitive w.r.t. unfolding time, it outperforms the existing approaches both in the size of unfolded nets as well as in the number of answered model checking queries from the 2020 Model Checking Contest.

Modern navigation systems warn the user of traffic jams ahead and suggest alternative routes. However, a lemming effect can cause the alternative routes also to become congested, as the system suggests the same route to all users. As such, in an attempt to optimize for the individual driver, the welfare of the traffic network is punished. In this paper we introduce an online and proactive method for collective rerouting recommendations based on real-time data and stochastic optimization. Our system periodically monitors the status of the network to identify potentially congested roads together with vehicles affected by them. The system then uses Uppaal Stratego to perform machine learning and approximate the best rerouting scenarios. As a proof of concept, we build a SUMO model of a representative traffic network. We perform exhaustive experiments considering different traffic loads and different traffic light controllers. Our results are promising, showing considerable improvement in travel times, queue lengths, and CO2 emissions.

Traditionally, the development workflow of Arrowhead applications is based on the usage of source code skeletons. This makes it difficult to update applications when the skeletons are changed, for example to fix security vulnerabilities or add new functionality. In fact, to update an application the developer has to either recreate the application on the new skeleton version or recreate the skeleton changes on the previous version of the application. Instead, we propose a client library, which allows the developers to create Arrowhead applications by referring to a library. Not only does this allow the Arrowhead Consortium to update the library without requiring changes to applications, it also eases the creation of new Arrowhead applications, reduces code duplication and increases readability. This paper describes the design and the structure of this client library, provides insights on how to employ the library in applications, and surveys a few sample applications that use the library.

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

This paper presents an offline approach to analyzing feature interactions in embedded systems. The approach consists of a systematic process to gather the necessary information about system components and their models. The model is first specified in terms of predicates, before being refined to timed automata. The consistency of the model is verified at different development stages, and the correct linkage between the predicates and their semantic model is checked. The approach is illustrated on a use case from home automation.

Defining control scenarios in a smart home is a difficult task for end users. In particular, one concern is that user-defined scenarios could lead to unsafe or undesired state of the system. To help them explore scenario specifications, we propose in this paper a system that enables specification of constraints restricting the control commands that can be used inside user-defined scenarios. The system is based on timed automata model checking abstracted by event condition action rules. A prototype was implemented, including a user interface to interact with the user. The usability of the system and interface was evaluated in a user study which results are reported here.

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.

This paper presents a method to check for feature interactions in a system assembled from independently developed concurrent processes as found in many reactive systems. The method combines and refines existing definitions and adds a set of activities. The activities describe how to populate the definitions with models to ensure that all interactions are captured. The method is illustrated on a home automation example with model checking as analysis tool. In particular, the modelling formalism is timed automata and the analysis uses Uppaal to find interactions.

We present the objectives, activities and some preliminary results of the FP7 STREP project INTrEPID (INTelligent systems for Energy Prosumer buildIngs at District level).

Home Automation systems provide a large number of devices to control diverse appliances. Taking advantage of this diversity to create efficient and intelligent environments requires well designed, validated, and implemented controllers. However, designing and deploying such controllers is a complex and error prone process. This paper presents a tool chain that transforms a design in the form of communicating state machines to an executable controller that interfaces to appliances through a service oriented middleware. Design and validation is supported by integrated model checking and simulation facilities. This is extendable to controller synthesis. This tool chain is implemented, and we provide different examples to show its usability.