Survey of Formal Specification Techniques for Reactive Systems
CARNEGIE-MELLON UNIV PITTSBURGH PA SOFTWARE ENGINEERING INST
Pagination or Media Count:
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.
- Computer Programming and Software