Application of the Trace Assertion Method to the Specification, Design, and Verification of Automaton Programs

摘要

The paper considers the application of the trace assertion method [1] for specification and verification of automaton programs [2-4]. The trace assertion method allows the programmer to define an externally visible behavior of an automaton program in a rigorous way, without considering details of its implementation. The method is employed at the requirements specification stage of the system development. The paper introduces techniques for defining semantics of some elements of an automaton program, especially those involved in interactions with the control system. A formal approach to defining states of automaton programs is described. Results of studies related to the verification of specification requirements for automaton programs are also presented.