×

Liveness reasoning with Isabelle/HOL. (English) Zbl 1252.68198

Berghofer, Stefan (ed.) et al., Theorem proving in higher order logics. 22nd international conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-03358-2/pbk). Lecture Notes in Computer Science 5674, 485-499 (2009).
Summary: This paper describes an extension of Paulson’s inductive protocol verification approach for liveness reasoning. The extension requires no change of the system model underlying the original inductive approach. Therefore, all the advantages, which makes Paulson’s approach successful for safety reasoning are kept, while liveness reasoning becomes possible. To simplify liveness reasoning, a new fairness notion, named parametric fairness is used instead of the standard ones. A probabilistic model is established to support this new fairness notion. Experiments with small examples as well as real world communication protocols confirm the practicality of the extension. All the work has been formalized with Isabelle/HOL using Isar.
For the entire collection see [Zbl 1173.68002].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of Computer Security 6(1-2), 85–128 (1998) · Zbl 05430359 · doi:10.3233/JCS-1998-61-205
[2] Paulson, L.C.: Inductive analysis of the Internet protocol TLS. ACM Transactions on Computer and System Security 2(3), 332–351 (1999) · doi:10.1145/322510.322530
[3] Manna, Z., Pnueli, A.: Completing the temporal picture. Theor. Comput. Sci. 83(1), 91–130 (1991) · Zbl 0795.68133 · doi:10.1016/0304-3975(91)90041-Y
[4] Pnueli, A., Zuck, L.D.: Probabilistic verification. Information and Computation 103(1), 1–29 (1993) · Zbl 0797.68112 · doi:10.1006/inco.1993.1012
[5] Baier, C., Kwiatkowska, M.: On the verification of qualitative properties of probabilistic processes under fairness constraints. Information Processing Letters 66(2), 71–79 (1998) · Zbl 1078.68664 · doi:10.1016/S0020-0190(98)00038-6
[6] Jaeger, M.: Fairness, computable fairness and randomness. In: Proc. 2nd International Workshop on Probabilistic Methods in Verification (1999) · Zbl 1170.93026
[7] Yang, H., Zhang, X., Wang, Y.: Liveness proof of an elevator control system. In: The ’Emerging Trend’ of TPHOLs, Oxford University Computing Lab. PRG-RR-05-02, pp. 190–204 (2005)
[8] Yang, H., Zhang, X., Wang, Y.: A correctness proof of the srp protocol. In: 20th International Parallel and Distributed Processing Symposium (IPDPS 2006), Proceedings, Rhodes Island, Greece, April 25-29 (2006)
[9] Yang, H., Zhang, X., Wang, Y.: A correctness proof of the dsr protocol. In: Cao, J., Stojmenovic, I., Jia, X., Das, S.K. (eds.) MSN 2006. LNCS, vol. 4325, pp. 72–83. Springer, Heidelberg (2006) · doi:10.1007/11943952_7
[10] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL – A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002) · Zbl 0994.68131 · doi:10.1007/3-540-45949-9
[11] Wenzel, M.: Isar - a generic interpretative approach to readable formal proof documents. In: Nipkow, T., Paulson, L.C., Wenzel, M.T. (eds.) Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)
[12] Pnueli, A.: On the extremely fair treatment of probabilistic algorithms. In: Proceedings of the fifteenth annual ACM symposium on Theory of computing, pp. 278–290. ACM Press, New York (1983)
[13] Zhang, X., Yang, H., Wang, Y.: Liveness reasoning for inductive protocol verification. In: The ’Emerging Trend’ of TPHOLs, Oxford University Computing Lab. PRG-RR-05-02, pp. 221–235 (2005)
[14] Hurd, J.: Formal Verification of Probabilistic Algorithms. Ph.D thesis, University of Cambridge (2002) · Zbl 1013.68193
[15] Richter, S.: Formlizing integration theory with an application to probabilistic algorithms. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 271–286. Springer, Heidelberg (2004) · Zbl 1099.68736 · doi:10.1007/978-3-540-30142-4_20
[16] Pnueli, A.: On the extremely fair treatment of probabilistic algorithms. In: ACM (ed.) Proceedings of the 15th annual ACM Symposium on Theory of Computing, Boston, Massachusetts, April 25–27, pp. 278–290. ACM Press, New York (1983)
[17] Wang, J., Zhang, X., Zhang, Y., Yang, H.: A probabilistic model for parametric fairness in isabelle/hol. Technical Report 364/07, Department of Computer Science, University of Kaiserslautern (2007)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.