Safety critical software of Meteor developed with the B formal method and the vital coded processor

The automatic train operation system for Meteor, the first driverless metro in the city of Paris, is designed to manage the traffic of the vehicles controlled automatically or manually. This automatic guideway transportation system, developed by Matra Transport International (MTI) for the transit authority in Paris (RATP), requires a very...