Success Stories in Formal Methods

Seminar in Theoretical CS, Winter Semester 2012/13

News

  • 27.08.2012: Setup of this web page


Schedule

Tue Jan 15, 2013, afternoon   Seminar talks 

Overview

The general term formal methods refers to rigorous, mathematically based techniques for the specification, development and verification of software and hardware systems. The use of such methods is motivated by the expectation that it will improve the correctness, reliability and robustness of the system under development. Formal methods can be classified according to the phase of the system design process in which they are employed (specification, development, verification, testing, ...) or to the underlying mathematical theories (process algebras, model checking, theorem proving, ...).

 

The goal of this seminar is to study some real-world case studies in which formal methods have successfully been applied. These examples are taken from several domains, such as traffic control, communication protocols, computer operating systems, and others.


Topics

  1. Air Traffic Control: Hall, A.; Isaac, D.; Formal methods in a real air traffic control project, IEEE Colloquium on Software in Air Traffic Control Systems - The Future, pp. 7/1-7/4, June 1992
  2. Needham-Schroeder Public-Key Protocol: G. Lowe: Breaking and Fixing the Needham-Schroeder Public-Key Protocol  using FDR, TACAS 1996, LNCS 1055, 1996, 147-166
  3. Paris Metro: Patrick Behm, Paul Benoit, Alain Faivre and Jean-Marc Meynadier: Météor: A Successful Application of B in a Large Project, Formal Methods (FM'99), LNCS 1708, 1999, 369-387
  4. Mobile Communication Protocol: M.A. Fecko, M.Ü. Uyar, P.D. Amer, A.S. Sethi, T. Dzik, R. Menell, M. McMahon, A success story of formal description techniques: Estelle specification and test generation for MIL-STD 188-220, Computer Communications, Volume 23, Issue 12, July 2000, Pages 1196-1213
  5. Mars Rover: Brat, G.; Drusinsky, D.; Giannakopoulou, D.; Goldberg, A.; Havelund, K.; Lowry, M.; Pasareanu, C.; Venet, A.; Visser, W.; Washington, R.: Experimental Evaluation of Verification and Validation Tools on Martian Rover Software, Form. Methods Syst. Des. 25(2-3), 2004, 167-198
  6. Railway Signaling: Bacherini, S.; Fantechi, A.; Tempestini, M.; Zingoni, N.: A Story About Formal Methods Adoption by a Railway Signaling Manufacturer, FM 2006: Formal Methods, LNCS 4085, 2006, 179-187
  7. Real-Time Operating System: Verhulst, Eric and De Jong, Gjalt: OpenComRTOS: an ultra-small network centric embedded RTOS designed using formal modeling, Proceedings of the 13th international SDL Forum conference on Design for dependable systems, LNCS 4745, 2007, 258-271
  8. San Juan Metro: Leuschel, Michael and Falampin, Jérôme and Fritz, Fabian and Plagge, Daniel: Automated Property Verification for Large Scale B Models, FM 2009: Formal Methods, LNCS 5850, 2009, 708-723
  9. New York Subway: Sabatier, Denis and Burdy, Lilian and Requet, Antoine and Guéry, Jérôme: Formal Proofs for the NYCT Line 7 (Flushing) Modernization Project, Abstract State Machines, Alloy, B, VDM, and Z, LNCS 7316, 2012, 369-372
  10. Rotterdam Storm Surge Barrier: Ken Madlener, Sjaak Smetsers and Marko van Eekelen: A Formal Verification Study on the Rotterdam Storm Surge Barrier, Formal Methods and Software Engineering, LNCS 6447, 2010, 287-302
  11. Operating System Kernel: Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood: seL4: Formal verification of an operating system kernel, Communications of the ACM, 53(6), 2010, 107–115


Additional Material


Contact

Thomas Noll <noll at cs.rwth-aachen.de>