Observations on industrial practice using formal methods

Formal methods refer to the use of mathematically based techniques in software and system engineering. The authors summarize observations on their use in a dozen applications in industrial settings. Application goals ranged from reengineering to system certification. The purpose is to extract some of the key observations about practice in software engineering terms with minimal reference to formal methods terminology and glossing over distinctions among methods. The methodology of the study is described. Applications include oscilloscopes, nuclear reactors, trains, planes, ships, satellites, smartcards, transaction processing, arithmetic units, networks, medical instruments, and language processors. The observations follow from a systematic survey of these applications using a structured interview process and analysis of results using a set of features covering various aspects of practice: process, methods, tools, and technology transfer