Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
International Journal on Software Tools for Technology Transfer
Erschienen in: International Journal on Software Tools for Technology Transfer 5/2016

01.10.2016 | PV 2014

A unified view of parameterized verification of abstract models of broadcast communication

verfasst von: Giorgio Delzanno

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 5/2016

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

We give a unified view of different parameterized models of concurrent and distributed systems with broadcast communication based on transition systems. Based on the resulting formal models, we discuss related verification methods and tools based on abstractions and symbolic state exploration.
Vorheriger Artikel Parameterized verification
Nächster Artikel Parameterized verification through view abstraction

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Literatur
1.
Abdulla, P., Delzanno, G.: Constrained multiset rewriting. In AVIS 06, (2006)
2.
3.
Abdulla, P.A., Atig, M.F., Kara, A., Rezine, O.: Verification of dynamic register automata. In: 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014, December 15–17, 2014, New Delhi, India, pp. 653–665, (2014)
4.
Abdulla, P.A., Atig, M.F., Rezine, O.: Verification of directed acyclic ad hoc networks. In: FMOODS/FORTE, pp. 193–208 (2013)
5.
Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27–30, 1996, pp. 313–321 (1996)
6.
Abdulla, P.A., Delzanno, G., Van Begin, L.: A classification of the expressive power of well-structured transition systems. Inf. Comput. 209(3), 248–279 (2011)MathSciNetCrossRefMATH
7.
Abdulla, P.A., Delzanno, G., Ben, N.: Henda, and A. Rezine. Monotonic abstraction: on efficient verification of parameterized systems. Int. J. Found. Comput. Sci. 20(5), 779–801 (2009)CrossRefMATH
8.
Abdulla, P.A., Delzanno, G., Rezine, A.: Approximated parameterized verification of infinite-state processes with global conditions. Formal Methods Syst. Des. 34(2), 126–156 (2009)CrossRefMATH
9.
Abdulla, P.A., Delzanno, G., Rezine, A.: Automatic verification of directory-based consistency protocols with graph constraints. Int. J. Found. Comput. Sci. 22(4) (2011)
10.
Abdulla, P.A., Delzanno, G., Rezine, O., Sangnier, A., Traverso, R.: On the verification of timed ad hoc networks. In: Formal Modeling and Analysis of Timed Systems - 9th International Conference, FORMATS 2011, Aalborg, Denmark, September 21–23, 2011. Proceedings, pp. 256–270 (2011)
11.
Abdulla, P.A., Haziza, F., Holík, L.: All for the price of few. In: Verification, Model Checking, and Abstract Interpretation, 14th International Conference, VMCAI 2013, Rome, Italy, January 20–22, 2013. Proceedings, pp. 476–495 (2013)
12.
Abdulla, P.A., Haziza, F., Holík, L.: Block me if you can! - context-sensitive parameterized verification. In: Static Analysis - 21st International Symposium, SAS 2014, Munich, Germany, September 11-13, 2014. Proceedings, pp. 1–17 (2014)
13.
Abdulla, P.A., Ben Henda, N., Delzanno, G., Rezine, A.: Handling parameterized systems with non-atomic global conditions. In VMCAI’08, volume 4905 of LNCS, pp. 22–36. Springer (2008)
14.
Abdulla, P.A., Jonsson, B.: Undecidable verification problems for programs with unreliable channels. Inf. Comput. 130(1), 71–90 (1996)MathSciNetCrossRefMATH
15.
Abdulla, P.A., Jonsson, B.: Verifying networks of timed processes (extended abstract). In: Tools and Algorithms for Construction and Analysis of Systems, 4th International Conference, TACAS ’98, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS’98, Lisbon, Portugal, March 28 – April 4, 1998, Proceedings, pp. 298–312 (1998)
16.
Abdulla, P.A., Jonsson, B.: Ensuring completeness of symbolic verification methods for infinite-state systems. Theor. Comput. Sci. 256(1–2), 145–167 (2001)MathSciNetCrossRefMATH
17.
Abdulla, P.A., Nylén, A.: Better is better than well: On efficient verification of infinite-state systems. In: 15th Annual IEEE Symposium on Logic in Computer Science, Santa Barbara, California, USA, June 26–29, 2000, pp. 132–140 (2000)
18.
Abdulla, P.A., Delzanno, G., Rezine, A.: Monotonic abstraction in action. In: Theoretical Aspects of Computing - ICTAC 2008, 5th International Colloquium, Istanbul, Turkey, September 1–3, 2008. Proceedings, pp. 50–65 (2008)
19.
Alberti, F., Ghilardi, S., Pagani, E., Ranise, S., Rossi, G.P.: Automated support for the design and validation of fault tolerant parameterized systems: a case study. ECEASST 35 (2010)
20.
Aminof, B., Kotek, T., Rubin, S., Spegni, F., Veith H., Parameterized model checking of rendezvous systems. In: CONCUR 2014 - Concurrency Theory - 25th International Conference, CONCUR 2014, Rome, Italy, September 2–5, 2014. Proceedings, pp. 109–124 (2014)
21.
Apt, K.R., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 307–309 (1986)
22.
Ball, T., Chaki, S., Rajamani, S.K.: Parameterized verification of multithreaded software libraries. In: Tools and Algorithms for the Construction and Analysis of Systems, (TACAS 2001) pp. 158–173 (2001)
23.
Bardin, Sébastien: Finkel, Alain, Leroux, Jérôme, Petrucci, Laure: FAST: acceleration from theory to practice. STTT 10(5), 401–424 (2008)CrossRef
24.
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, pp. 101–116 (2012)
25.
Bertrand N., Fournier, P.: Parameterized verification of many identical probabilistic timed processes. In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2013, December 12–14, 2013, Guwahati, India, pp. 501–513 (2013)
26.
Bertrand, N., Fournier, P., Sangnier, A.: Playing with probabilities in reconfigurable broadcast networks. In: Foundations of Software Science and Computation Structures - 17th International Conference, FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5–13, 2014, Proceedings, pp. 134–148 (2014)
27.
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, pp. 44–57 (2015)
28.
R. Bonnet. The reachability problem for vector addition system with one zero-test. In Mathematical Foundations of Computer Science 2011-36th International Symposium, MFCS 2011, Warsaw, Poland, August 22–26, 2011. Proceedings, pp. 145–157 (2011)
29.
Bonnet, R., Finkel, A., Haddad, S., Rosa-Velardo, F.: Ordinal theory for expressiveness of well-structured transition systems. Inf. Comput. 224, 1–22 (2013)MathSciNetCrossRefMATH
30.
Bozzano, M., Delzanno, G.: Beyond parameterized verification. In: Tools and Algorithms for the Construction and Analysis of Systems, 8th International Conference, TACAS 2002, Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8–12, 2002, Proceedings, pp. 221–235 (2002)
31.
Bozzano, M., Delzanno, G.: Automatic verification of secrecy properties for linear logic specifications of cryptographic protocols. J. Symb. Comput. 38(5), 1375–1415 (2004)MathSciNetCrossRefMATH
32.
Bozzelli, L., Pinchinat, S.: Verification of gap-order constraint abstractions of counter systems. Theor. Comput. Sci. 523, 1–36 (2014)MathSciNetCrossRefMATH
33.
Browne, M.C., Clarke, E.M.: Grumberg, Orna: Reasoning about networks with many identical finite state processes. Inf. Comput. 81(1), 13–31 (1989)MathSciNetCrossRefMATH
34.
Clarke, E.M., Talupur, M., Veith, H.: Environment abstraction for parameterized verification. In: Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8–10, 2006, Proceedings, pp. 126–141 (2006)
35.
36.
David, N., Jard, C., Lime, D., Roux, O.H.: Discrete parameters in Petri nets. In: Application and Theory of Petri Nets and Concurrency - 36th International Conference, PETRI NETS 2015, Brussels, Belgium, June 21–26, 2015, Proceedings, pp. 137–156 (2015)
37.
Delzanno, G.: An overview of msr(c): A clp-based framework for the symbolic verification of parameterized concurrent systems. Electr. Notes Theor. Comput. Sci. 76, 65–82 (2002)CrossRef
38.
Delzanno, G.: Constraint-based verification of parameterized cache coherence protocols. Formal Methods Syst. Des. 23(3), 257–301 (2003)CrossRefMATH
39.
Delzanno, G.: Constraint-based automatic verification of abstract models of multithreaded programs. TPLP 7(1–2), 67–91 (2007)MathSciNetMATH
40.
Delzanno, G., Esparza, J., Podelski, A.: Constraint-based analysis of broadcast protocols. In: CSL’99, volume 1683 of LNCS, pp. 50–66. Springer (1999)
41.
Delzanno, G., Ganty, P.: Automatic verification of time sensitive cryptographic protocols. In: Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 – April 2, 2004, Proceedings, pp. 342–356 (2004)
42.
Delzanno, G., Di, C., Giusto, Gabbrielli, M., Laneve, C., Zavattaro, G.: The kappa-lattice: Decidability boundaries for qualitative analysis in biological languages. In: CMSB, pp. 158–172 (2009)
43.
Delzanno, G., Raskin, J.-F., Van Begin, L.: Towards the automated verification of multithreaded java programs. In: Tools and Algorithms for the Construction and Analysis of Systems, 8th International Conference, TACAS 2002, Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8–12, 2002, Proceedings, pp. 173–187 (2002)
44.
Delzanno, G., Raskin, J.-F., Van Begin, L.: Covering sharing trees: a compact data structure for parameterized verification. STTT 5(2–3), 268–297 (2004)CrossRef
45.
Delzanno, G., Rosa-Velardo, F.: On the coverability and reachability languages of monotonic extensions of petri nets. Theor. Comput. Sci. 467, 12–29 (2013)MathSciNetCrossRefMATH
46.
Delzanno, G., Sangnier, A., Traverso, R.: Parameterized verification of broadcast networks of register automata. In: RP, pp. 109–121 (2013)
47.
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, pp. 289–300 (2012)
48.
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, pp. 313–327 (2010)
49.
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, pp. 441–455 (2011)
50.
Delzanno, G., Sangnier, A., Zavattaro, G.: Verification of ad hoc networks with node and communication failures. In FORTE/FMOODS’12, volume 7273 of LNCS, pp. 235–250. Springer (2012)
51.
Delzanno, G., Traverso, R.: Decidability and complexity results for verification of asynchronous broadcast networks. In LATA, pp. 238–249 (2013)
52.
Delzanno, Giorgio: Rezine, Ahmed: A lightweight regular model checking approach for parameterized systems. STTT 14(2), 207–222 (2012)CrossRef
53.
Dickson, L.E.: Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors. Am. J. Math. 35(4), 413–422 (1913)MathSciNetCrossRefMATH
54.
55.
Dufourd, C., Finkel, A., Schnoebelen, P.: Reset nets between decidability and undecidability. In Automata, Languages and Programming, 25th International Colloquium, ICALP’98, Aalborg, Denmark, July 13–17, 1998, Proceedings, pp. 103–115 (1998)
56.
Emerson, E.A., Kahlon, V.: Exact and efficient verification of parameterized cache coherence protocols. In Correct Hardware Design and Verification Methods, 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L’Aquila, Italy, October 21–24, 2003, Proceedings, pp. 247–262 (2003)
57.
Emerson, E.A., Namjoshi, K.S.: 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, pp. 70–80 (1998)
58.
Emerson, E. Allen, Kahlon, V.: Parameterized model checking of ring-based message passing systems. In Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20–24, 2004, Proceedings, pp. 325–339 (2004)
59.
Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999, pp. 352–359 (1999)
60.
Esparza, J., Ganty, P., Majumdar, R.: Parameterized verification of asynchronous shared-memory systems. In Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13–19, 2013. Proceedings, pp. 124–140 (2013)
61.
Esparza, J., Ledesma-Garza, R., Majumdar, R., Meyer, P., Niksic, F.: An smt-based approach to coverability analysis. In Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18–22, 2014. Proceedings, pp. 603–619 (2014)
62.
Farzan, A., Kincaid, Z., Podelski, A.: Proofs that count. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20–21, 2014, pp. 151–164 (2014)
63.
Farzan, A., Kincaid, Z., Podelski, A.: Proof spaces for unbounded parallelism. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15–17, 2015, pp. 407–420 (2015)
64.
Finkel, A., Geeraerts, G., Raskin, J.-F., Van Begin, L.: On the omega-language expressive power of extended Petri nets. Electr. Notes Theor. Comput. Sci. 128(2), 87–101 (2005)CrossRefMATH
65.
Finkel, A., McKenzie, P., Picaronny, C.: A well-structured framework for analysing petri net extensions. Inf. Comput. 195(1–2), 1–29 (2004)MathSciNetCrossRefMATH
66.
67.
Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V.: Improving reachability analysis of infinite state systems by specialization. Fundam. Inform. 119(3–4), 281–300 (2012)MathSciNetMATH
68.
Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V.: Generalization strategies for the verification of infinite state systems. TPLP 13(2), 175–199 (2013)MathSciNetMATH
69.
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, pp. 396–408 (2014)
70.
Geeraerts, G., Raskin, J.-F., Van Begin, L.: Expand, enlarge and check: New algorithms for the coverability problem of WSTS. J. Comput. Syst. Sci. 72(1), 180–203 (2006)MathSciNetCrossRefMATH
71.
72.
73.
Ghilardi, S., Ranise, S.: Backward reachability of array-based systems by SMT solving: Termination and invariant synthesis. Logical Methods Comput Sci 6(4) (2010)
74.
Gmeiner, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Tutorial on parameterized model checking of fault-tolerant distributed algorithms. In Formal Methods for Executable Software Models - 14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2014, Bertinoro, Italy, June 16–20, 2014, Advanced Lectures, pp. 122–171 (2014)
75.
Higman, G.: Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society, 3(2 (7)):326–336 (1952)
76.
Joshi, S., König, B.: Applying the graph minor theorem to the verification of graph transformation systems. In CAV’08, volume 5123 of LNCS, pp. 214–226. Springer (2008)
77.
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, pp. 141–155 (2014)
78.
Kaiser, A., Kroening, D.: Wahl, Thomas: A widening approach to multithreaded program verification. ACM Trans. Program. Lang. Syst. 36(4), 14 (2014)CrossRef
79.
80.
81.
Kloos, J., Majumdar, R., Niksic, F., Piskac, R.: Incremental, inductive coverability. In Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13–19, 2013. Proceedings, pp. 158–173 (2013)
82.
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. 211, 201–210 (2008)CrossRef
83.
Kroening, D.: Automated verification of concurrent software. In: Reachability Problems - 7th International Workshop, RP 2013, Uppsala, Sweden, September 24-26, 2013 Proceedings, pp. 19–20 (2013)
84.
Lazic, R., Newcomb, T., Ouaknine, J., Roscoe, A.W., Worrell, J.: Nets with tokens which carry data. Fundam. Inf. 88(3), 251–274 (2008)MathSciNetMATH
85.
Leroux, J.: The general vector addition system reachability problem by presburger inductive invariants. Logical Methods Comput. Sci. 6(3) (2010)
86.
Leroux, J.: Vector addition systems reachability problem (A simpler solution). In Turing-100 - The Alan Turing Centenary, Manchester, UK, June 22–25, 2012, pp. 214–228 (2012)
87.
Lipton, R.: The reachability problem requires exponential space (1975)
88.
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, pp. 155–162 (2014)
89.
Martos-Salgado, M., Rosa-Velardo, F.: Expressiveness of dynamic networks of timed Petri nets. In Language and Automata Theory and Applications - 8th International Conference, LATA 2014, Madrid, Spain, March 10–14, 2014. Proceedings, pp. 516–527 (2014)
90.
91.
McMillan, K.L.: Parameterized verification of the FLASH cache coherence protocol by compositional model checking. In Correct Hardware Design and Verification Methods, 11th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2001, Livingston, Scotland, UK, September 4–7, 2001, Proceedings, pp. 179–195 (2001)
92.
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, pp. 175–179 (2010)
93.
Pnueli, A., Xu, J., Zuck, L.D.: Liveness with (0, 1, infty)-counter abstraction. In Computer Aided Verification, 14th International Conference, CAV 2002, Copenhagen, Denmark, July 27–31, 2002, Proceedings, pp. 107–122 (2002)
94.
Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Program. Lang. Syst. 22(2), 416–430 (2000)CrossRef
95.
Reinhardt, K.: Reachability in Petri nets with inhibitor arcs. Electr. Notes Theor. Comput. Sci. 223, 239–264 (2008)CrossRefMATH
96.
Revesz, P.Z.: A closed-form evaluation for datalog queries with integer (gap)-order constraints. Theor. Comput. Sci. 116(1), 117–149 (1993)MathSciNetCrossRefMATH
97.
Rosa-Velardo, F., de Frutos-Escrig, D.: Decidability results for restricted models of Petri nets with name creation and replication. In Applications and Theory of Petri Nets (PETRI NETS 2009), pp. 63–82 (2009)
98.
Rosa-Velardo, F., de Frutos-Escrig, D.: Decidability and complexity of Petri nets with unordered data. Theor. Comput. Sci. 412(34), 4439–4451 (2011)MathSciNetCrossRefMATH
99.
Saksena, M., Wibling, O., Jonsson, B.: Graph grammar modeling and verification of ad hoc routing protocols. In TACAS, pp. 18–32 (2008)
100.
Schnoebelen, P.: Revisiting ackermann-hardness for lossy counter machines and reset Petri nets. In Mathematical Foundations of Computer Science 2010, 35th International Symposium, MFCS 2010, Brno, Czech Republic, August 23–27, 2010. Proceedings, pp. 616–628 (2010)
101.
Singh, A., Ramakrishnan, C.R., Smolka, S.A.: Query-based model checking of ad hoc network protocols. In CONCUR, pp. 603–619 (2009)
102.
Singh, A., Ramakrishnan, C.R., Smolka, S.A.: A process calculus for mobile ad hoc networks. Sci. Comput. Program. 75(6), 440–469 (2010)MathSciNetCrossRefMATH
103.
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, pp. 266–274 (2015)
104.
105.
106.
107.
108.
109.
110.
111.
112.
113.
114.
115.
Metadaten
Titel
A unified view of parameterized verification of abstract models of broadcast communication
verfasst von
Giorgio Delzanno
Publikationsdatum
01.10.2016
Verlag
Springer Berlin Heidelberg
Erschienen in
International Journal on Software Tools for Technology Transfer / Ausgabe 5/2016
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-016-0412-7

Weitere Artikel der Ausgabe 5/2016

International Journal on Software Tools for Technology Transfer 5/2016 Zur Ausgabe

PV 2014

Parameterized model checking for security policy analysis

PV 2014

Counting dynamically synchronizing processes

PV 2014

Soundness of data-aware, case-centric processes

PV 2014

Parameterized verification through view abstraction

Introduction

Parameterized verification