Logic-based Verification of the Distributed Dining Philosophers Protocol

• Autorzy: Delzanno, G.
• Konferencja: Italian Conference on Computational Logic (Convegno Italiano di Logica Computazionale, CILC 2016) (31; 20-22.07.2016; Università degli Studi di Milano-Bicocca, Italy)
• Języki publikacji: EN

Abstrakty

EN

We present a logic-based framework for the specification and validation of distributed protocols. Our specification language is a logic-based presentation of update rules for arbitrary graphs. Update rules are specified via conditional rewriting rules defined over a relational language. We focus our attention on unary and binary relations as a way to specify predicates over nodes and edges of a graph. For the considered language, we define assertions that can be applied to specify correctness properties for arbitrary configurations. We apply the language to model the distributed version of the Dining Philosopher Protocol. The protocol is defined for asynchronous processes distributed over a graph with arbitrary topology. We propose then validation methods based on source to source transformations and deductive reasoning. We apply the resulting method to provide a succint correctness proof of the considered case-study.

Słowa kluczowe

EN

mathematical models; mathematical analysis; programming languages; arbitrary constants; graph theory; probability theory

• Czasopismo: Fundamenta Informaticae
• Rocznik: 2018
• Tom: Vol. 161, nr 1/2
• Strony: 113--133
• Opis fizyczny: Bibliogr. 40 poz., tab.

Twórcy

autor

Delzanno, G.

• DIBRIS, University of Genova, Italy,

Bibliografia

• [1] Namjoshi KS, Trefler RJ. Uncovering Symmetries in Irregular Process Networks. In: VMCAI. 2013 pp. 496-514.
• [2] Hariri BB, Calvanese D, De Giacomo G, Deutsch A, Montali M. Verification of relational data-centric dynamic systems with external services. In: Proceedings of the 32nd ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, PODS 2013, New York, NY, USA - June 22-27, 2013. 2013 pp. 163-174. doi:10.1145/2463664.2465221.
• [3] Delzanno G, Sangnier A, Zavattaro G. Parameterized Verification of Ad Hoc Networks. In: CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings. 2010 pp. 313-327. doi:10.1007/978-3-642-15375-4\_22.
• [4] Delzanno G, Sangnier A, Zavattaro G. On the Power of Cliques in the Parameterized Verification of Ad Hoc Networks. In: Foundations of Software Science and Computational Structures - 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings. 2011 pp. 441-455. doi:10.1007/978-3-642-19805-2\_30.
• [5] Delzanno G, Sangnier A, Zavattaro G. Verification of Ad Hoc Networks with Node and Communication Failures. In: FORTE/FMOODS’12, volume 7273 of LNCS. Springer, 2012 pp. 235-250.
• [6] Bertrand N, Fournier P, Sangnier A. Distributed Local Strategies in Broadcast Networks. In: 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1.4, 2015. 2015 pp. 44-57. doi:10.4230/LIPIcs.CONCUR.2015.44.
• [7] Bertrand N, Delzanno G, König B, Sangnier A, Stückrath J. On the Decidability Status of Reachability and Coverability in Graph Transformation Systems. In: RTA’12, volume 15 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2012 pp. 101-116.
• [8] Kanovich MI, Kirigin TB, Nigam V, Scedrov A. Bounded Memory Dolev-Yao Adversaries in Collaborative Systems. In: Formal Aspects of Security and Trust - 7th International Workshop, FAST 2010, Pisa, Italy, September 16-17, 2010. Revised Selected Papers. 2010 pp. 18-33.
• [9] Kanovich MI, Rowe PD, Scedrov A. Collaborative Planning with Confidentiality. J. Autom. Reasoning, 2011. 46(3-4):389-421.
• [10] Namjoshi KS, Trefler RJ. Analysis of Dynamic Process Networks. In: Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. 2015 pp. 164-178. doi:10.1007/978-3-662-46681-0_11.
• [11] Ghilardi S, Ranise S. Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis. Logical Methods in Computer Science, 2010. 6 (4).
• [12] Delzanno G. A Logic-based Approach to Verify Distributed Protocols. In: Proceedings of the 31st Italian Conference on Computational Logic, Milano, Italy, June 20-22, 2016. 2016 pp. 86-101.
• [13] Bertrand N, Delzanno G, König B, Sangnier A, Stückrath J. On the Decidability Status of Reachability and Coverability in Graph Transformation Systems. In: 23rd International Conference on Rewriting Techniques and Applications (RTA’12) , RTA 2012, May 28-June 2, 2012, Nagoya, Japan. 2012 pp. 101-116. doi:10.4230/LIPIcs.RTA.2012.101.
• [14] Delzanno G, Sangnier A, Traverso R, Zavattaro G. On the Complexity of Parameterized Reachability in Reconfigurable Broadcast Networks. In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2012, December 15-17, 2012, Hyderabad, India. 2012 pp. 289-300. doi:10.4230/LIPIcs.FSTTCS.2012.289.
• [15] German SM, Sistla AP. Reasoning about Systems with Many Processes. J. ACM, 1992. 39 (3): 675-735.
• [16] Emerson EA, Namjoshi KS. On Model Checking for Non-Deterministic Infinite-State Systems. In: Thirteenth Annual IEEE Symposium on Logic in Computer Science, Indianapolis, Indiana, USA, June 21-24, 1998. 1998 pp. 70-80. doi:10.1109/LICS.1998.705644.
• [17] Bardin S, Finkel A, Leroux J, Petrucci L. FAST: acceleration from theory to practice. STTT, 2008. 10 (5): 401-424. doi:10.1007/s10009-008-0064-3.
• [18] http://wwwlsvens-cachanfr/Software/fast/.
• [19] http://wwwliafajussieufr/~sighirea/trex/.
• [20] http://wwwmontefioreulgacbe/~boigelot/research/lash/.
• [21] https://githubcom/pierreganty/mist.
• [22] Fioravanti F, Pettorossi A, Proietti M, Senni V. Improving Reachability Analysis of Infinite State Systems by Specialization. Fundam. Inform., 2012. 119(3-4):281-300. doi:10.3233/FI-2012-738.
• [23] http://usersmatunimiit/users/ghilardi/mcmt/.
• [24] http://wwwituuse/research/docs/fm/apv/tools/pfs/.
• [25] http://wwwituuse/research/docs/fm/apv/tools/undip/.
• [26] http://wwwccsneuedu/home/wahl/Research/boom-and-cutoffshtml.
• [27] Kaiser A, Kroening D, Wahl T. A Widening Approach to Multithreaded Program Verification. ACM Trans. Program. Lang. Syst., 2014. 36(4):14.
• [28] Kroening D. Automated Verification of Concurrent Software. In: Reachability Problems - 7th International Workshop, RP 2013, Uppsala, Sweden, September 24-26, 2013 Proceedings. 2013 pp. 19-20. doi:10.1007/978-3-642-41036-9_2.
• [29] Liu P, Wahl T. Infinite-state backward exploration of Boolean broadcast programs. In: Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, October 21-24, 2014. 2014 pp. 155-162. doi:10.1109/FMCAD.2014.6987608.
• [30] Kaiser A, Kroening D, Wahl T. Lost in Abstraction: Monotonicity in Multi-threaded Programs. In: CONCUR 2014 - Concurrency Theory - 25th International Conference, CONCUR 2014, Rome, Italy, September 2-5, 2014. Proceedings. 2014 pp. 141-155. doi:10.1007/978-3-662-44584-6_11.
• [31] http://wwwahmedrezinecom/tools/.
• [32] Ganty P, Rezine A. Ordered Counter-Abstraction - Refinable Subword Relations for Parameterized Verification. In: Language and Automata Theory and Applications - 8th International Conference, LATA 2014, Madrid, Spain, March 10-14, 2014. Proceedings. 2014 pp. 396-408. doi:10.1007/978-3-319-04921-2_32.
• [33] König B, Kozioura V. Augur 2 - A New Version of a Tool for the Analysis of Graph Transformation Systems. Electr. Notes Theor. Comput. Sci., 2008. 211:201-210. doi:10.1016/j.entcs.2008.04.042.
• [34] Meyer R, Strazny T. Petruchio: From Dynamic Networks to Nets. In: Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings. 2010 pp. 175-179. doi:10.1007/978-3-642-14295-6_19.
• [35] Stückrath J. Uncover: Using Coverability Analysis for Verifying Graph Transformation Systems. In: Graph Transformation - 8th International Conference, ICGT 2015, Held as Part of STAF 2015, L’Aquila, Italy, July 21-23, 2015. Proceedings. 2015 pp. 266-274. doi:10.1007/978-3-319-21145-9_17.
• [36] http://wwwtiinfuni-duede/de/research/tools/uncover/.
• [37] Conchon S, Goel A, Krstic S, Mebsout A, Zaïdi F. Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems - Tool Paper. In: Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings. 2012 pp. 718-724.
• [38] Cervesato I, Durgin NA, Lincoln P, Mitchell JC, Scedrov A. A Meta-Notation for Protocol Analysis. In: Proceedings of the 12th IEEE Computer Security Foundations Workshop, CSFW 1999, Mordano, Italy, June 28-30, 1999. 1999 pp. 55-69.
• [39] Delzanno G. Constraint-based automatic verification of abstract models of multithreaded programs. TPLP, 2007. 7(1-2):67-91.
• [40] Delzanno G. Reachability Predicates for Graph Assertions. In: Reachability Problems - 10th International Workshop, RP 2016, Aalborg, Denmark, September 19-21, 2016, Proceedings. 2016 pp. 63-76.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2018).

Identyfikatory

DOI

10.3233/FI-2018-1697