SACEM software validation

The authors report on the software validation process for SACEM, a partly embedded system (hard and soft) which continuously controls the speed of all trains on the RER Line A in Paris. Modern techniques have been used for validation, including formal specification, assertions, and formal proofs. About 100 man-years have been spent in validating the software. The authors conclude that a safe system has been realized and that all the formal work was useful, essentially to make the specifications more precise.<
>