ComputingComputer EngineeringComputer ScienceEmbedded SystemsFormal MethodsSoftware EngineeringDeductive VerificationSafety ValidationSoftware ValidationVerificationControl System ValidationEmbedded System ValidationEmbedded System VerificationFormal SpecificationsSafe System DesignSafety System ValidationSafety Verification And ValidationSystem 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.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">></ETX>