PL EN


Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
Tytuł artykułu

Verification Techniques for a Network Algebra

Wybrane pełne teksty z tego czasopisma
Identyfikatory
Warianty tytułu
Języki publikacji
EN
Abstrakty
EN
The Core Network Algebra (CNA) is a model for concurrency that extends the point-to-point communication discipline of Milner’s CCS with multiparty interactions. Links are used to build chains describing how information flows among the different agents participating in a multiparty interaction. The inherent non-determinism in deciding both the number of participants in an interaction, and how they synchronize, makes it difficult to devise verification techniques for this language. We propose a symbolic semantics and a symbolic bisimulation for CNA which are more amenable for automating reasoning. Unlike the operational semantics of CNA, the symbolic semantics is finitely branching and it represents, compactly, a possibly infinite number of transitions. We give necessary and sufficient conditions to efficiently check the validity of symbolic configurations. We also propose the Symbolic Link Modal Logic, a seamless extension of the Hennessy-Milner logic which is able to characterize the (symbolic) transitions of CNA processes. Finally, we specify both the symbolic semantics and the modal logic as an executable rewriting theory. We thus obtain several verification procedures to analyze CNA processes.
Wydawca
Rocznik
Strony
1--38
Opis fizyczny
Bibliogr. 44 poz., rys.
Twórcy
autor
  • Università degli Studi di Sassari, Italy
  • ECT, Universidade Federal do Rio Grande do Norte, Brazil
Bibliografia
  • [1] Hoare C. Communicating Sequential Processes. Prentice-Hall, Inc., 1985.
  • [2] Peter H J van Eijk MD Chris A Vissers. The Formal Description Technique LOTOS. North-Holland, 1989.
  • [3] Hillston J. A Compositional Approach to Performance Modelling. Cambridge University Press, 1996.
  • [4] Fournet C, Gonthier G. The Reflexive CHAM and the Join-Calculus. In: Boehm H, Jr GLS (eds.), Conference Record of POPL’96: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, St. Petersburg Beach, Florida, USA, January 21-24, 1996. ACM Press 1996 pp. 372-385. ISBN-0-89791-769-3. doi:10.1145/237721.237805.
  • [5] Nestmann U. On the Expressive Power of Joint Input. Electronic Notes in Theoretical Computer Science, 1998. 16(2):145-152. URL https://doi.org/10.1016/S1571-0661(04)00123-9.
  • [6] Laneve C, Vitale A. The Expressive Power of Synchronizations. In: Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, 11-14 July 2010, Edinburgh, United Kingdom. IEEE Computer Society 2010 pp. 382-391. ISBN-978-0-7695-4114-3. doi:10.1109/LICS.2010.15.
  • [7] Montanari U, Sammartino M. Network Conscious pi-calculus: a Concurrent Semantics. In: MFPS 2012, Electronic Notes in Theoretical Computer Science 286. Elsevier, 2012 pp. 291-306.
  • [8] Bodei C, Brodo L, Bruni R. Open Multiparty Interaction. In: Martí-Oliet N, Palomino M (eds.), WADT 2012, Revised Selected Papers, volume 7841 of LNCS. Springer 2012 pp. 1-23. ISBN-978-3-642-37634-4. doi:10.1007/978-3-642-37635-1_1.
  • [9] Cardelli L, Gordon AD. Mobile ambients. Theor. Comput. Sci., 2000. 240(1):177-213. URL https://doi.org/10.1016/S0304-3975(99)00231-5.
  • [10] Bodei C, Brodo L, Bruni R, Chiarugi D. A Flat Process Calculus for Nested Membrane Interactions. Sci. Ann. Comp. Sci., 2014. 24(1):91-136. doi:10.7561/SACS.2014.1.91.
  • [11] Milner R, Parrow J, Walker D. A Calculus of Mobile Processes, I. Inf. Comput., 1992. 100(1):1-40. doi:10.1016/0890-5401(92)90008-4.
  • [12] Ciobanu G, Zakharov VA. Encoding Mobile Ambients into the π-Calculus. In: Perspectives of Systems Informatics, volume 4378. Springer Berlin Heidelberg, 2007 pp. 148-165. doi:10.1007/978-3-540-70881-0_15.
  • [13] Brodo L. On the expressiveness of the π-calculus and the mobile ambients. In: Algebraic Methodology and Software Technology, volume 6486 of LNCS. 2011 pp. 44-59. doi:10.1007/978-3-642-17796-5_3.
  • [14] Brodo L. On the expressiveness of pi-calculus for encoding mobile ambients. Mathematical Structures in Computer Science, 2018. 28(2):202-240. URL https://doi.org/10.1017/S0960129516000256.
  • [15] Bodei C, Brodo L, Bruni R. A Formal Approach to Open Multiparty Interactions. ArXiv:1807.03002, 2018. 1807.03002.
  • [16] Milner R. A Calculus of Communicating Systems, volume 92 of LNCS. Springer, 1980. ISBN-3-540-10235-3. doi:10.1007/3-540-10235-3.
  • [17] Meseguer J. Conditioned Rewriting Logic as a United Model of Concurrency. Theor. Comput. Sci., 1992. 96(1):73-155. doi:10.1016/0304-3975(92)90182-F.
  • [18] Clavel M, Durán F, Eker S, Lincoln P, Martí-Oliet N, Meseguer J, Talcott CL (eds.). All About Maude – A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, volume 4350 of LNCS. Springer, 2007. ISB- 978-3-540-71940-3. doi:10.1007/978-3-540-71999-1.
  • [19] Clavel M, Durán F, Eker S, Lincoln P, Martí-Oliet N, Meseguer J, Talcott CL. LTL Model Checking. In: All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic [18], 2007 pp. 385-418. doi:10.1007/978-3-540-71999-1_13.
  • [20] Brodo L, Olarte C. Symbolic Semantics for Multiparty Interactions in the Link-Calculus. In: Steffen B, Baier C, van den Brand M, Eder J, Hinchey M, Margaria T (eds.), SOFSEM 2017, volume 10139 of LNCS. Springer. ISBN-978-3-319-51962-3, 2017 pp. 62-75. doi:10.1007/978-3-319-51963-0_6.
  • [21] Milner R. Communication and concurrency. PHI Series in computer science. Prentice Hall, 1989. ISBN-978-0-13-115007-2.
  • [22] Milner R. Communicating and mobile systems - the Pi-calculus. Cambridge University Press, 1999. ISBN-978-0-521-65869-0.
  • [23] Gorrieri R, Versari C. Introduction to Concurrency Theory - Transition Systems and CCS. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2015. ISBN-978-3-319-21490-0. doi:10.1007/978-3-319-21491-7.
  • [24] Giambiagi P, Schneider G, Valencia FD. On the Expressiveness of Infinite Behavior and Name Scoping in Process Calculi. In: Walukiewicz I (ed.), FOSSACS 2004, volume 2987 of LNCS. Springer 2004 pp. 226-240. ISBN-3-540-21298-1. doi:10.1007/978-3-540-24727-2_17.
  • [25] Hennessy M, Milner R. On Observing Nondeterminism and Concurrency. In: de Bakker JW, van Leeuwen J (eds.), Automata, Languages and Programming, 7th Colloquium, Noordweijkerhout, The Netherland, July 14-18, 1980, Proceedings, volume 85 of LNCS. Springer 1980 pp. 299-309. ISBN-3-540-10003-2. doi:10.1007/3-540-10003-2_79.
  • [26] Hennessy M, Milner R. Algebraic Laws for Nondeterminism and Concurrency. J. ACM, 1985. 32(1):137-161. doi:10.1145/2455.2460.
  • [27] Kozen D. Results on the Propositional mu-Calculus. Theor. Comput. Sci., 1983. 27:333-354. doi:10.1016/0304-3975(82)90125-6.
  • [28] Manna Z, Pnueli A. The temporal logic of reactive and concurrent systems - specification. Springer, 1992. ISBN-978-3-540-97664-6.
  • [29] Lehmann DJ, Rabin MO. On the Advantages of Free Choice: A Symmetric and Fully Distributed Solution to the Dining Philosophers Problem. In: White J, Lipton RJ, Goldberg PC (eds.), POPL. ACM Press 1981 pp. 133-138. ISBN-0-89791-029-X. doi:10.1145/567532.567547.
  • [30] Meseguer J. The Temporal Logic of Rewriting: A Gentle Introduction. In: Degano P, Nicola RD, Meseguer J (eds.), Concurrency, Graphs and Models, Essays Dedicated to Ugo Montanari on the Occasion of His 65th Birthday, volume 5065 of LNCS. Springer 2008 pp. 354-382. ISBN-978-3-540-68676-7. doi:10.1007/978-3-540-68679-8_22.
  • [31] De Nicola R, Vaandrager FW. Action versus State based Logics for Transition Systems. In: Guessarian I (ed.), Semantics of Systems of Concurrent Processes, LITP Spring School on Theoretical Computer Science, volume 469 of LNCS. Springer 1990 pp. 407-419. ISBN-3-540-53479-2. doi:10.1007/3-540-53479-2_17.
  • [32] Bae K, Meseguer J. A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting. Electr. Notes Theor. Comput. Sci., 2012. 290:19-36. doi:10.1016/j.entcs.2012.11.009.
  • [33] Fournet C, Gonthier G. The Join Calculus: A Language for Distributed Mobile Programming. In: Barthe G, Dybjer P, Pinto L, Saraiva J (eds.), Applied Semantics, International Summer School, APPSEM 2000, Caminha, Portugal, September 9-15, 2000, Advanced Lectures, volume 2395 of LNCS. Springer. ISBN-3-540-44044-5, 2000 pp. 268-332. doi:10.1007/3-540-45699-6\_6.
  • [34] Coppo M, Dezani-Ciancaglini M, Yoshida N, Padovani L. Global progress for dynamically interleaved multiparty sessions. Mathematical Structures in Computer Science, 2016. 26(2):238-302. doi:10.1017/S0960129514000188.
  • [35] Honda K, Yoshida N, Carbone M. Multiparty Asynchronous Session Types. J. ACM, 2016. 63(1):9:1-9:67. doi:10.1145/2827695.
  • [36] Hankin C (ed.). Programming Languages and Systems - ESOP’98, 7th European Symposium on Programming, Held as Part of ETAPS’98, volume 1381 of LNCS. Springer, 1998. ISBN-3-540-64302-8. doi:10.1007/BFb0053558.
  • [37] Hennessy M, Lin H. Symbolic Bisimulations. Theor. Comput. Sci., 1995. 138(2):353-389. doi:10.1016/0304-3975(94)00172-F.
  • [38] Calder M, Shankland C. A Symbolic Semantics and Bisimulation for Full LOTOS. In: Kim M, Chin B, Kang S, Lee D (eds.), FORTE 2001, volume 197 of IFIP Conference Proceedings. Kluwer. 2001 pp. 185-200. ISBN-0-7923-7470-3.
  • [39] Verdejo A. Building Tools for LOTOS Symbolic Semantics in Maude. In: Peled DA, Vardi MY (eds.), FORTE 2002, volume 2529 of LNCS. Springer 2002 pp. 292-307. ISBN-3-540-00141-7. doi:10.1007/3-540-36135-9_19.
  • [40] Saraswat VA, Rinard MC, Panangaden P. Semantic Foundations of Concurrent Constraint Programming. In: Wise DS (ed.), POPL 1991. ACM Press. 1991 pp. 333-352. ISBN-0-89791-419-8. doi:10.1145/99583.99627.
  • [41] Olarte C, Rueda C, Valencia FD. Models and emerging trends of concurrent constraint programming. Constraints, 2013. 18(4):535-578. doi:10.1007/s10601-013-9145-3.
  • [42] Rocha C, Meseguer J, Muñoz CA. Rewriting modulo SMT and open system analysis. J. Log. Algebr. Meth. Program., 2017. 86(1):269-297. doi:10.1016/j.jlamp.2016.10.001.
  • [43] Bodei C, Brodo L, Gori R, Levi F, Bernini A, Hermith D. A static analysis for Brane Calculi providing global occurrence counting information, Theor. Comput. Sci., 2017. 696:11-51. URL https://doi.org/10.1016/j.tcs.2017.07.008.
  • [44] Bernini A, Brodo L, Degano P, Falaschi M, Hermith D. Process calculi for biological processes, 2018. Natural Computing, 17(2):345-373. URL https://doi.org/10.1007/s11047-018-9673-2.
Uwagi
Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2020).
Typ dokumentu
Bibliografia
Identyfikator YADDA
bwmeta1.element.baztech-2f167cd7-8e35-44c0-bb4c-56c95063f535
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.