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 March 2022
DaVinci Spring School
Organised by
Guillermina Cledou.
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)
Set of tools to reason about communication safety in families (or software product lines) of teams.
http://arcatools.org/feta
A light-weight and optimised framework to support the quick prototyping of formal models with operational rules, using Scala.
https://github.com/arcalab/caos
A prototypical tool to specify and analyse global communication protocols
https://github.com/arcalab/choreo
28 Apr 2021, talk at GAG Seminar, given by José Proença (video) (slides)
2 Dec 2020,
talk at ICTAC'20,
given by
José Proença and
Renato Neves.
(slides)
(paper)
28 Aug 2020,
talk at Haskell Symposium 2020,
given by
Armando Santos.
(code)
(video)
(paper)
18 June 2020
Talk at DisCoTec 2020,
given by
Guillermina Cledou and
José Proença.
(video)
(slides)
(paper)
Set of tools to analyse reactive programs inspired in Reo with synchronisation constraints.
http://arcatools.org/#arx
Set of tools to compose, analyse, and verify hubs for the RTOS VirtuosoNext™ by Altreonic.
http://arcatools.org/hubs
12 February 2020
1st DaVinci Workshop on distributed architectures for Cyber-Physical Systems, joint with the KLEE workshop.
Organised by José Proença and Luís Barbosa.
Set of tools to analyse hybrid programs using simulation based on symbolic evaluation.
(Tech. report)
http://arcatools.org/lince
7 October 2019
5th Workshop on Formal Integrated Development Environment
Co-organised by
José Proença.
Co-located with
Formal Methods 2019.
(proceedings)
20 June 2019
Talk at DisCoTec 2019,
given by
José Proença.
(slides)
(paper)
15 May 2019
Given by
prof. Farhad Arbab
(slides)
3 May 2019
Talk at FSEN 2019,
given by
José Proença.
(slides)
(paper)
2 May 2019
Talk at FSEN 2019,
given by
Leandro Gomes.
(slides)
(paper)
11 Apr 2019
Talk at CISTER's Seminar Series 2019,
given by
José Proença.
(slides)
(video)
(photos)
5 April 2019
Talk at ICEGOV 2019,
given by
Luís Soares Barbosa.
(paper)
Set of tools in the scope of the project, executable online.
http://arcatools.org
12 November 2018
Invited talk at EGOV Talks 2018,
given by
José Proença.
(slides)