A basic formal verification problem is, given an implementation I and a specification or property S of a system show that I satisfies S. For programs, the problem can be cast in Hoare's axiomatic framework, {P}Q{R}, which means, if the precondition P holds before program Q executes, then the postcondition R holds after Q completes. Hoare gives rules on how to compute the precondition from the postcondition, then the verification can (possibly) be carried out by computing P from R. However, for systems that never terminate, like an air-traffic controller, which continuously interacts with its environment, the above correctness definition does not apply. Instead of formalizing correct outputs of the system, we need to characterize correct behaviors of the system.
Since Pnueli's landmark work in 1977, people believe that temporal logics are a suitable formalism to specify behaviors of the above mentioned systems. For a finite state transition system, there are two views for describing behavior.
The above mentioned verification problem is therefore reformulated as the model-checking problem: Given a finite state system I and a temporal logic formula S, does I satisfy S? It is well-known that the model-checking problem for finite state systems against temporal properties (LTL, CTL, CTL*, mu-calculus) is decidable. Symbolic model checking techniques [McMillan 92], based upon the succinct representation technique like Binary Decision Diagrams (BDD) [Bryant 86] of a finite set of states, have been widely used in automatic verification of finite-state systems describing protocols, hardware devices, and reactive systems.
Obviously, many real-world applications can not be modeled as finite state systems. Our research focuses on automatically analyzing infinite state systems using model checking techniques.
In this research, time is considered discrete. This makes it possible for us to use a number of existing results in automata theory. We distinguish two kinds of real-time systems: finite state real-time systems and infinite state real-time systems, depending on the number of states in a system when clocks are ignored. A typical example of finite state real-time systems is timed automata [Alur and Dill 90], where finite state machines are augmented with a number of clocks. An example of infinite state real-time systems is pushdown timed automata, where pushdown machines are augmented with a number of clocks. Further, instead of considering general temporal properties, we focus on a simpler but practically important class of properties called safety properties, which are satisfied by every reachable state. Verification of such properties is called safety analysis.
By using automata theory, we have given binary reachability characterizations for a number of infinite state real-time system models. These characterizations are essential in establishing a number of decidability results for safety analysis problems of the models.
We consider practical approximation techniques to debug a complex (real-time) specification. These techniques include various search strategies and approximation techniques of image computations. We couple the research with an existing specification language, called ASTRAL.
We consider a nontrivial subset of ASTRAL, Small-ASTRAL, with discrete time. This allows us using the Omega library to symbolically representing Small-ASTRAL formulas (i.e., Presburger formulas). The model-checking procedure is carried out on the execution tree of a Small-ASTRAL process instance. To speed up the debugging process, we introduce a number of search strategies (depth-first search, breadth-first search, and depth-breadth search) as well as a number of image approximation techniques (partial image, random walk and dynamic environment generation). A large set of mutation tests on a benchmark specification shows the effectiveness of the techniques.
We have also been co-operating with other researchers:
[Postscript] Oscar H. Ibarra, Jianwen Su, Zhe Dang, T. Bultan and R. A. Kemmerer, Counter Machines: Decidable Properties and Applications to Verification Problems, Proceedings of the 25th International Symposium on Mathematical Foundations of Computer Science (MFCS 2000), Lecture Notes in Computer Science, Springer, (to appear).
[Postscript] Zhe Dang and R. A. Kemmerer, Using the ASTRAL Symbolic Model Checker as a Specification Debugger: Three Approximation Techniques, Proceedings of the 22nd International Conference on Software Engineering (ICSE 2000), pp. 345-354, IEEE Press.
[Postscript] Zhe Dang, Oscar H. Ibarra, Tevfik Bultan, Richard A. Kemmerer, and Jianwen Su, Binary Reachability Analysis of Discrete Pushdown Timed Automata, Proceedings of the International Conference on Computer Aided Verification (CAV 2000), Lecture Notes in Computer Science 1855, pp. 69-84, Springer.
[Postscript] Zhe Dang and R. A. Kemmerer, Using the ASTRAL Model Checker to Analyze Mobile IP, Proceedings of the 21st International Conference on Software Engineering (ICSE 99), pp. 132-141, IEEE Press.
[Postscript] Paul Z. Kolano, Zhe Dang, Richard A. Kemmerer, The Design and Analysis of Real-Time Systems Using the ASTRAL Software Development Environment, Annals of Software Engineering 7: 177-210 (1999)
[Postscript] Zhe Dang and R. A. Kemmerer, A symbolic model checker for testing ASTRAL real-time specifications, Proceedings of the 6th International Conference on Real-Time Computing Systems and Applications (RTCSA'99), pp. 174-181, IEEE Press.
[Postscript] Zhe Dang and R. A. Kemmerer, Dynamic Environment Generations for an ASTRAL Process, Technical Report, Computer Science Department, University of California, Santa Barbara, 2000.
[HTML] Zhe Dang and R. A. Kemmerer, Using the ASTRAL Model Checker for Cryptographic Protocol Analysis, DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997.