Buildings are the largest energy consumers in Europe and are responsible for approximately 40% of EU energy consumption and 36% of the greenhouse gas emissions in Europe. Two-thirds of the building consumption is for residential buildings. To achieve energy efficiency, buildings are being integrated with IoT devices through the use of smart IoT services. For instance, a smart space heating service reduces energy consumption by dynamically heating apartments based on indoor and outdoor temperatures. The W3C recommends the use of the Web of Things (WoT) standard to enable IoT interoperability on the Web. However, in the context of a smart building, the ability to search and discover building metadata and IoT devices available in the WoT ecosystems remains a challenge due to the limitation of the current WoT Discovery, which only includes a directory containing only IoT devices metadata without including building metadata. Integrating the IoT device's metadata with building metadata in the same directory can provide better discovery capabilities to the IoT services providers. In this paper, we integrate building metadata into the W3C WoT Discovery through the construction of a Building Description JSON-LD file. This Building Description is integrated into the W3C WoT Discovery and based on the domOS Common Ontology (dCO) to achieve semantic interoperability in smart residential buildings for the WoT IoT ecosystem within the Horizon 2020 domOS project. This integration results in a Thing and Building Description Directory. dCO integrates the SAREF core ontology with the Thing Description ontology, devices, and building metadata. We have implemented and validated the WoT discovery on top of a WoT Thing and Building Description Directory. The WoT Discovery implementation is also made available for the WoT community.

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.

Abstract The architecture of ARINC-653 partitioned scheduling has been widely applied to avionics systems owing to its robust temporal isolation among applications. However, this partitioning mechanism causes the problem of how to optimize the partition scheduling of a complex system while guaranteeing its schedulability. In this paper, a model-based optimization approach is proposed. We formulate the problem as a parameter sweep application, which searches for the optimal partition scheduling parameters with respect to minimum processor occupancy via an evolutionary algorithm. An ARINC-653 partitioned scheduling system is modeled as a set of timed automata in the model checker UPPAAL. The optimizer tentatively assigns parameter settings to the models and subsequently invokes UPPAAL to verify schedulability as well as evaluate promising solutions. The parameter space is explored with an evolutionary algorithm that combines refined genetic operators and the self-adaptation of evolution strategies. The experimental results show the applicability of our optimization method.

Traditionally, the development workflow of Arrow-head 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.

Efficient and effective verification and validation of complex embedded systems is challenging, and requires the use of various tools and techniques, such as model-based testing and analysis. The aim of this paper is to devise an overall \method{} for how analysis and testing may be used in combination to increase the quality of embedded systems, and reduce development cost. The method is centered on a common verification planning and iteratively exploiting the established results to strengthen the verification activities. We conclude that the proposed method is general enough to capture most interesting combinations and workflows, but also that formulation of more specific combination patterns will be useful to encourage future tool collaborations.

We propose an automated, tool-supported approach to scenario-based analysis and synthesis of real-time embedded systems. The inter-object behaviors of a system are modeled as a set of live sequence charts (LSCs), and the scenario-based user requirement is specified as a separate LSC. By translating the set of LSC charts into a behavior-equivalent network of timed automata (TA), we reduce the problems of model consistency checking and property verification to classical CTL real-time model checking problems, and reduce the problem of centralized synthesis for open systems to a timed game solving problem. We implement a prototype LSC-to-TA translator, which can be linked to existing real-time model checker UPPAAL and timed game solver UPPAAL-TIGA. Preliminary experiments on a number of examples show that it is a viable approach.

This paper studies the problem of model-based testing of real-time systems that are only partially observable. We model the system under test (SUT) using timed game automata (TGA) which has internal actions, uncontrollable outputs and timing uncertainty of outputs. We define the partial observability of SUT using a set of predicates over the TGA state space, and specify the test purposes in computation tree logic (CTL) formulas. A developed partially observable timed game solver is used to generate winning strategies, which are used as test cases. We propose a conformance testing framework, define a partial observation-based conformance relation, present the test execution algorithms, and prove the soundness and completeness of this test method (i.e., a detected error really violates the conformance relation; and if the SUT violates the test purpose, then a test case can be generated to detect this violation). Experiments on some non-trivial examples show that this method yields encouraging results.

This paper presents a game-theoretic approach to the testing of uncontrollable real-time systems. By modelling the systems with timed I/O game automata and specifying the test purposes as Timed CTL formulas, we employ a recently developed timed game solver UPPAAL-TIGA to synthesize winning strategies, and then use these strategies to conduct black-box conformance testing of the systems. The testing process is proved to be sound and complete with respect to the given test purposes. Case study and preliminary experimental results indicate that this is a viable approach to uncontrollable timed system testing.

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.

We present a coordination language and its semantics for specification and implementation of object-oriented real-time systems. Real-time systems operate under real-time constraints, and our language supports expression thereof. In our language, a system is modeled by two separate but complementary descriptions: A collection of objects define the system's structure and functional behavior and a set of interaction constraints define how these objects may interact. Our language thereby supports development of real-time systems by enabling objects build in isolation or re-used from other systems to be composed via interaction constraints. We use the Actor model to describe objects and the concept of real-time synchronizers to describe interaction constraints. Our model is accompanied by a formal semantics that precisely defines what real-time constraints means, and what constitutes a program's correct real-time behaviors. The semantics defines how the system may evolve in the real-time domain, and what progress guarantees the language makes. We briefly discuss implementation problems and potential solutions.