Formal Specification and Verification of Real-Time Sequential Control Systems

摘要

A variety of methods have been employed for specifying the behavior of sequentialcontrol systems that, e.g., can be implemented by programmable logic controllers (PLC's). 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.