Tools

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 …

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 …

Formal Verification of User-Level Real-Time Property Patterns

To ease the expression of real-time requirements, Dwyer, and then Konrad, studied a large collection of existing systems in order to identify a set of real-time property patterns covering most of the useful use cases. The goal was …