Re: European train deaths

["Jean-Pierre Rosen" <rosen@adalog.fr>]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 1366 bytes --]


"Colin Paul Gloster" <Colin_Paul_Gloster@ACM.org> a �crit dans le message news: slrn9eiqb9.58t8.Colin_Paul_Gloster@tolka.dcu.ie...
> Something which occured to me only yesterday (unless I cleanly
> forgot before) is that Ada and formal methods are used for
> European train systems and so these may be involved in some
> of the spate of fatal crashes over the last circa two years
> in the U.K.; Norway; and elsewhere in the E.U.. At least one
> in the U.K. had to do with a light signalling error if
> memory serves correctly but I do not recall if this had
> anything to do with software. It may be worthwhile to investigate this --
> would any of ye happen to remember if computers were involved in these
> locomotive incidents?
>
I can confirm that no Ada nor formal methods were involved in the UK crashes (don't know for Norway, but it is highly unlikely).
AFAIK, the first attempt to use formal methods and Ada was for Meteor, the new automated subway line of the Parisian subway. Safety
critical software was coded and proven in B, then automatically translated to Ada. Less critical parts were directly coded in Ada.
And I heard from trustable sources that software integration went remarkably well.

--
---------------------------------------------------------
           J-P. Rosen (rosen@adalog.fr)
Visit Adalog's web site at http://www.adalog.fr