Programme

Abstract: In the Confirm research centre on Smart Manufacturing as well as in Industry 4.0 in general, a Digital Thread connects the data and processes for smarter products, smarter production, and smarter integrated ecosystems. While the tangible goods (products and production lines) are understood as needing a Digital Twin as an executable model, i.e. an in-silico entity on which to virtually explore design, production, quality, and lifetime maintenance, the immaterial goods like software are not yet treated on par.

We argue that the increasingly ambitious needs of the people, the economic sectors, and the large-scale trends can only be met if the IT professions embrace and adopt a new way of producing and consuming IT. The new way to deal with software will be more mature in the sense of automation of production and management, based on more formal descriptions, more models, more reasoning and analysis before expensive implementations are incurred. Behavioural models are accordingly the natural Digital Twins of the software.

For this new paradigm to enter mainstream, models need to be coupled with automatic transformations, generations, and analyses that take advantage of the formalized knowledge about the immaterial and material entities. This formalized knowledge includes a variety of models together wit Domain Specific Languages that use semantic types at their core.

We provide a few examples of how the new thinking can disrupt the status quo but empower a better understanding, a more efficient organization, and a more automatic management of the many cross-dimensional issues that future connected software and systems will depend upon.

Abstract: Randomized fault-tolerant distributed algorithms pose a number of challenges for automated verification: (i) parameterization in the number of processes and faults, (ii) randomized choices and probabilistic properties, and (iii) an unbounded number of asynchronous rounds. The combination of these challenges makes verification hard. Challenge (i) was recently addressed in the framework of threshold automata. We extend threshold automata to model randomized algorithms that perform an unbounded number of asynchronous rounds. For non-probabilistic properties, we show that it is necessary and sufficient to verify these properties under round-rigid schedules, that is, schedules where no process enters round r before all other processes finished round r − 1. For almost-sure termination, we analyze these algorithms under round-rigid adversaries , that is, fair adversaries that only generate round-rigid schedules. This allows us to do compositional and inductive reasoning that reduces verification of the asynchronous multi-round algorithms to model checking of a one-round threshold automaton. We apply this framework to classic algorithms: Ben-Or’s and Bracha’s seminal consensus algorithms for crashes and Byzantine faults, 2-set agreement for crash faults, and RS-Bosco for the Byzantine case.

Abstract: The BIP (Behavior, Interactions, Priorities) framework is intended to the design and analysis of complex, heterogeneous embedded applications. It allows the construction of hierarchically structured models by coordinating components using highly expressive glue operators (i.e. connectors/interactions and priorities).

In this talk we first revisit previous work on glue expressiveness, and show the limitations of existing implementations of BIP with respect to both expressiveness and runtime performance. Then, we propose new notions of interactions and connectors to overcome those limitations. These new glue operators have the expressivity of the universal glue, and are much more compact for specifying data transfers. They also allow straightforward generation of efficient implementation code.

Abstract: DR-BIP is an extension of the BIP component framework intended for programming reconfigurable systems encompassing various aspects of dynamism. A system is built from instances of types of components characterized by their interfaces. The latter consist of sets of ports through which data can be exchanged when interactions take place. DR-BIP allows the description of parametric exogenous interactions and reconfiguration operations. To naturally model self-organization and mobility of components, a system is composed of several architecture motifs, each motif consisting of a set of component instances and coordination rules. The use of motifs allows a disciplined management of dynamically changing coordination rules. This presentation illustrates the basic concepts of DR-BIP through a collection of non-trivial examples from different application areas: fault-tolerant systems, mobile systems and autonomous systems. The presented solutions show that DR-BIP is both minimal and expressive allowing concise and natural description of non-trivial systems.

Abstract: This talk reflects upon 20 years long efforts of the speaker to apply model-checking based formal verification to the practice of industrial automation. These efforts were mainly happening in the academia with sporadic attempts to interact with industry.

From the very beginning the closed-loop view on the systems under verification was taken.

Early works on the application of model-checking to verification of programs date back to early 90s, and the first works on closed-loop verification appeared a few years after, in the end of 90s.

The reason behind the closed-loop approach is two-fold. First and foremost, explicit modelling of the plant enables formulation of requirements in terms of the plant’s processes which makes more sense for the automation system owner.

Another reason is that the closed-loop pattern promises lower complexity of model-checking than that of open-loop systems.

Another feature of the modern automation systems is modularity, and this feature is becoming increasingly more obvious. This requires modularization and “aspectisation” of the formal models as well, leading to the concept of cyber-physical component as an artefact used in both engineering and verification. To increase industrial applicability of this concept, we tried to rely on industrial standards for defining the input to our verification tools.

The fundamental question in the closed-loop approach is how to develop models of the plant systematically and with less effort. In recent works we explored ideas of using simulation models as a source for generating automatically discrete state models using evolutionary algorithms or other heuristics. We also tried to limit evolutions of the plant to those which the controller under verification could bring the plant to, trying to “infuse” non-determinism on a limited scale.

The talk will touch upon several techniques aiming at practical applicability of model-checking and its use by the practicing control engineers.

Abstract: Fault-localization is considered to be a very tedious and time-consuming activity in the design of complex Cyber-Physical Systems (CPS). This laborious task essentially requires expert knowledge of the system in order to discover the cause of the fault. In this context, we propose a new procedure that aids designers in debugging Simulink/Stateflow hybrid system models, guided by Signal Temporal Logic (STL) specifications. The proposed method relies on three main ingredients: (1) a monitoring and a trace diagnostics procedure that checks whether a tested behavior satisfies or violates an STL specification, localizes time segments and interfaces variables contributing to the property violations; (2) a slicing procedure that maps these observable behavior segments to the internal states and transitions of the Simulink model; and (3) a spectrum-based fault-localization method that combines the previous analysis from multiple tests to identify the internal states and/or transitions that are the most likely to explain the fault. We demonstrate the applicability of our approach on two Simulink models from the automotive and the avionics domain.

Abstract: The advances towards IoT systems with increased autonomy support improvements to existing applications and open new perspectives for other application domains. However, the design of IoT systems is challenging, due to the multiple design aspects that need to be considered. Connectivity and storage aspects are amongst the most significant ones, as IoT devices are resource-constrained and in many cases battery-powered. On top of them, it is also essential to consider privacy and security aspects that are linked to the protection the IoT system, as well as of the data exchanged through its connectivity interfaces. Ensuring security in an IoT system, though, is an evident need and a complex challenge, due to its impact in the battery lifetime. In this paper, we propose a methodology to manage energy consumption through a model-based approach for the energy characterization of IoT design aspects using the BIP (Behavior, Interaction, Priority) component framework. Our approach is exemplified based on an Intelligent Transport System (ITS) that uses Zolertia Zoul devices placed in traffic lights and road signs to broadcast environmental and road hazard information to crossing vehicles. The results allow to find a feasible design solution that respects battery lifetime and security requirements.

Abstract: This work presents a methodology for the formal modeling of security attacks on cyber-physical systems, and the analysis of their effects on the system using logic theories. We consider attacks only on sensors and actuators. A simulated attack can be triggered internally by the simulation algorithm or interactively by the user, and the effect of the attack is a set of assignments to the variables. The effects of the attacks are studied by injecting attacks in the system model and simulating them. The overall system, including the attacks, the system dynamics and the control part, is co-simulated. The INTO-CPS framework has been used for co-simulation, and the methodology is applied to the Line follower robot case study of the INTO-CPS project.