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.
24-25 May 2021
6th Workshop on Formal Integrated Development Environment
Co-organised by José Proença.
Co-located with NASA Formal Methods 2021.
Set of tools to reason about communication safety in families (or software product lines) of teams.
A light-weight and optimised framework to support the quick prototyping of formal models with operational rules, using Scala.
A prototypical tool to specify and analyse global communication protocols
Lince provides a set of online tools to simulate and analyse hybrid programs, which are simple c-like programs where some variables can sometimes evolve according to a system of differential equations. You can experiment with it in http://arcatools.org/lince, or you can download it and run it locally.
This talk provides an overview of how to use Lince, and lists possible challenges that could be pursued by BSc or MSc students.
Hybrid programs combine digital control with differential equations, and naturally appear in a wide range of application domains, from biology and control theory to real-time software engineering. The entanglement of discrete and continuous behaviour inherent to such programs goes beyond the established computer science foundations, producing challenges related to e.g. infinite iteration and combination of hybrid behaviour with other effects. A systematic treatment of hybridness as a dedicated computational effect has emerged recently. In particular, a generic idealized functional language HybCore with a sound and adequate operational semantics has been proposed. The latter semantics however did not provide hints to implementing HybCore as a runnable language, suitable for hybrid system simulation (e.g. the semantics features rules with uncountably many premises). We introduce an imperative counterpart of HybCore, whose semantics is simpler and runnable, and yet intimately related with the semantics of HybCore at the level of hybrid monads. We then establish a corresponding soundness and adequacy theorem. To attest that the resulting semantics can serve as a firm basis for the implementation of typical tools of programming oriented to the hybrid domain, we present a web-based prototype implementation to evaluate and inspect hybrid programs, in the spirit of GHCi for Haskell and UTop for OCaml. The major asset of our implementation is that it formally follows the operational semantic rules.
We study a simple inductive data type for representing correct- by-construction matrices. Despite its simplicity, it can be used to implement matrix-manipulation algorithms efficiently and safely, performing in some cases faster than existing alternatives even though the algorithms are written in a direct and purely functional style. A rich collection of laws makes it possible to derive and optimise these algorithms using equational reasoning, avoiding the notorious off-by-one indexing errors when fiddling with matrix dimensions. We demonstrate the usefulness of the data type on several examples, and highlight connections to related topics in category theory.
Reactive programming (RP) languages and Synchronous Coordination (SC) languages share the goal of orchestrating the execution of computational tasks, by imposing dependencies on their execution order and controlling how they share data. RP is often implemented as libraries for existing programming languages, lifting operations over values to operations over streams of values, and providing efficient solutions to manage how updates to such streams trigger reactions, i.e., the execution of dependent tasks. SC is often implemented as a standalone formalism to specify existing component-based architectures, used to analyse, verify, transform, or generate code. These two approaches target different audiences, and it is non-trivial to combine the programming style of RP with the expressive power of synchronous languages.
This paper proposes a lightweight programming language to describe component-based Architectures for Reactive systems, dubbed ARx, which blends concepts from RP and SC, mainly inspired to the Reo coordination language and its composition operation, and with tailored constructs for reactive programs such as the ones found in ReScala. ARx is enriched with a type system and with algebraic data types, and has a reactive semantics inspired in RP. We provide typical examples from both the RP and SC literature, illustrate how these can be captured by the proposed language, and describe a web-based prototype tool to edit, parse, and type check programs, and to animate their semantics.
Set of tools to analyse reactive programs inspired in Reo with synchronisation constraints.
Set of tools to compose, analyse, and verify hubs for the RTOS VirtuosoNext™ by Altreonic.
7 October 2019
5th Workshop on Formal Integrated Development Environment
Co-organised by José Proença.
Co-located with Formal Methods 2019.
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.
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.
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.
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.
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.
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.
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:
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.