Abstract
The method of invisible invariants was developed originally in order to verify safety properties of parameterized systems in a fully automatic manner. The method is based on (1) a project&generalize heuristic to generate auxiliary constructs for parameterized systems and (2) a small-model theorem, implying that it is sufficient to check the validity of logical assertions of a certain syntactic form on small instantiations of a parameterized system. The approach can be generalized to any deductive proof rule that (1) requires auxiliary constructs that can be generated by project&generalize, and (2) the premises resulting when using the constructs are of the form covered by the small-model theorem.
The method of invisible ranking, presented here, generalizes the approach to liveness properties of parameterized systems. Starting with a proof rule and cases where the method can be applied almost “as is,” the paper progresses to develop deductive proof rules for liveness and extend the small-model theorem to cover many intricate families of parameterized systems.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Apt, K.R., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Inf. Proc. Lett. 22(6), 307–309 (1986)
Arons, T., Pnueli, A., Ruah, S., Xu, J., Zuck, L.: Parameterized verification with automatically computed inductive assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) Proceedings of the 13th International Conference on Computer-Aided Verification (CAV’01). Lecture Notes in Computer Science, vol. 2102, pp. 221–234. Springer, Berlin Heidelberg New York (2001)
Bjørner, N., Browne, I.A., Chang, E., Colóon, 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, Stanford, CA (1995)
Clarke, E.M., Grumberg, O., Jha, S.: Verifying parametrized networks using abstraction and regular languages. In: Proceedings of the 6th International Conference on Concurrency Theory (CONCUR92), Philadelphia. Lecture Notes in Computer Science, vol. 962, pp. 395–407. Springer, Berlin Heidelberg New York (1995)
Choueka, Y.: Theories of automata on ω-tapes: a simplified approach. J. Comput. Syst. Sci. 8, 117–141 (1974)
Colon, M., Sipma, H.: Practical methods for proving program termination. In: Brinksma, E., Larsen, K.G. (eds.) Proceedings of the 14th International Conference on Computer-Aided Verification (CAV’02). Lecture Notes in Computer Science, vol. 2404, pp. 442–454. Springer, Berlin Heidelberg New York (2002)
Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: Proceedings of the 17th International Conference on Automated Deduction (CADE-17), pp. 236–255 (2000)
Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: Procedings of the 22nd ACM Conference on Principles of Programming Languages (POPL’95), San Francisco (1995)
Fang, Y., Piterman, N., Pnueli, A., Zuck, L.: Liveness with incomprehensible ranking. In: Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’04). Lecture Notes in Computer Science, vol. 2988, pp. 482–496. Springer, Berlin Heidelberg New York (2004)
Fang, Y., Piterman, N., Pnueli, A., Zuck, L.: Liveness with invisible ranking. In: Proceedings of the 5th conference on Verification, Model Checking, and Abstract Interpretation, Venice, Italy. Lecture Notes in Computer Science, vol. 2937, pp. 223–238. Springer, Berlin Heidelberg New York (2004)
Gyuris, V., Sistla, A.P.: On-the-fly model checking under fairness that exploits symmetry. In: Grumberg, O. (ed.) Proceedings of the 9th International Conference on Computer-Aided Verification (CAV’97). Lecture Notes in Computer Science, vol. 1254. Springer, Berlin Heidelberg New York (1997)
Gribomont, E.P., Zenner, G.: Automated verification of szymanski’s algorithm. In: Steffen, B. (ed.) Proceedings of 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’98). Lecture Notes in Computer Science, vol. 1384, pp. 424–438. Springer, Berlin Heidelberg New York (1998)
Jonsson, B., Nilsson, M.: Transitive closures of regular relations for verifying infinite-state systems. In: Graf, S., Schwartzbach, M. (eds.) Proceedings of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’00). Lecture Notes in Computer Science, vol. 1785. Springer, Berlin Heidelberg New York (2000)
Kesten, Y., Piterman, N., Pnueli, A.: Bridging the gap between fair simulation and trace inclusion. In: Hunt Jr, W., Somenzi, F. (eds.) Proceedings of the 15th International Conference on Computer-Aided Verification (CAV’03), pp. 381–392. Boulder, CO (2003)
Lesens, D., Halbwachs, N., Raymond, P.: Automatic verification of parameterized linear networks of processes. In: Proceedings of the 24th ACM Symposium on Principles of Programming Languages (POPL’97), Paris (1997)
McMillan, K.L.: Verification of an implementation of Tomasulo’s algorithm by compositional model checking. In: Hu, A.J., Vardi, M.Y., Hu, A.J., Vardi, M.Y. (eds.) Proceedings of the 10th International Conference on Computer-Aided Verification (CAV’98). Lecture Notes in Computer Science, vol. 1427, pp. 110–121. Springer, Berlin Heidelberg New York (1998)
Manna, Z., Pnueli, A.: Completing the temporal picture. Theor. Comput. Sci. 83(1), 97–130 (1991)
Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, Berlin Heidelberg New York (1995)
Owre, S., Shankar, N., Rushby, J.M.: User guide for the PVS specification and verification system (draft). Technical Report, Computer Science Laboratory, SRI International, Menlo Park, CA (1993)
Pnueli, A., Ruah, S., Zuck, L.: Automatic deductive verification with invisible invariants. In: Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’01). Lecture Notes in Computer Science, vol. 2031, pp. 82–97. Springer, Berlin Heidelberg New York (2001)
Pnueli, A., Xu, J., Zuck, L.: Liveness with (0, 1, ∞)-counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) Proceedings of the 14th International Conference on Computer Aided Verification (CAV’02). Lecture Notes in Computer Science, vol. 2404, pp. 107–122. Springer, Berlin Heidelberg New York (2002)
Shahar, E.: The TLV manual (2000). http://www.wisdom.weizmann.ac.il/~verify/tlv
Szymanski, B.K.: A simple solution to Lamport’s concurrent programming problem with linear wait. In: Proceedings of the International Conference on Supercomputing Systems, pp. 621–626, St. Malo, France (1988)
Vardi, M.Y.: Verification of concurrent programs – the automata-theoretic framework. Ann. Pure Appl. Logic 51, 79–98 (1991)
Zuck, L., Pnueli, A.: Model checking and abstraction to the aid of parameterized systems. Comput. Lang. Syst. Struct. 30 (3/4), 139–169 (2004)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Fang, Y., Piterman, N., Pnueli, A. et al. Liveness with invisible ranking. Int J Softw Tools Technol Transfer 8, 261–279 (2006). https://doi.org/10.1007/s10009-005-0193-x
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10009-005-0193-x