The verus tool: A quantitative approach to the formal verification of real-time systems
This work describes Verus, a new tool to be used in the formal verification of realtime systems. In Verus the designer specifies the system to be verified in a C-like language, and uses temporal logic model checking and quantitative timing analysis to verify its correctness. The information produced by our tool can help in verifying a real-time system in many ways. It not only assists in determining its correctness, but also provides insight into the behavior of the system. This allows for a better understanding of the system and in some cases it even suggests optimizations to the design.
We have used this tool to analyze several real-time systems of industrial complexity, such as an aircraft controller, a robotics controller and a distributed heterogeneous system. In all cases we have been able to determine the temporal correctness of the system. In several instances the results produced suggested modifications to the design that resulted in more efficient systems.
KeywordsModel Check Formal Verification Symbolic Model Check Priority Inversion Semiconductor Research Corporation
- 1.S. V. Campos. A quantitative approach to the formal verification of real-time systems. Ph.D. thesis, SCS, Carnegie Mellon University, 1996.Google Scholar
- 2.S. V. Campos. The priority inversion problem and real-time symbolic model checking. Technical Report CMU-CS-93-125, Carnegie Mellon University, 1993.Google Scholar
- 3.S. V. Campos and O. Grumberg. Selective quantitative analysis and interval model checking: verifying different facets of a system. Computer Aided Verification, 1996.Google Scholar
- 4.S. Campos, E. Clarke, W. Marrero, M. Minea, and H. Hiraishi. Computing quantitative characteristics of finite-state real-time systems. IEEE Real-Time Systems Symposium, 1994.Google Scholar
- 5.S. Campos, E. Clarke, W. Marrero and M. Minea. Verus: a tool for quantitative analysis of finite-state real-time systems. Languages,Compilers and Tools for Real-Time Systems, 1995Google Scholar
- 6.E. Clarke, O. Grumberg, and H. Hamaguchi. Another look at LTL model checking. Computer-Aided Verification, LNCS vol. 818. Springer-Verlag, 1994.Google Scholar
- 7.E. A. Emerson, A. K. Mok, A. P. Sistla, and J. Srinivasan. Quantitative temporal reasoning. Computer-Aided Verification, 1990.Google Scholar
- 8.K. L. McMillan. Symbolic model checking — an approach to the state explosion problem. Ph.D. thesis, SCS, Carnegie Mellon University, 1992.Google Scholar