Experiments with Formal Specifications on MAGGALY

Until lately, safety functions for automatic train driving systems have mostly been implemented with classical techniques such as relays, way circuitry and, more recently, electronic devices. By now, microprocessors are being massively introduced into very high safety level transportation systems. While (in the French systems) hardware safety is ensured by the use of a coded monoprocessor, software safety can be reached by rigorous development and validation methods. We present here an experiment on the development and use of formal specifications on the on board software of Lyon's unmanned subway MAGGALY, using the PLUSS modular algebraic specification language. This experiment was done in parallel with and independently of the actual industrial development. Our specification is executable and has been used as a prototype of the system, thus allowing a validation of the specification against the user's needs. It is also used to generate test data sets for the system. Logic programming with constraints is used to derive relevant testing values from the axioms of the specification.