Institute of Information Science, Academia Sinica



Press Ctrl+P to print from browser


Formal Methods in Industry (Z, B and Event-B): an Historical Perspective

  • LecturerDr. Jean-Raymond Abrial (Independent Consultant, Marseille, France)
    Host: Dr. Tyng-Ruey Chuang
  • Time2010-08-23 (Mon.) 11:00 – 12:00
  • LocationAuditorium 106 at new IIS Building
Abstract: I will present the evolution in concepts, tools, and presence in Industry for the various formal methods Z, B, and Event-B. Before that, I will review what I think is important in Formal Methods and why they should be used in Industry. I will mention the technical difficulties in spreading them resulting in some necessary efforts to be pursued in the future in research and teaching as well. Bio: Jean-Raymond Abrial Date of birth: November 6 1938 Place of birth: Versailles, France Status: separated Nationality: French Address: 11 rue Chateauredon 13001 Marseille France Email: Employment From June 2009 Independent Consultant, Marseille, France February 2008 to May 2009 Researcher, ETH Zurich Switzerland April 2004 to August 2007 Guest Professor, ETH Zurich Switzerland 1976 - 2004 Independent Consultant, Paris 1979 - 1981 Researcher, Oxford University, UK 1976 - 1978 Independent Consultant, Paris 1974 - 1975 Researcher, INRIA, Paris 1968 - 1973 Researcher, Grenoble University, France 1964 - 1967 French Navy, Paris Education 1958-1960 Ecole Polytechnique, Paris. 1961-1963 Ecole Nationale Superieure du Genie Maritime, Paris 1965-1966 Master of Science, Stanford University, California Selected Publications 1.Jean-Raymond Abrial: Modeling in Event-B: System and Software Engineering. To be published by Cambridge University Press 2010 2. Jean-Raymond Abrial: A System Development Process with Event-B and the Rodin Platform. ICFEM 2007: 1-3 3.Jean-Raymond Abrial, Stefan Hallerstede: Refinement, Decomposition, And Instantiation of Discrete Models: Application to Event-B. Fundam. Inform. 77(1-2): 1-28 (2007) 4. Gary T. Leavens, Jean-Raymond Abrial, Don S. Batory, Michael Butler, Alessandro Coglio, Kathi Fisler, Eric C. R. Hehner, Cliff B. Jones, DaleMiller, Simon L. Peyton Jones, Murali Sitaraman, Douglas R. Smith, Aaron Stump: Roadmap for enhanced languages and methods to aid verification. GPCE 2006: 221-236 5.Jean-Raymond Abrial, Michael Butler, Stefan Hallerstede, Laurent Voisin: An Open Extensible Tool Environment for Event-B. ICFEM 2006: 588-605 6.Jean-Raymond Abrial: Formal methods in industry: achievements, problems, future. ICSE 2006: 761-768 7. Jean-Raymond Abrial: Train Systems. RODIN Book 2006: 1-36 8. Jean-Raymond Abrial: Tools for Developing Large Systems (A Proposal). RODIN Book 2006: 387-390 9. Jean-Raymond Abrial: Refinement, Decomposition and Instantiation of Discrete Models. Abstract State Machines 2005: 17-40 10. Carroll Morgan, Thai Son Hoang, Jean-Raymond Abrial: The Challenge Of Probabilistic Event B - Extended Abstract. ZB 2005: 162-171 11. Jean-Raymond Abrial, Dominique Cansell, Dominique Mery: Refinement And Reachability in EventB. ZB 2005: 222-241 12. Jean-Raymond Abrial, Dominique Cansell: Formal Construction of a Nonblocking Concurrent Queue Algorithm (a Case Study in Atomicity). J. UCS 11(5): 744-770 (2005) 13. Jean-Raymond Abrial: Event Based Sequential Program Development: Application to Constructing a Pointer Program. FME 2003: 51-74 14. Jean-Raymond Abrial, Dominique Cansell: Click’n Prove: Interactive Proofs within Set Theory. TPHOLs 2003: 1-24 15. Jean-Raymond Abrial: B#: Toward a Synthesis between Z and B. ZB 2003: 168-177 16. Jean-Raymond Abrial, Dominique Cansell, Dominique Mery: Formal Derivation of Spanning Trees Algorithms. ZB 2003: 457-476 17. Jean-Raymond Abrial, Dominique Cansell, Dominique Mery: A Mechanically Proved and Incremental Development of IEEE 1394 Tree Identify Protocol. Formal Asp. Comput. 14(3): 215-227 (2003) 18. Jean-Raymond Abrial: B : pass, prsent, futur. Technique et Science Informatiques 22(1): 89-118 (2003) 19. Jean-Raymond Abrial, Louis Mussat: On Using Conditional Definitions In Formal Theories. ZB 2002: 242-269 20. Jean-Raymond Abrial, Dominique Cansell, Guy Laffitte: ”Higher-Order” Mathematics in B. ZB 2002: 370-393 21. Jean-Raymond Abrial: On B. B 1998: 1-8 22. Jean-Raymond Abrial, Louis Mussat: Introducing Dynamic Constraints in B. B 1998: 83-128 23. Jean-Raymond Abrial, Egon Brger, Hans Langmaack: Formal Methods for Industrial Applications, Specifying and Programming the Steam Boiler Control (the book grow out of a Dagstuhl Seminar, June 1995). Springer 1996 24. Jean-Raymond Abrial: The B-Book: Assigning Programs to Meanings. Cambridge University Press 1996 25. Jean-Raymond Abrial, Egon Brger, Hans Langmaack: The Stream Boiler Case Study: Competition of Formal Program Specification and Development Methods. Formal Methods for Industrial Applications 1995: 1-12 26. Jean-Raymond Abrial: Steam-Boiler Control Specification Problem. Formal Methods for Industrial Applications 1995: 500-509 27. Jean-Raymond Abrial: On Constructing Large Software Systems. IFIP Congress (1) 1992: 103-112 28. Jean-Raymond Abrial, Matthew K. O. Lee, David Neilson, P. N. Scharbach, Ib Holm Srensen: The B-Method. VDM Europe (2) 1991: 398-405 29. Jean-Raymond Abrial: A Formal Approach To Large Software Construction. MPC 1989: 1-20 30. Jean-Raymond Abrial: The B Tool (Abstract). VDM Europe 1988: 86-87 31. Jean-Raymond Abrial: The Mathematical Construction of a Program. Sci. Comput. Program. 4(1): 45-86 (1984) 32. Jean-Raymond Abrial: A Practical Approach to the Analysis of Concurrent Systems. The Analysis of Concurrent Systems 1983: 66-96 33. Jean-Raymond Abrial, Stephen A. Schuman, Bertrand Meyer: Specification Language. On the Construction of Programs 1980: 343-410 34. Jean-Raymond Abrial, Stephen A. Schuman: Non-Deterministic System Specification. Semantics of Concurrent Computation 1979: 34-50 35. Jean-Raymond Abrial: Data Semantics. IFIP Working Conference Data Base Management 1974: 1-60