MeTRiD 2018 Programme

Abstract: The ICT revolution is dominated by the IoT vision which promises increasingly interconnected smart objects providing autonomous services for the optimal management of resources and enhanced quality of life. These include smart grids, smart transport systems, smart health care services, automated banking services, smart factories, etc. Their coordination will be achieved using a unified network infrastructure, in particular to collect data and send them to the cloud which in return will provide using data analytics, intelligent services to ensure global trustworthiness and performance.

This vision raises a lot of expectations and in my opinion some over-optimism about its short-term impact.

The purpose of this talk is to discuss to what extent the IoT vision is reachable under the current state of the art, identify technical obstacles and point out work directions for overcoming them.

It is well-understood that the current network infrastructure is neither safe nor secure enough. Furthermore, it is hard to guarantee time predictability for critical events. All these make problematic the development and coordination of critical autonomous systems and services. Additional problems come from the need to integrate critical and best-effort systems and deal with heterogeneous technical requirements.

For decades critical systems engineering has relied on two pillars: the first pillar is Verification and Validation (V&V) seeking systematic and accountable exploration of models of the designed system and/or its development process; the second is the V-model of the systems engineering process demonstrating the relationships between each phase of the development life cycle and its associated phase of V&V.

These engineering principles are not any more affordable. They both need rigorous formulation of requirements as well as faithful models of the developed system and process. Writing rigorous requirements for open autonomous systems, e.g. self-driving cars, turns to be an insurmountable problem. It is very hard to understand and logically analyze rules involving not only technical but also ethical, legal and societal issues. Additionally, machine learning techniques — viewed as the key to building autonomous systems — are not developed based on requirements e.g. that specify how a dog looks different from a cat.

Consequently in absence of rigorous requirements, the application of existing V&V techniques becomes also problematic.

The application of rigorous system design techniques is currently challenged by three factors: the extended use of cyber physical components, the deployment of dynamic and reconfigurable systems that exhibit adaptive behavior, and the increasing and unmanageable uncertainty of execution and external environments.

Existing design flows for critical systems are not any more affordable in the IoT context for both technical and economic reasons. Guaranteeing statically at design time correctness of critical autonomous systems becomes impossible. We need effective design flows seeking an appropriate balance between properties guaranteed at design time and properties enforced at run time. This implies in particular that we break with the deterministic concept of correctness adopted by current critical application standards.

We advocate the design of adaptive systems that can change dynamically their behavior to cope timely and effectively with mishaps of any kind caused by design errors, failures or malevolent action. Adaptation is the capability to change system behavior in particular by reconfiguring its services and resources guided by knowledge acquired both at design time and at run time. We identify technical challenges for adaptive control achieved by combining three main functions: objective management, planning and learning.

Abstract: A major challenge that is currently faced in the design of applications for the Internet of Things (IoT) concerns with the optimal use of energy resources that are tightly coupled with the battery lifetime of the IoT devices. The challenge is derived from the heterogeneity of the devices, in terms of their hardware and the provided functionalities (e.g data processing/communication). In this paper we propose a novel method for (i) characterizing the parameters that influence energy consumption and (ii) validating the energy consumption of IoT devices against the system’s energy-efficiency requirements (e.g. lifetime). Our approach is based on energy-aware models of the IoT application’s design in the BIP (Behavior, Interaction, Priority) component framework. This allows for a detailed formal representation of the system’s behavior and its validation, thus providing feedback for enhancements in the pre-deployment or pre-production stages. We illustrate our approach through a Building Management System, using well-known IoT devices that communicate by diverse IoT protocols (e.g. CoAP, MQTT) in the Contiki OS. The results allow to derive tight bounds for the energy consumption in various device functionalities, as well as to validate lifetime requirements through Statistical Model Checking.

Abstract: This work presents a compositional approach for schedulability analysis of Distributed Integrated Modular Avionics (DIMA) systems that consist of spatially distributed ARINC-653 modules connected by a unified AFDX network. We model a DIMA system as a set of stopwatch automata in UPPAAL to verify its schedulability by model checking. However, direct model checking is infeasible due to the large state space. Therefore, we introduce the compositional analysis that checks each partition including its communication environment individually. Based on a notion of message interfaces, a number of message sender automata are built to model the environment for a partition. We define a timed selection simulation relation, which supports the construction of composite message interfaces. By using assume-guarantee reasoning, we ensure that each task meets the deadline and that communication constraints are also fulfilled globally. The approach is applied to the analysis of a concrete DIMA system.

Abstract: Usage control models provide an integration of access control, digital rights, and trust management. To achieve this integration, usage control models support additional concepts such as attribute mutability and continuity of decision. However, these concepts may introduce an additional level of complexity to the underlying model, rendering its definition a cumbersome and prone to errors process. Applying a formal verification technique allows for a rigorous analysis of the interactions amongst the components, and thus for formal guarantees in respect of the correctness of a model. In this paper, we elaborate on a case study, where we express the high-level functional model of the UseCON usage control model in the TLA+ formal specification language, and verify its correctness.

Abstract: While many studies and tools target the basic stabilizability problem of networked control systems (NCS), nowadays modern systems require more sophisticated objectives such as those expressed as formulae in linear temporal logic or as automata on infinite strings. One general technique to achieve this is based on so-called symbolic models, where complex systems are modeled using finite abstractions, and then, correct-by-construction controllers are automatically synthesized for them. We present SENSE as a tool for the construction of finite abstractions of NCS and the automated synthesis of their controllers, to enforce complex specifications over plants in NCS by taking into account several non-infidelities of the network.

Given a symbolic model of the plant and network delays, SENSE can efficiently construct a symbolic model of the NCS, by employing operations on binary decision diagrams (BDDs). Then, it synthesizes symbolic controllers satisfying a class of specifications. It has interfaces for the simulation and the visualization of the resulting closed-loop system using OMNeT++ and MATLAB. Additionally, SENSE can generate ready-to-implement VHDL/Verilog or C/C++ codes from the synthesized controllers.

Abstract: Back in 2004, while working as the Senior Software Engineer and Technical Lead of Semantix — a company I co-founded — I found myself facing a significant technical challenge: I had to figure out a way to effectively handle 7 different versions of evolving telecom protocols, while implementing more than three thousand validation rules for each one of them. Through shear luck — reading the right paper at the right time — I realized that instead of writing the code myself, I could instead create a small language to describe the logic of the validations, mergings, etc. — and then create a parser and code generator that would write the code for me.

Six months later, my code generators had created 700’000 lines of C++ code addressing all the needs for all possible versions. We released the resulting product line to the world, and it quickly became world leading — with the rather distinctive characteristic of zero bug reports; with companies all over the world using the tools constantly, processing millions of call records every day.

ESA became aware of this work through a presentation we later did on these code generators. The Agency had always been — and still is — on the lookout for ways to shield mission codebases from errors — since any one of them may lead to mission loss. The right people from ESA saw in that presentation what Semantix did, and involved my company — and me personally — in a series of projects, where TASTE was born and rapidly evolved into an ever-expanding set of closely knit model-to-model and model-to-code transformation engines.

In this talk, I will try to share with the workshop attendees what TASTE is; how it started, how it evolved into what it is today, and what it provides in terms of real-world semantics-preserving model transformations; with specific emphasis on targeting the safety-critical domains.

Abstract: Existing model-based processes for embedded real-time systems support the analysis of various non-functional properties, most notably schedulability, through model checking, simulation or other means. The analysis results are then used for modifying the system’s design, so that the expected properties are satisfied. A rigorous model-based design flow differs in that it aims at a system implementation derived from high-level models by applying a sequence of semantics-preserving transformations. Properties established at any design step are preserved throughout the subsequent steps including the executable implementation. We introduce such a design flow using a process network model of computation for application design at a high level, which combines streaming and reactive control processing with task parallelism. The schedulability of the so-called FPPNs (Fixed Priority Process Networks) is well-studied and various solutions have been presented. This article focuses on the design flow’s steps for deriving executable implementations on the BIP (Behavior – Interaction – Priority) runtime environment. FPPNs are designed using the TASTE toolset, a convenient architecture description interface. In this way, the developers do not program explicitly low-level real-time OS services and the schedulability properties are guaranteed throughout the design steps by construction. The approach has been validated on the design of a real spacecraft on-board application that has been scheduled for execution on an industrial multicore platform.

Abstract: The Behavior-Interaction-Priority (BIP) framework—rooted in rigorous semantics—allows the construction of systems that are correct-by-design. BIP has been effectively used for the construction and analysis of large systems such as robot controllers and satellite on-board software. Nevertheless, the specification of BIP models is done in a purely textual manner without any code editor support. To facilitate the specification of BIP models, we present DesignBIP, a web-based, collaborative, version-controlled design studio. To promote model scaling and reusability of BIP models, we use a graphical language for modeling parameterized BIP models with rigorous semantics. We present the various services provided by the design studio, including model editors, code editors, consistency checking mechanisms, code generators, and integration with the JavaBIP tool-set.

Abstract: Synchronisation classes are an important building block for shared memory concurrent programs. Thus to reason about such programs, it is important to be able to verify the implementation of these synchronisation classes, considering atomic operations as the synchronisation primitives on which the implementations are built. For synchronisation classes controlling exclusive access to a shared
resource, such as locks, a technique has been proposed to reason about their behaviour. This paper proposes a technique to verify implementations of both exclusive access and shared-reading synchronisers. We use permission-based Separation Logic to describe the behaviour of the main atomic operations, and the basis for our technique is formed by a specification for class AtomicInteger, which is commonly used to implement synchronisation classes in java.util.concurrent. To demonstrate the applicability of our approach, we mechanically verify the implementation of various synchronisation classes like Semaphore, CountDownLatch and Lock.

Abstract: Reo is an interaction-centric model of concurrency for compositional specification of communication and coordination protocols. Formal verification tools exist to ensure correctness and compliance of protocols specified in Reo, which can readily be (re)used in different applications, or composed into more complex protocols. Recent benchmarks show that compiling such high-level Reo specifications into executable code can compete or even beat the performance of hand-crafted programs written in languages such as C or Java using conventional concurrency constructs.

The original declarative graphical syntax of Reo does not support intuitive constructs for parameter passing, iteration, recursion, or conditional specification. This shortcoming hinders Reo’s uptake in large scale practical applications. Although a number of Reo-inspired syntax alternatives have appeared in the past, none of them follows the primary design principles of Reo: a) declarative specification; b) all channel types in Reo are user-defined; and 3) composition occurs at the level of nodes, which have predefined behavior. In this paper, we offer a textual syntax for Reo that follows respects these principles. We have used this textual syntax to compile Reo into target languages such as Java, Promela, and Maude.