Loading...
Research Project
Untitled
Funder
Authors
Publications
MARS: a toolset for the safe and secure deployment of heterogeneous distributed systems
Publication . Nandi, Giann; Pereira, David; Proenca, José; Santos, José; Rodrigues, Lourenço A.; Lourenço, André; Tovar, Eduardo
This work discusses the ongoing development of a toolset named MARS aimed to ease the process of safely
deploying runtime verification monitors into distributed micro-ROS and ROS2 nodes. The work is motivated by a
use case in the health and automotive domains and covers safety/security concerns around the manipulation of
sensitive biometric data.
Verification of multiple models of a safetycritical motor controller in railway systems
Publication . Proenca, José; Borrami, Sina; Nova, Jorge Sanchez de; Pereira, David; Spilere Nandi, Giann
Motor controllers, such as the ones used in signalling systems, include critical embedded software. Alstom is a company that produces such embedded systems, which must follow complex certification processes that require formal modelling and analysis. The formal analysis of these real-time systems have to balance between including enough details to be useful and abstracting away enough details to be verifiable.
This paper describes our work in the context of the European VALU3S project to integrate the analysis of such systems with the Uppaal model checker during the development cycle, involving both developers from Alstom and academic partners. We use special Excel tables to configure the underlying Uppaal models and requirements, bridging these two stakeholders. We follow Software Product Line Engineering principles, e.g., allowing features to be turned on and off and periodicities to be changed, and verify different properties for each of such configuration. We automate the instantiation and verification in Uppaal of a set of selected configurations via an open-source prototype tool named Uppex.
Organizational Units
Description
Keywords
Contributors
Funders
Funding agency
Fundação para a Ciência e a Tecnologia
Funding programme
3599-PPCDT
Funding Award Number
ECSEL/0016/2019