We provide EU funding and world-class technical support to engineering and technology businesses.

Find out more about who we are and what we do

Stay in Touch

EventBrite logo Twitter logo RSS logo Linked In  logo Email us

Join our mailing list

Join our mailing list to receive notification of CPSE Labs events and upcoming calls

Smart Anything Everywhere

Cyber-Physical Systems Engineering Labs is part of the Smart Anything Everywhere initiative.

This project has received funding from the European Union's Horizon 2020 research and innovation programme under grant agreement No 644400.

SafeNav (Formal Verification Applied to the Navigation of an Autonomous Shuttle)

Problem and solution

This experiment applies the GenoM3/BIP framework with the navigation stack to the autonomous shuttle EZ10:


The EZ10 is an autonomous shuttle vehicle produced by EasyMile that can transport 10 people, typically for last-mile use cases or for short travels of some kilometers in city centers, large industrial sites, etc. Safety is at the heart of such a system and there is thus a need to apply verification techniques on the software.

This experiment validates the architecture of this robotic stack, with the added benefit of making it easier to check the addition of new software components. This validation includes verifying that safety properties hold and that temporal constraints are respected.

How did CPSE Labs Help?

The benefit for Verimag is to deploy and test its formal V&V tool and approach on real systems. For EasyMile, the benefit is to test these V&V tool on their system and integrate them in their development tool chain. The experimenters were able to work together, the centre acting as a bridge through the GenoM3 technology which has one foot in the V&V world and another one in the autonomous robot one.


The V&V offline tool (RT D-Finder) was not able to deliver proof on the properties identified by EasyMile. Despite this, the run time V&V worked as expected on the EasyMiles simulation, however EasyMile found out that the type of requirements they wanted to satisfy in the near future were at a lower level of specification (more like safety bag of basic function) than the type of formal property they proposed early in the project (linked to navigation). The project was successful in demonstrating that a regular yet complex navigation system can easily be implemented in GenoM3, offering middleware independence, and synthesis of other V&V tool.


The EZ10 software is proprietary, however, we applied the same approach to the Osmosis experiment, which can be tested and we encourage users to download and experiment with it.

Design centre

This experiment is supported by our France design centre

France design centre

Technology platforms

GenoM Logo


EasyMile Logo
Verimag Logo


01 Nov 2016 - 30 Oct 2017
Funded under: CPSE Labs Call 3