DaVinci

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.

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.

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.