Untitled

Funder

Organizational Unit

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.

2022-12-05Conference object

Open access

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.

2022-06-02Journal article

Open access