Accession Number:

ADA275776

Title:

Formal Specification and Verification of Real-Time Sequential Control Systems

Descriptive Note:

Corporate Author:

UNIVIEW SYSTEMS MOUNTAIN VIEW CA

Personal Author(s):

Report Date:

1994-01-01

Pagination or Media Count:

12.0

Abstract:

A variety of methods have been employed for specifying the behavior of sequential control systems that, e.g., can be implemented by programmable logic controllers PLCs. In dealing with real-time issues, timed Petri nets and other popular formalisms provide limited capabilities with respect to both specification and analysis of behavior. At the same time, many of the formal methods that have been reported in the literature are not readily applicable to the area of sequential control. In this paper, we explore the application of a formal method for real-time systems based on hierarchical multi-state HMS machines, to the specification and verification of sequential control systems. Verification in this context goes beyond simulation and testing by attempting to provide mathematical proofs for correctness of behavior with respect to general safety properties. HMS machines, which were originally introduced in 1988, consist of parallel and hierarchical automata in which multiple states are true and multiple transitions can fire simultaneously. The temporal behavior of an HMS machine is defined in terms of an interval-based temporal logic. Examples of applications of HMS machines to sequential control problems and an overview of verification approaches are presented.

Subject Categories:

  • Computer Programming and Software
  • Test Facilities, Equipment and Methods

Distribution Statement:

APPROVED FOR PUBLIC RELEASE