Academia and industry meet: some experiences of formal methods in practice

摘要

We present an overview of our observations and experiences of applying formal methods in industry. Our approach combines two existing and complimentary formal methods, namely the Cleanroom method [H. D. Mills et al., (1987), S. J. Prowell et al. (1998)] and the CSP framework [C. A. R. Hoare (1985), A. W. Roscoe (1998)] together with its model checker FDR. The problem we are interested in is the use of formal methods to develop software systems of a business-critical and untestable nature, where the software forms an essential part of some core product or service offered by a business. We argue that the successful implementation of such systems needs a more formal approach and reflect on why formal methods are rarely used in practice. We discuss the combination of Cleanroom and CSP, and show how they can be applied to develop the control software that is embedded in a complex manufacturing machine.