| In the last decade, model checking has been used extensively to verify complex hardware and software systems. However, in practice, model checking suffers from a phenomenon called state explosion, where the global state transition graph may be exponential in the number of subcomponents in the system. The state explosion problem severely limits the size of the systems that one can model check automatically. Another obstacle is that formal specification methods, based on temporal logic or automata, are largely unknown in the design community. This dissertation addresses both these issues by introducing a visual notation that is already used in the informal specification of hardware systems and by providing efficient model checking algorithms for these specifications.; The first part of the dissertation presents, Regular Timing Diagrams (RTDs), an expressive notation for specifying the temporal behavior of asynchronous systems. These polynomial-time algorithms are a significant improvement over previous monolithic algorithms that are exponential in the worst case. The second part of the dissertation introduces Synchronous Regular Timing Diagrams (SRTDs) that are used to specify the behavior of synchronous systems.; The final part of the dissertation offers a way to cope with state explosion by employing a proof technique called compositional reasoning that reduces reasoning about the entire system to reasoning about individual components. When the property is an SRTD, this rule can be applied in a fully automatic manner by using the fact that SRTDs have a natural decomposition into assume-guarantee pairs. The application of this rule to Lucent's PCI Core and other case studies yielded substantial reductions in the space and time required for model checking.; In summary, this dissertation introduces an alternative and visual way of specifying temporal properties, which makes model checking more accessible to the non-expert user. Furthermore, this work addresses the state explosion problem by presenting efficient model checking algorithms and a general assume-guarantee proof methodology that can be applied in a fully automated manner to specifications in this form. (Abstract shortened by UMI.)... |
