Abstract
The method of Invisible Invariants was developed in order to verify safety properties of parametrized systems in a fully automatic manner. In this paper, we apply the method of invisible invariant to “bounded response” properties, i.e., liveness properties of the type \( p \Rightarrow \diamondsuit q\) that are bounded – once a p-state is reached, it takes a bounded number of rounds (where a round is a sequence of steps in which each process has been given a chance to proceed) to reach a q-state – thus, they are essentially safety properties.
With a “liveness monitor” that observes certain behavior of a system, establishing “bounded response” properties over the system is reduced to the verification of invariant properties.
It is often the case that the inductive invariants for systems with “liveness monitors” contain assertions of a certain form that the original method of invisible invariant is not able to generate, nor to check inductiveness. To accommodate invariants of such forms, we extend the techniques used for invariant generation, as well as the small model theorem for validity check.
This research was supported in part by NSF grant CCR-0205571 and ONR grant N00014-99-1-0131.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Apt, K.R., Kozen, D.: Limits for automatic program verification of finite-state concurrent systems. Info. Proc. Lett. 22(6) (1986)
Arons, T., Pnueli, A., Ruah, S., Xu, J., Zuck, L.D.: Parameterized verification with automatically computed inductive assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 221–234. Springer, Heidelberg (2001)
Arons, T., Pnueli, A., Zuck, L.D.: Parameterized verification by probabilistic abstraction. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 87–102. Springer, Heidelberg (2003)
Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. In: Cleaveland, R., Garavel, H. (eds.) Electronic Notes in Theoretical Computer Science, vol. 66. Elsevier, Amsterdam (2002)
Bjørner, N., Browne, I.A., Chang, E., Colón, M., Kapur, A., Manna, Z., Sipma, H.B., Uribe, T.E.: STeP: The Stanford Temporal Prover, User’s Manual. Technical Report STAN-CS-TR-95-1562, Computer Science Department, Stanford University (November 1995)
Balaban, I., Fang, Y., Pnueli, A., Zuck, L.D.: An invisible invariant verifier. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 291–295. Springer, Heidelberg (2005)
Clarke, E.M., Grumberg, O., Jha, S.: Verifying parametrized networks using abstraction and regular languages. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 395–407. Springer, Heidelberg (1995)
Cohen, S., Lehmann, D., Pnueli, A.: Symmetric and economical solutions to the mutual exclusion problem in a distributed system. Theor. Comp. Sci. 34, 215–225 (1984)
Colón, M.A., Sipma, H.B.: Practical methods for proving program termination. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 442–454. Springer, Heidelberg (2002)
Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: 17th International Conference on Automated Deduction (CADE-17), pp. 236–255 (2000)
Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: Proc. 22nd ACM Conf. on Principles of Programming Languages, POPL 1995, San Francisco (1995)
Fang, Y., Piterman, N., Pnueli, A., Zuck, L.D.: Liveness with incomprehensible ranking. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 482–496. Springer, Heidelberg (2004)
Fang, Y., Piterman, N., Pnueli, A., Zuck, L.D.: Liveness with invisible ranking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 223–238. Springer, Heidelberg (2004)
Gyuris, V., Sistla, A.P.: On-the-fly model checking under fairness that exploits symmetry. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254. Springer, Heidelberg (1997)
Gribomont, E.P., Zenner, G.: Automated verification of szymanski’s algorithm. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 424–438. Springer, Heidelberg (1998)
Jonsson, B., Nilsson, M.: Transitive closures of regular relations for verifying infinite-state systems. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, p. 220. Springer, Heidelberg (2000)
Lesens, D., Halbwachs, N., Raymond, P.: Automatic verification of parameterized linear networks of processes. In: 24th ACM Symposium on Principles of Programming Languages, POPL 1997, Paris (1997)
McMillan, K.L.: Verification of Infinite State Systems by Compositional Model Checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 219–237. Springer, Heidelberg (1999)
Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995)
Owre, S., Shankar, N., Rushby, J.M.: User guide for the PVS specification and verification system (draft). Technical report, Comp. Sci., Laboratory, SRI International, Menlo Park, CA (1993)
Pnueli, A., Ruah, S., Zuck, L.D.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 82–97. Springer, Heidelberg (2001)
Pnueli, A., Xu, J., Zuck, L.: Liveness with (0,1, ∞ )-counter abstraction (2002)
Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. First IEEE Symp. Logic in Comp. Sci., pp. 332–344 (1986)
Zuck, L., Pnueli, A.: Model checking and abstraction to the aid of parameterized systems. Computer Languages, Systems, and Structures 30(3–4), 139–169 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 IFIP International Federation for Information Processing
About this paper
Cite this paper
Fang, Y., McMillan, K.L., Pnueli, A., Zuck, L.D. (2006). Liveness by Invisible Invariants. In: Najm, E., Pradat-Peyre, JF., Donzeau-Gouge, V.V. (eds) Formal Techniques for Networked and Distributed Systems - FORTE 2006. FORTE 2006. Lecture Notes in Computer Science, vol 4229. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11888116_26
Download citation
DOI: https://doi.org/10.1007/11888116_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-46219-4
Online ISBN: 978-3-540-46220-0
eBook Packages: Computer ScienceComputer Science (R0)