Distributed software systems are becoming more and more integrated with our daily lives. This ongoing trend is particularly visible in Cyber Physical Systems (CPS) - networks of cooperating computational devices such as mobiles, sensors, and actuators that bridge ICT processes and the physical world. These networks are usually characterised by (1) their large number of nodes, (2) an extra uncertainty and mobility in the connections, and (3) the interplay between continuous sending of sensor values or movement and the discrete events at precise moments in time.
In these scenarios it is crucial to identify software abstractions for the interactions between distributed components, services, nodes, or devices, that can guide how to cost-effectively develop, manage, and verify Cyber Physical Systems. Within this scope, the key questions addressed by this project concern:
To address these questions, the main contributions of this project will be:
A concrete case-study will be provided by Altreonic, a Belgian company that develops tools and engineering services for trustworthy embedded systems, with especial attention to scalability, distributed operation, high reliability and real- time. This case-study will address the steering of their modular electric city-vehicles - KURT vehicles - from a remote location.
The project is coordinated at HASLab INESC-TEC, University of Minho. It also counts with the participation of external members from CWI/Leiden University, from SRI International, and from the company Altreonic.
Set of tools in the scope of the project, executable online.
ArcaTools is a framework to bring to the web a collection of tools, decreasing the time to start experimenting with existing tools, while exploiting the interactivity and visualisation capabilities of existing web technologies. Developed mainly by members of ARCA.
All tools follow the following approach:
The key projects are:
Programming language constructs and abstractions, along with techniques for their efficient compilation, have dramatically advanced in the last half-century, to the extent that today we can program at the level of (parametric) types, classes, objects, mathematical functions, monads, or Horn clauses, when appropriate, and obtain executable code whose performance competes with–indeed often beats–that of code written by competent programmers in some low-level language. In contrast to advances in abstractions and constructs for sequential programming, no real abstract protocol constructs have evolved. Consequently, programmers today use the same cumbersome, error-prone concurrency constructs to express protocols in modern software as they did 50 years ago: processes, threads, locks, semaphores, monitors, rendezvous, etc. The unavailability of high-level protocol constructs in contemporary programming languages hampers full utilization of the enormous potential offered by massively parallel hardware platforms in real-life applications.
We describe an interaction-centric model of concurrency that turns interaction protocols into concrete first-class mathematical objects, expressed as relations that constrain communication actions of their engaged processes. This model serves as the formal foundation for a domain-specific language, called Reo, for programming concurrency protocols. A protocol in Reo manifests itself as a connector. Complex connectors result from direct composition of simpler ones, which in turn comprise of a network of primitive binary connectors, called channels. In Reo, interaction protocols become explicit, concrete, tangible pieces of software that can be specified, verified, composed, and reused, independently of the actors that they may engage in various applications. Using Reo for concurrent programming not only has significant software engineering advantages, such as modularity, compositionality, verifiability, scalability, and verbatim reuse, it also allows novel, high-level optimizations that result in efficient executable code on multicore platforms. We explore different formal semantics of Reo, its various software development support tools, and discuss compilation and optimization techniques for generating efficient executable code from high-level protocol specifications in Reo.
While abstractions and constructs for sequencial languages have dramatically advanced since the early ages of computer science, programming concurrent programs relies on the same fundamental concepts for the last 50 years. These include processes, threads, locks, semaphores, monitors, rendezvous, etc. This talk will provide insights on a paradigm that regards interactions as first-class mathematical objects, expressed as relations that constrain communication ports of cooperating processes.
I will present the Reo coordination model - a formal domain-specific language for this interaction-based paradigm, used for programming concurrency protocols. These protocols take the form of Reo connectors, built compositionally, that can be specified, verified, composed, and reused, independently of the actors being coordinated. I will describe the visual syntax of connectors and some of its semantic models, and I will highlight some of my recent contributions to this community, including a compositional real-time semantics, a variability calculus, and tools to analyse connectors.
Will take place on 7 October 2019
5th Workshop on Formal Integrated Development Environment
VirtuosoNextTM is a distributed real-time operating system (RTOS) developed and supported by Altreonic NV – an embedded technology focused company. The RTOS finds its origins in Hoare’s CSP process algebra and offers a more generic programming model dubbed Interacting Entities. This paper focuses on these interactions, implemented as so-called Hubs. Hubs act as synchronisation and communication mechanisms between the application tasks and implement the services provided by the kernel as a kind of Guarded Protected Action with a well defined semantics. As in any RTOS, having a predictable behaviour in time is crucial. While the kernel provides the most basic services, each carefully designed, tested and optimised, tasks are limited to this handful of basic hubs, leaving the development of more complex synchronization and communication mechanisms up to application specific implementations. In this work we investigate how to support a programming paradigm to compositionally build new services, using notions borrowed from the Reo coordination language, and relieving tasks from coordination aspects while delegating them to the hubs. We formalise the semantics of hubs using an automata model, identify the behaviour of existing hubs, and propose an approach to build new hubs by composing simpler ones. We also provide tools and methods to analyse and simplify hubs under our automata interpretation. In a first experiment several hub interactions are combined into a single more complex hub, which raises the level of abstraction and contributes to a higher productivity for the programmer. Finally, we investigate the impact on the performance by comparing different implementations on an embedded board.
Petri nets play a central role in the formal modelling of a wide range of complex systems and scenarios. Their ability to handle with both concurrency and resource awareness justifies their spread in the current formal development practices. On the logic side, Dynamic Logics are widely accepted as the de facto formalisms to reason about computational systems. However, as usual, the application to new situations raises new challenges and issues. The ubiquity of failures in the execution of current systems, interpreted in these models as triggered events that are not followed by the corresponding transition, entails not only the adjustment of these structures to deal with this reality, but also the introduction of new logics adequate to this emerging phenomenon. This paper contributes to this challenge by exploring a combination of two previous works of the authors, namely the Propositional Dynamic Logic for Petri Nets and a parametric construction of multi-valued dynamic logics. This exercise results in a new family of Dynamic Logics for Petri Nets suitable to deal with firing failures.
Building and maintaining complex systems requires good software engineering practices, including code modularity and reuse. The same applies in the context of coordination of complex component-based systems. This paper investigates how to verify properties of complex coordination patterns built hierarchically, i.e., built from composing blocks that are in turn built from smaller blocks. Most existing approaches to verify properties flatten these hierarchical models before the verification process, losing the hierarchical structure. We propose an approach to verify hierarchical models using containers as actions; more concretely, containers interacting with their neighbours. We present a dynamic modal logic tailored for hierarchical connectors, using Reo and Petri Nets to illustrate our approach. We realise our approach via a prototype implementation available online to verify hierarchical Reo connectors, encoding connectors and formulas into mCRL2 specifications and formulas.
In the context of digital transformation by governments, the public sector and other organizations, many information is moving to digital platforms. Chatbots and similar question answering systems are becoming popular to answer information queries, opposed to browsing online repositories or webpages. State-of-the-art approaches for these systems may be laborious to implement, hard to train and maintain, and also require a high level of expertise. This work explores the definition of a generic framework to systematically build question-answering systems. A sandbox implementation of this framework enables the deployment of turnkey systems, directly from already existing collections of documents. These systems can then be used to provide a question-answering system communication channel to enrich the organization digital presence.
Secure Runtime Verification for Reliable Real-Time Embedded Software
Coalgebraic Modeling and Analysis for Computational Synthetic Biology.
Dynamic logics for cyber-physical systems: towards contract based design.