Compositional and hierarchical techniques for the formal verification of real-time systems
Serdar Taşiran, Robert K. Brayton · 1998
The focus of this dissertation is the formal verification of real-time systems: systems with discrete control structures operating over a continuous time domain. Validation of functionality and timing constitutes a major portion of any electronic system design effort. The prevalent approach based on software simulation is no longer satisfactory, not only because it does not provide formal assurance, but also because it requires an inordinate amount of computational and human resources. The scale of modern electronic systems make formal verification techniques indispensable. Algorithmic verification techniques suffer from “compositional complexity”: the fact that the size of a system's state-space grows exponentially in the number and sizes of its components. For real-time systems, this difficulty is compounded by the representation of the timing information. Recent research has produced formal verification algorithms with significantly improved performance; however, system sizes multiply every few years, and it is unlikely that these algorithms will be made exponentially more efficient over time. To counter the computational complexity of verifying real-time systems, a scheme for decomposing the problem is required. Toward this end, we develop a compositional and hierarchical verification methodology. As our modeling formalism, we use a variant of timed automata and languages. We explore several notions of refinement for real-time systems, present complexity results and algorithms. An assume-guarantee style verification rule is proposed for dividing the hierarchical verification task into subtasks, each one corresponding to one module in the system. The soundness of this rule used in conjunction with the refinement preorders is proven. The algorithms developed were implemented on the COSPAN and MOCHA verification platforms. We demonstrate the efficacy of our framework on two practical circuit designs: the Seitz queue and the STARI communication chip. We also specialize our techniques to the delay modeling and computation problem for combinational circuits. Modified modeling assumptions brought about by shrinking circuit feature sizes has revived interest in this problem. We report results that improve on previous timed-automaton-based methods significantly.