Abstract
In this paper we proposed a formalism based on automata on two dimensional strings for specifying inductive invariants for proving correctness of families of linear and circular networks. We proved our inductive approach to be sound and complete (semantical completeness). We have illustrated our approach by simple examples.
We have also given the inductive approach for verification of parametrized systems under fairness. In this case, we use generalized Buchi automata (or Streett automata) as inductive invariants. For this case, we have proved the soundness theorem.
As part of future work, it will be interesting to automate the different parts of the induction based approach and apply them to real practical examples. It will also be interesting to extend our approach to networks defined by context free grammars [SG89]. Further more, it will also be interesting to investigate logic based approaches for specification of the invariants.
This work is partly supported by the NSF grants CCR-9623229, CCR-9212183, CCR-9633536
Chapter PDF
References
K. R. Apt and D. Kozen: Limits to Automatic Program Verification. Information Processing Letters, 22.6 (1986), 307–309
M. Browne, E. M. Clarke and O. Grumberg: Reasoning About Networks with Many Identical Finite State Processes. Inf. and Computation, 81(1):13–31, Apr. 1989.
E. M. Clarke, O. Grumberg and S. Jha: Verifying Parametrized Networks Using Abstraction and Regular Languages. CONCUR 95.
E. M. Clarke, and O. Grumberg: Avoiding the State Explosion Problem in Temporal Logic Modelchecking Problem. In Proceedings of ACM Symposium on Principles of Distributed Computing 1987.
E. A. Emerson and K. S. Namjoshi: Reasoning About Rings, Proceedings of 22nd POPL conferece, Jan 1995.
E. A. Emerson and K. S. Namjoshi: Automatic Verification of Parametrized Synchronous Systems. Proceeding of the International Conference on Computer Aide Verification 1996.
S. M. German and A. P. Sistla: Reasoning About Systems with many Processes. JACM, July 1992, Vol 39, No. 3, pp 675–735.
P. Godefroid and P. Wolper: Using Partial Approach to Modelchecking. Proc 6th IEEE Symposium on Logic in Computer Science, pp 406–415, Amsterdam, July 1991.
R. P. Kurshan and K. McMillan: A Structural Induction Theorem for Processes. ACM Sym. on Principles of Distributed Computing, Aug. 1989.
Z. Shtadler and O. Grumberg: Network Grammars, Communication Behaviors and Automatic Verififcation. Proc. of International Workshop on Automatic Verification Methods for Finite State Systems, June 1989.
A. P. Sistla: Parametrized Verification of Linear Networks Using Automata as Invariants. Technical report, University of Illinois at Chicago 1997.
A. P. Sistla, M. Vardi and P. Wolper: The Complementation Problem for Buchi Automata and Applications to Temporal Logics. Proceedings Of The 12th International Colloquium On Automata, Languages And Programming, Greece, August 1985; The journal version of the paper appeared in Theoretical Computer Science, 49, No 2,3 1987, pp 217–237.
A. P. Sistla and S. M. German: Reasoning About many Processes. LICS 87.
P. Wolper and V. Lovinfosse: Verifying Properties of Large Sets of Processes with Network Invariants. Proc. 1989 Intl Wokshop on Automatic Verification Methods for Finite State Systems 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sistla, A.P. (1997). Parametrized verification of linear networks using automata as invariants. In: Grumberg, O. (eds) Computer Aided Verification. CAV 1997. Lecture Notes in Computer Science, vol 1254. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63166-6_40
Download citation
DOI: https://doi.org/10.1007/3-540-63166-6_40
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63166-8
Online ISBN: 978-3-540-69195-2
eBook Packages: Springer Book Archive