General CS Department seminar:
Wednesday, 12 December 2001, 16:15-17:15
Room: ETH, IFW A36.
,b>In addition, there will be a presentation of a B case study on the same day (just before the Department seminar) from 14:15 to 16 in E42, part of the "Trusted Components course" but open to the public.
Jean-Raymond Abrial, consultant (Marseille).
Special presentation at 14:15:
A case study in formal development
The Department seminar at 16:15 is intended for a broad audience and is an excellent way to get up to date with the progress of formal methods and their industrial applications to large systems, e.g. the security control system of the "Meteor" line of the Paris metro.
If you have any serious interest in advanced software techniques, I (BM) suggest that you also attend the earlier presentation at 14:15, which will be an excellent way to understand in more depth, on an actual example, the development of systems that are provably (and provedly) correct from start to finish.
A brief introduction to a formal method (B) and corresponding tools is presented. Recent developments in using this method with an event-like approach in sequential or distributed program development, in electronic circuit construction, as well as in more general system development is outlined.
As provided by the speaker: Pedagogue, consultant, mechanic (of proofs), bit of a mathematician.
(Comments by BM, my sole responsibility): Abrial is one of the pioneers in formal methods, the originator of Z and the developer of the B method and supporting tools, which provide one of the most practical frameworks for developing industrial systems so that they can be proved correct as part of the process. He has also made contributions to the theory of databases (Data Semantics) and to many software systems such as the Socrate database, the LTR3 language and the concurrency mechanism of Ada.