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
Erschienen in:
Model Checking at Scale: Automated Air Traffic Control Design Space Exploration Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

BigraphER: Rewriting and Analysis Engine for Bigraphs

verfasst von : Michele Sevegnani, Muffy Calder

Erschienen in: Computer Aided Verification

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

BigraphER is a suite of open-source tools providing an efficient implementation of rewriting, simulation, and visualisation for bigraphs, a universal formalism for modelling interacting systems that evolve in time and space and first introduced by Milner. BigraphER consists of an OCaml library that provides programming interfaces for the manipulation of bigraphs, their constituents and reaction rules, and a command-line tool capable of simulating Bigraphical Reactive Systems (BRSs) and computing their transition systems. Other features are native support for both bigraphs and bigraphs with sharing, stochastic reaction rules, rule priorities, instantiation maps, parameterised controls, predicate checking, graphical output and integration with the probabilistic model checker PRISM.

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
Vorheriges Kapitel BFS-Based Model Checking of Linear-Time Properties with an Application on GPUs
Nächstes Kapitel Verification-Aided Debugging: An Interactive Web-Service for Exploring Error Witnesses
Fußnoten
1
Note that a model may have an infinite state space.
 
2
An instantiation map is a function associating each site in the right-hand side to sites in the left-hand side.
 
3
The reaction rules belonging to a reducible class are assumed confluent i.e. they yield the same result regardless of the order in which they are applied.
 
Literatur
1.
Bacci, G., Grohmann, D., Miculan, M.: \(\sf DBtk\): a toolkit for directed bigraphs. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol. 5728, pp. 413–422. Springer, Heidelberg (2009)CrossRef
2.
Benford, S., Rodden, T., Calder, M., Sevegnani, M.: On lions, impala, and bigraphs: modelling interactions in physical/virtual spaces. ACM Trans. Comput. Hum. Interact. (2016, in press)
3.
Birkedal, L., Damgaard, T.C., Glenstrup, A.J., Milner, R.: Matching of bigraphs. ENTCS 175(4), 3–19 (2007)MATH
4.
Boucebsi, R., Belala, F.: Towards a channels allocation scheme model for WMNs based on SBRS with sharing. In: Proceedings of MeMo 2015, p. 5 (2015)
5.
Calder, M., Koliousis, A., Sevegnani, M., Sventek, J.: Real-time verification of wireless home networks using bigraphs with sharing. Sci. Comput. Program. 80(Pt. B), 288–310 (2014)CrossRef
6.
Calder, M., Sevegnani, M.: Modelling IEEE 802.11 CSMA/CA RTS/CTS with stochastic bigraphs with sharing. Formal Aspects Comput. Sci. 26, 537–561 (2014)MathSciNetCrossRef
7.
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)CrossRef
8.
Ellson, J., Gansner, E.R., Koutsofios, L., North, S.C., Woodhull, G.: Graphviz - open source graph drawing tools. In: Mutzel, P., Jünger, M., Leipert, S. (eds.) GD 2001. LNCS, vol. 2265, p. 483. Springer, Heidelberg (2002)CrossRef
9.
Faithfull, A., Perrone, G., Hildebrandt, T.T.: Big Red: a development environment for bigraphs. In: Proceedings of GCM 2012, vol. 61 (2013)
10.
Gillespie, D.T.: Exact stochastic simulation of coupled chemical reactions. J. Phys. Chem. 81(25), 2340–2361 (1977)CrossRef
11.
Krivine, J., Milner, R., Troina, A.: Stochastic bigraphs. ENTCS 218, 73–96 (2008)MATH
12.
Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011)CrossRef
13.
Milner, R.: The Space and Motion of Communicating Agents. Cambridge University Press, Cambridge (2009)CrossRefMATH
14.
Pereira, E., Kirsch, C., Sengupta, R., Sousa, J.: BigActors - a model for structure-aware computation. In: 4th International Conference on Cyber-Physical Systems, pp. 199–208. ACM/IEEE (2013)
15.
Perrone, G., Debois, S., Hildebrandt, T.T.: A model checker for bigraphs. In: Proceedings of SAC 2012, pp. 1320–1325. ACM (2012)
16.
17.
Tseitin, G.S.: On the complexity of derivation in propositional calculus. Stud. Constr. Math. Math. Logic 2(115–125), 10–13 (1968)
18.
Tsigkanos, C., Pasquale, L., Ghezzi, C., Nuseibeh, B.: Ariadne: topology aware adaptive security for cyber-physical systems. In: ICSE 2015, vol. 2, pp. 729–732 (2015)
19.
Yu, L., Tsai, W.T., Wei, X., Gao, J., Hildebrandt, T., Guo, X.Q.: Modeling and analysis of mobile cloud computing based on bigraph theory. MobileCloud 2014, 67–76 (2014)
Metadaten
Titel
BigraphER: Rewriting and Analysis Engine for Bigraphs
verfasst von
Michele Sevegnani
Muffy Calder
Copyright-Jahr
2016
Buch
Computer Aided Verification

Print ISBN: 978-3-319-41539-0

Electronic ISBN: 978-3-319-41540-6

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-41540-6_27