Formal Methods for Industrial Applications

1. Front Matter

   PDF

2. The steam boiler case study: Competition of formal program specification and development methods

   • Jean-Raymond Abrial, Egon Börger, Hans Langmaack

   Pages 1-12

3. Structural synthesis of programs from refined user requirements (Programming boiler control in NUT)

   • Mattin Addibpour, Enn Tyugu

   Pages 13-34

4. Using Focus, Lustre and probability theory for the design of a reliable control program

   • Christoph Andriessens, Thomas Lindner

   Pages 35-51

5. Refining abstract machine specifications of the steam boiler control to well documented executable code

   • Christoph Beierle, Egon Börger, Igor Đurđanović, Uwe Glässer, Elvinia Riccobene

   Pages 52-78

6. An algebraic specification of the Steam-Boiler Control System

   • Michel Bidoit, Claude Chevenier, Christine Pellen, JérÔme Ryckbosch

   Pages 79-108

7. A steam-boiler control specification with statecharts and Z

   • Robert Büssow, Matthias Weber

   Pages 109-128

8. An action system approach to the steam boiler problem

   • Michael Butler, Emil Sekerinski, Kaisa Sere

   Pages 129-148

9. The Steam Boiler problem in Lustre

   • Thierry Cattel, Gregory Duval

   Pages 149-164

10. The steam-boiler problem — A TLT solution

    • Jorge Cuéllar, Isolde Wildgruber

    Pages 165-183

11. The real-time behavior of the steam-boiler

    • Jorge R. Cuéllar, Isolde Wildgruber

    Pages 184-202

12. Specifying and verifying the Steam Boiler Problem with SPIN

    • Gregory Duval, Thierry Cattel

    Pages 203-217

13. TRIO specification of a steam boiler controller

    • Angelo Gargantini, Angelo Morzenti

    Pages 218-232

14. A formal specification of the Steam-Boiler Control problem by algebraic specifications with implicit state

    • Marie-Claude Gaudel, Pierre Dauchy, Carole Khoury

    Pages 233-264

15. Using HyTech to synthesize control parameters for a steam boiler

    • Thomas A. Henzinger, Howard Wong-Toi

    Pages 265-282

16. A VDM specification of the steam-boiler problem

    • Yves Ledru, Marie-Laure Potet

    Pages 283-317

17. Proving safety properties of the steam boiler controller

    • Gunter Leeb, Nancy Lynch

    Pages 318-338

18. Steam boiler control specification problem: A TLA solution

    • Frank Leßke, Stephan Merz

    Pages 339-358

19. Specifying optimal design for a steam-boiler system

    • Li XiaoShan, Wang JuAn

    Pages 359-378

20. An object-oriented algebraic steam-boiler control specification

    • Peter Csaba ölveczky, Piotr Kosiuczenko, Martin Wirsing

    Pages 379-402

This book, with the CD-ROM included, is the documentation of a unique collaborative effort in evaluating formal methods for usage under industrial constraints: the major techniques for formally supported specification, design, and verification of large programs and complex systems are applied to a non-trivial and non-academic problem which is typical for industrial informal requirements specifications.
The 21 papers included in the book, together with an introduction and competition report, were selected from 33 candidate solutions. This book comes with a CD-ROM containing, besides the printed papers, executable code, full definitions of all parts of the specifications, and detailed descriptions of foundational matters where appropriate.

• CD-R
• CD-ROM
• code
• complex systems
• design
• documentation
• formal method
• programming
• verification

Policies and ethics