Abstract
This paper describes a method to verify safety properties of parameterized binary tree networks of processes. The method is based on the construction of a network invariant, defined as a fixpoint. Since least fixpoints did not give satisfactory results, backward computation of greatest fixpoints is explored, and a technique of computation based on heuristics is proposed. This technique has been implemented and two examples are presented.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
K. R. Apt and D. C. Kozen. Limits for automatic verification of finite-state concurrent systems. Information Processing Letters, 22:307–309, 1986.
G. Berry and G. Gonthier. The Esterel synchronous programming language: Design, semantics, implementation. Science of Computer Programming, 19(2):87–152, 1992.
P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4 th ACM Symposium on Principles of Programming Languages, POPL '77, Los Angeles, January 1977.
P. Cousot and R. Cousot. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In M. Bruynooghe and M. Wirsing, editors, PLILP'92, Leuven (Belgium), January 1992. LNCS 631, Springer Verlag.
E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM TOPLAS, 8(2), 1986.
E. M. Clarke, O. Grumberg, and S. Jha. Verifying parameterized networks using abstraction and regular languages. In CONCUR'95. LNCS 962, Springer Verlag, August 1995.
S. Eilenberg. Automata, Languages, and Machines. Academic Press, 1974.
E. A. Emerson and K. S. Namjoshi. Reasoning about rings. In Proc. 22th ACM Conf. on Principles of Programming Languages, POPL'95, San Francisco, January 1995.
E. A. Emerson and K. S. Namjoshi. Automatic verification of parameterized synchronous systems. In R. Alur and T. Henzinger, editors, 8th International Conference on Computer Aided Verification, CAV'96, Rutgers (N.J.), 1996.
N. Halbwachs. Synchronous programming of reactive systems. Kluwer Academic Pub., 1993.
D. Harel. Statecharts: A visual approach to complex systems. Science of Computer Programming, 8(3), 1987.
N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous dataflow programming language Lustre. Proceedings of the IEEE, 79(9):1305–1320, September 1991.
N. Halbwachs, F. Lagnier, and C. Ratel. An experience in proving regular networks of processes by modular model checking. Acta Informatica, 29(6/7):523–543, 1992.
N. Halbwachs, F. Lagnier, and P. Raymond. Synchronous observers and the verification of reactive systems. In M. Nivat, C. Rattray, T. Rus, and G. Scollo, editors, Third Int. Conf. on Algebraic Methodology and Software Technology, AMAST'93, Twente, June 1993. Workshops in Computing, Springer Verlag.
R. P. Kurshan and K McMillan. A structural induction theorem for processes. In 8th ACM Symposium on Principles of Distributed Computing, pages 239–247, Edmonton (Alberta), August 1989.
D. Lesens. The boolean automaton network grammar checker home page. http://www.imag.fr/VERIMAG/PEOPLE/David.Lesens/BANG, 1997.
D. Lesens, N. Halbwachs, and P. Raymond. Automatic verification of parameterized linear networks of processes. In 24th ACM Symposium on Principles of Programming Languages, POPL'97, Paris, January 1997.
F. Maraninchi. Operational and compositional semantics of synchronous automaton compositions. In CONCUR'92, Stony Brook, August 1992. LNCS 630, Springer Verlag.
R. Marelly and O. Grumberg. Gormel-grammar oriented model checker. Technical report, The Technion, 1991.
J. P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In International Symposium on Programming. LNCS 137, Springer Verlag, April 1982.
Z. Shtadler and O. Grumberg. Network grammars, communication behaviors and automatic verification. In Workshop on Automatic Verification Methods for Finite State Systems, Grenoble. LNCS 407, Springer Verlag, June 1989.
J. D. Ullman. Computational aspects of VLSI. Computer Science Press, 1984.
P. Wolper and V. Lovinfosse. Verifying properties of large sets of processes with network invariants. In International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble. LNCS 407, Springer Verlag, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lesens, D. (1997). Invariants of parameterized binary tree networks as greatest fixpoints. In: Johnson, M. (eds) Algebraic Methodology and Software Technology. AMAST 1997. Lecture Notes in Computer Science, vol 1349. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0000481
Download citation
DOI: https://doi.org/10.1007/BFb0000481
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63888-9
Online ISBN: 978-3-540-69661-2
eBook Packages: Springer Book Archive