Project Summary - 2018-2021

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:

  1. how to specify and verify interaction patterns between large component-based systems with a plethora of devices, sensors, and actuators, taking into account aspects such as continuous behaviour, modularity, and failure, and
  2. how to derive efficient and trustworthy implementations that realise the abstractions for interactions between components.

To address these questions, the main contributions of this project will be:

  1. to develop a paradigm, encompassing foundations, software engineering methods and techniques, to reason about distributed reactive systems in the large, with strong fundamentals grounded on real-time models, dynamic logics, and relational algebra;
  2. to allow the safe reusability of (distributed) software product lines with continuous behaviour, i.e. of software components and connectors with configuration parameters, considering both discrete and continuous time;
  3. to provide a set of tools that will allow these results to be transferred to interested industrial partners and other academics, grounded on the Reo coordination language.

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.


Tasks

  1. Formal Models for Distributed Families
    (months: 1-24; Grants: MSc-8)
    • Hybrid components – multi-party consensus of continuous functions
    • Real-time behaviour – time constraints to model and verify interactions
    • Variability – using a calculus and (dynamic) logics
    • Probabilities – probabilistic state machines or enriched connector calculus
  2. Distribution of Families of Reactive Systems
    (months: 12-36; Grants: Lic-3, MSc-6)
    • DSL's for large systems with unreliable communication
    • Minimising number of components involved in interactions at runtime
    • Eventual consistency of continuously-evolving variables
  3. Framework for interactive and variable components
    (months: 7-36; Grants: Lic-6, MSc-7)
    • Framework for interactive and variable components
    • Use of web-based technologies
  4. Case-study: Remote Wireless Steering with Kurt
    (months: 7-36; Grants: Lic-3, MSc-3)
    • KURT electric city-vehicles
    • Based on a modular, scalable and fault tolerant architecture
    • Analyse components with continuous behaviour
    • Unreliable network to remotely steers the vehicles

Grants

  • Master student (19/20)
    • Runtime monitoring of continuous properties
  • Master student (20/21)
    • 3rd party extensions to the framework motivated by the case-study
  • PhD student (Feb 20 - Jan 21)
    • Development of models for visually analyse and simulate variable connectors
  • PhD student (Sep 19 - Aug 20)
    • A monadic calculus of connectors with probabilities

Work Plan


Team

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.


Publications

  • , [], (journal) (conference) (book chapter) (technical report) (PhD thesis) (MSc thesis) download
  • (),

    , , , Supervised by ,


Dissemination

Organisation of DaVinci Spring School

24-25 March 2022
DaVinci Spring School
Organised by Guillermina Cledou.

Organisation of the F-IDE workshop

24-25 May 2021
6th Workshop on Formal Integrated Development Environment
Co-organised by José Proença.
Co-located with NASA Formal Methods 2021.
(proceedings)

fETA - Featured Team Automata

Set of tools to reason about communication safety in families (or software product lines) of teams.
http://arcatools.org/feta

CAOS - Computer Aided Operational Semantics

A light-weight and optimised framework to support the quick prototyping of formal models with operational rules, using Scala.
https://github.com/arcalab/caos

Choreo - choreographies with strong choice and loops

A prototypical tool to specify and analyse global communication protocols
https://github.com/arcalab/choreo

Lince - programming with differential equations

28 Apr 2021, talk at GAG Seminar, given by José Proença (video) (slides)

Implementing Hybrid Semantics: From Functional to Imperative

2 Dec 2020, talk at ICTAC'20, given by José Proença and Renato Neves.
(slides) (paper)

Type Your Matrices for Great Good: A Haskell Library of Typed Matrices and Applications (Functional Pearl)

28 Aug 2020, talk at Haskell Symposium 2020, given by Armando Santos.
(code) (video) (paper)

ARx - Reactive Programming for Synchronous Connectors

18 June 2020
Talk at DisCoTec 2020, given by Guillermina Cledou and José Proença.
(video) (slides) (paper)

ARx - Reactive Programming for Synchronous Architectures

Set of tools to analyse reactive programs inspired in Reo with synchronisation constraints.
http://arcatools.org/#arx

Hubs - composing and analysing hubs for VirtuosoNext™

Set of tools to compose, analyse, and verify hubs for the RTOS VirtuosoNext™ by Altreonic.
http://arcatools.org/hubs

Lince - analysis of hybrid programs

Set of tools to analyse hybrid programs using simulation based on symbolic evaluation.
(Tech. report)
http://arcatools.org/lince

Organisation of the F-IDE workshop

7 October 2019
5th Workshop on Formal Integrated Development Environment
Co-organised by José Proença.
Co-located with Formal Methods 2019.
(proceedings)

Coordination of Tasks on a Real-Time OS

20 June 2019
Talk at DisCoTec 2019, given by José Proença.
(slides) (paper)

Invited tutorial on Interaction-Based Programming

15 May 2019
Given by prof. Farhad Arbab (slides)

Taiming Hierarchical Connectors

3 May 2019
Talk at FSEN 2019, given by José Proença.
(slides) (paper)

Logics for Petri nets with propagating failures

2 May 2019
Talk at FSEN 2019, given by Leandro Gomes.
(slides) (paper)

The Interaction-Based Paradigm

11 Apr 2019
Talk at CISTER's Seminar Series 2019, given by José Proença.
(slides) (video) (photos)

Deep Learning Powered Question-Answering Framework for Organizations Digital Transformation

5 April 2019
Talk at ICEGOV 2019, given by Luís Soares Barbosa.
(paper)

ArcaTools - web-based tools

Set of tools in the scope of the project, executable online.
http://arcatools.org

Project DaVinci: managing interactions in cyber-physical systems

12 November 2018
Invited talk at EGOV Talks 2018, given by José Proença.
(slides)


Statistics

Artefacts (middle), milestones of each tasks to which they contribute (left), and type of artefact (right).
Artefacts by year, organised by type
Artefacts by venue.

Related Projects


This work is financed by the ERDF – European Regional Development Fund through the Operational Programme for Competitiveness and Internationalisation - COMPETE 2020 Programme (project POCI-01-0145-FEDER-029946) and by National Funds through the Portuguese funding agency, FCT - Fundação para a Ciência e a Tecnologia (project PTDC/CCI-COM/29946/2017).

Back to top