TIMING VERIFICATION BY SUCCESSIVE APPROXIMATION

被引:37
作者
ALUR, R
ITAI, A
KURSHAN, RP
YANNAKAKIS, M
机构
[1] AT and T Bell Laboratories, Murray Hill
关键词
D O I
10.1006/inco.1995.1059
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
We present an algorithm for verifying that a model M with timing constraints satisfies a given temporal property T. The model M is given as a parallel composition of omega-automata P-i, where each automaton P-i is constrained by bounds on delays. The property T is given as an omega-automaton as well, and the verification problem is posed as a language inclusion question L(M) subset of or equal to L(T). In constructing the composition M of the constrained automata P-i, one needs to rule out the behaviors that are inconsistent with the delay bounds, and this step is (provably) computationally expensive. We propose an iterative solution which involves generating successive approximations M(i) to M, with containment L(M) subset of or equal to L(M(j)) and monotone convergence L(M(j)) --> L(M) within a bounded number of steps. As the succession progresses, the approximations M(j) become more complex. At any step of the iteration one may get a proof or a counter-example to the original language inclusion question. The described algorithm is implemented into the verifier Cospan. We illustrate the benefits of our strategy through some examples. (C) 1995 Academic Press, Inc.
引用
收藏
页码:142 / 157
页数:16
相关论文
共 25 条
[21]  
McMillan K., Symbolic Model Checking: An Approach to the State Explosion Problem, (1993)
[22]  
Papadimitriou C.H., Steiglitz K., Combinatorial Optimization: Algorithms and Complexity, (1982)
[23]  
Thomas W., Automata on infinite objects, Handbook of Theoretical Computer Science, B, pp. 133-191, (1990)
[24]  
Vardi M.Y., Wolper P., An automata-theoretic approach to automatic program verification, Proceedings of the First IEEE Symposium on Logic in Computer Science, pp. 332-344, (1986)
[25]  
Yannakakis M., Graph-theoretic methods in database theory, Proceedings of the 9Th ACM Symposium on Principles of Database Systems, pp. 230-242, (1990)