Verification

Formal Verification of Complex Robotic Systems on Resource-Constrained Platforms

Software constitutes a major part of the development of robotic and autonomous systems and is critical to their successful deployment in our everyday life. Robotic software must thus run and perform as specified. Since most of these …

Petri Net Reductions for Counting Markings

We propose a method to count the number of reachable markings of a Petri net without having to enumerate these rst. The method relies on a structural reduction system that reduces the number of places and transitions of the net in …

Time-accurate Middleware for the Virtualization of Communication Protocols

Communication between devices in avionics systems must be predictable and deterministic, and data must be delivered reliably. To help the system architects comply with these requirements, network protocol standards like ARINC 429 …

Timed Formal Model and Verification of Satellite FDIR in Early Design Phase

In a previous work, we proposed an extension of the AltaRica language and tools to deal with the modelling and analysis of failures propagation in presence of timed and temporal constraints. This need is crucial in the space …

A Model-Checking Approach to Analyse Temporal Failure Propagation with AltaRica

The design of complex safety critical systems raises new technical challenges for the industry. As systems become more complex—and include more and more interacting functions—it becomes harder to evaluate the safety implications of …