Symbolic verification of real-time controllers
Mark A. Stalzer · University of Southern California Digital Library · 2017
Presented are techniques for formally verifying the correctness of real-time, safety-critical controllers based on a synchronous model of computation. These techniques are generalizations of symbolic model checking, as introduced by Clarke et al., and are applicable to systems that were intractable for other model checking methods due to their large number of states. The work has four major directions: (1) generalizing symbolic model checking to Real-Time Computational Tree Logic (Emerson et al.); (2) the development of a new algorithm for computing the predecessors of states that improves the performance of symbolic model checking; (3) applying the techniques to the verification of useful real-time controllers; and, (4) the introduction of the S scYNCHRONOUS A scCTION L scANGUAGE (S scAL) for implementing real-time controllers. S scAL is based on rules which consist of an enabling condition and a set of assignments to the system's state variables. At each clock tick, all enabled actions fire simultaneously. As such, S scAL is highly concurrent and can be compiled directly into programmable hardware. One problem is simultaneous assignments to the same variable, which is commonly known as a race condition. As part of the S scAL semantics, a technique for detecting race conditions is presented. One result is that the synchronous system model used by S scAL and the verification techniques is also applicable to asynchronous systems. All techniques presented in this work have been implemented in the Real-Time Symbolic Model Checker (RTSMC) program. Timing results are given and compared with other approaches. (Copies available exclusively from the Micrographics Department, Doheny Library, USC, Los Angeles, CA 90089-0182.)