Industrial Tools for Formal Methods
This chapter gives a flavour of a selection of tools that are available to support the formal methodist in the performance of the various activities. Tools for VDM, Z, B, UML, theorem provers and model checking are considered. The tools include syntax checkers to determine whether the specification is syntactically correct; specialized editors which ensure that the written specification is syntactically correct; tools to support refinement; automated code generators that generate a high-level language corresponding to the specification; theorem provers to demonstrate the correctness of the refinement steps and to identify and resolve proof obligations, as well proving the presence or absence of key properties; and specification animation tools where the execution of the specification can be simulated.
- 1.J. Fitzgerald, P.G. Larsen, Modelling Systems—Practical Tools and Techniques in Software Development (Cambridge University Press, 2009)Google Scholar
- 2.J.P. Hoare, Application of the B method to CICS, in Applications of Formal Methods. Prentice Hall International Series in Computer Science (1995)Google Scholar