Iterative algorithms for formal verification of embedded real-time systems

ABSTRACT

Most embedded real-time systems consist of many concurrent components operating at significantly different speeds. Thus, an algorithm for formal verification of such systems must efficiently deal with a large number of states and large ratios of timing constants. We present such an algorithm based on timed automata, a model where a finite state system is augmented with time measuring devices called timers. We also present a semi-decision procedure for an extended model where timers can be decremented. This extension allows describing behaviors that are not expressible by timed automata, for example interrupts in a real-time operating system.

References

1. 1.R. Alur and D. L. Dill. Automata for modelling real-time systems. In Proceeding of ICALP'90. Springer-Verlag, 1990. LNCS vol. 443.
2. 2.R. Alur et al. An implementation of three algorithms for timing verification based on automata emptiness. In Proceedings of IEEE Real-time Systems Symposium, 1992.
3. 3.R. Alur et al. Timing verification by successive approximation. In Proceedings of CA V'92. Springer-Verlag, 1993. LNCS vol. 663.
4. 4.A. Aziz et al. HSIS: A BDD-based environment for formal verification. In Proceedings of the 3lib A CM/IEEE Design Automation Conference, 1994.
5. 5.F. Balarin. Iterative Methods for Formal Verification of Discrete Event Systems. PhD thesis, University of California Berkeley, 1994. in preparation.
6. 6.F. Balarin et al. Formal verification of the PATHO real-time operating system. In Proceedings of 33lh Conference on Decision and Control, 1994.
7. 7.F. Balarin and A. L. Sangiovanni-Vincentelli. An iterative approach to verification of real-time systems. Formal Methods in System Design: An International Journal, 1994. to be published.
8. 8.T. A. Henzinger et al. Symbolic model-checking for real-time systems. In Proceedings of 7th LICS. IEEE Computer Society Press, 1992.
9. 9.J. Hopcroft and J. Ullman. Introduction to Automata Theory, languages and Computation. Addison Wesley, 1979.
10. 10.J. McManis and P. Varaiya. Suspension automata: A decidable class of hybrid automata. In Proceedings of CA V'94. Springer-Verlag, 1994. LNCS vol. 818.
11. 11.R. E. Tarjan. Data Structures and Network Algorithms. Society for Industrial and Applied Mathematics, Philadelphia, PA, 1983.

Index Terms

• Hardware

  • Hardware validation

    • Functional verification

• Theory of computation

  • Formal languages and automata theory