Survey of Formal Specification Techniques for Reactive Systems
Patrick R. H. Place, William Graham Wood, Mike Tudball · 1990
Abstract : Formal methods are being considered for the description of many systems including systems with real time constraints and multiple concurrently executing processes. This report develops a set of evaluation criteria and evaluates Communicating Sequential Processes (CSP), the Vienna Development Method (VDM), and temporal logic. The evaluation is based on specifications, written with each of the techniques, of an example avionics system. The term reactive systems is used in this report to describe systems that do not terminate but instead maintain continuing interaction with the environment. Examples of reactive systems are operating systems and industrial control systems. The report classifies each specification technique using criteria based on the characteristics and development of reactive systems. We also provide an evaluation of the applicability of the techniques to the specification of reactive systems. The report also includes a summary of our discussions with developers and practitioners of formal specification techniques.