Survey of Formal Specification Techniques for Reactive Systems

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
May 01, 1990
Accession Number
ADA232045

Entities

People

  • Mike Tudball
  • Patrick R. Place
  • William G. Wood

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Abstracts
  • Computer Programming
  • Computer Programs
  • Computers
  • Construction
  • Control Systems
  • Dead Reckoning
  • Engineering
  • Industrial Control Systems
  • Inertial Navigation
  • Inertial Navigation Systems
  • Language
  • Navigation
  • Operating Systems
  • Software Development
  • Standards
  • Time Intervals

Fields of Study

  • Computer science
  • Engineering

Readers

  • Software Engineering.
  • Systems Analysis and Design