Debugging and verification of infinite state real-time systems
Zhe Dang, Richard A. Kemmerer, Tevfik Bultan · 2000
The successes of the automatic verification of finite state systems describing protocols, hardware devices and reactive systems have lead to much research in automatic verification of infinite state systems. In this dissertation, we consider a special, yet very important, class of infinite-state systems, real-time systems. Real-time systems are widely regarded as a natural application area for formal methods, since the presence of a time variable makes the systems more difficult to specify, design and test. In this research, time is considered to be discrete. This makes it possible for us to use a number of existing results in automata theory. Instead of restricting our research to be purely theoretical, we tie the questions to an existing specification language, called ASTRAL, which has been used to specify a number of real-world systems. Two subsets of the language, Small-ASTRAL and Mini-ASTRAL, are defined. They both preserve the most important timing features of ASTRAL. Though Small-ASTRAL is undecidable, it encourages us to investigate approximation techniques (partial image, random walk and dynamic environment generation) for debugging Small-ASTRAL specifications. Experimental results are presented and analyzed on a benchmark by using different approximation techniques as well different search strategies. One of the conclusions of this dissertation is that the proposed approximation techniques are effective for debugging a specification in a much shorter time than without using them. We also introduce a number of new proof techniques to show that both history-independent Mini-ASTRAL and the entire Mini-ASTRAL are decidable. These techniques allow us to further investigate other extensions of timed automata. In theory, we introduce two new models for infinite state systems. The first model is a timed automaton coupled with a multi-queue automaton so that the resulting machine retains the decidability of a class of Presburger formulas. The second model is a class of multicounter machines with mixed types of counters. This model is capable of providing an alternative theoretical tool for analyzing various timed models.