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:
Buchtitelbild

2016 | OriginalPaper | Buchkapitel

Modeling Distributed Algorithms by Abstract State Machines Compared to Petri Nets

verfasst von : Egon Börger

Erschienen in: Abstract State Machines, Alloy, B, TLA, VDM, and Z

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

We show how to model distributed algorithms by Abstract State Machines (ASMs). Comparing these models with Petri nets (PNs) reveals a certain number of idiosyncrasies of PNs which complicate both model design and analysis. The ASMs we define illustrate how one can avoid such framework related technicalities.

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
Nächstes Kapitel A Universal Control Construct for Abstract State Machines
Fußnoten
1
See the use of modes in [23] as a means to structure the set of states.
 
2
\(diff(p,q) = orderNumber(p)-orderNumber(q)\) for processes numbered \(1,2,\ldots ,\) in increasing order.
 
3
Not to be confused with the issue of a global vs local state view.
 
4
The problem to separate business from coordination logic triggered a similar observation in [18, p. 133] that in a PN “every component must be modeled explicitly”.
 
5
One would expect that using colored tokens [16] may help, but the tokens in [28] are already of a most general nature, namely elements of abstract domains (represented by first-order logical terms) which comprise colored tokens.
 
6
We disregard here the peculiar (global overall process view triggered?) design decision in Fig. 30.1 where the slaves organize the refusal case among themselves, triggering (via c) the master to eventually return to idle (via f), without further master involvement: no slave ‘reports ... refusal to the master’ and never ‘the master sends a cancellation to each slave’, contrary to the formulated requirements [28, p. 30].
 
7
Compare this with the “illustration of the power of decomposition methods in enabling simple descriptions (and proofs) of complicated distributed algorithms” in [22], quote from p. 532.
 
8
We interprete ‘may cause’ as ‘causes’; otherwise add \(\mathrel {\mathbf {choose}}s \in \{swap, noSwap\} \mathrel {\mathbf {in}}~ \mathrel {\mathbf {if}}s=swap \mathrel {\mathbf {then}}\)   Swap to Answer.
 
9
The protocol specification does not include a specification of the communication medium. It seems to be another example for PN Idiosyncrasy 2 that Fig. 27.7, 28.1, 28.2 also define the possible message loss by the transmission lines as an internal nondeterministic action of the PN. Message loss is not an action of the protocol agents but of the communication medium.
 
10
[22, p. 280] has a similar nondeterministic choice for the order in which the processes write the shared \(stickAt_1\) (there called turn) location, a nondeterminism resulting from the interleaving assumption of the underlying asynchronous shared memory I/O automata execution model. But this extraneous nondeterminism could easily be avoided the same way as in the ASM model.
 
11
This is already a form of mutual exclusion. For a genuine solution of the mutual exclusion problem for multiple writers see [19].
 
12
For a prominent example see [22, p. 346]. [20] uses the assumption only for concurrent atomic read/write operations of single digits.
 
13
See [21, p. 561] for a distributed mutual exclusion algorithm which deals with the case where the order matters in which requests for the resource are made.
 
14
See the observation in [11, p. 3]: “The core issue of Petri nets is that they model behavioral aspects of distributed systems, i.e., systems with components that are locally separated and communicate with each other. Surprisingly, neither components nor any notion of locality appears with the usual definition of a Petri net”.
 
15
Note that at the time of Petri’s doctoral thesis [24] computers were monolithic mainframes, there were no agents interacting via pools of networks, servers, services, etc.
 
16
In [28, p. V] it is even suggested that “The hurried reader may just study the pictures”! See also the analysis in [11, p. 2] where the characteristics that “Petri nets are a graphical notion and at the same time a precise mathematical notion” are taken as “the most important properties”.
 
17
Right before sending this paper for the Proceedings Klaus-Dieter Schewe and myself discovered that distributed PN runs are distributed ASM runs in the sense of Gurevich [13]. A further investigation of the consequences of this surprising fact remains to be done.
 
18
In [7] ASM nets are defined through which IBM’s Guard-State-Milestone approach [15] to BPM can be equipped with the systematic ASM refinement method.
 
19
Idiosyncrasies 3 and 3b which do speak about graphical PN features however discuss only possible deficiencies of PN diagrams; they are not related to flowcharts.
 
Literatur
1.
Börger, E.: Computability, Complexity, Logic (English translation of “Berechenbarkeit, Komplexität, Logik", Vieweg-Verlag 1985). Studies in Logic and the Foundations of Mathematics, vol. 128, North-Holland (1989)
2.
Börger, E.: The origins and the development of the ASM method for high-level system design and analysis. J. Univ. Comput. Sci. 8(1), 2–74 (2002)
3.
Börger, E.: The ASM ground model method as a foundation of requirements engineering. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 145–160. Springer, Heidelberg (2004)CrossRef
4.
5.
Börger, E.: Construction and analysis of ground models and their refinements as a foundation for validating computer based systems. Formal Aspects Comput. 19, 225–241 (2007)CrossRefMATH
6.
Börger, E.: The abstract state machines method for modular design and analysis of programming languages. J. Logic Comput (2014). Special Issue Concepts and Meaning (Leitsch Festschrift). First published online 18 December 2014. doi:10.​1093/​logcom/​exu077
7.
Börger, E., Fleischmann, A.: Abstract state machine nets. closing the gap between business process models and their implementation. In: Proceeding S-BPM ONE 2015, ACM Digital Library. ACM, April 2015. ISBN 978-1-4503-3312-2
8.
9.
Börger, E., Stärk, R.F.: Abstract State Machines. A Method for High-LevelSystem Design and Analysis. Springer, Heidelberg (2003)CrossRefMATH
10.
Cohn, D., Hull, R.: Business artifacts: a data-centric approach to modeling business operations and processes. IEEE Data Eng. Bull. 32, 3–9 (2009)
11.
Desel, J., Juhás, G.: What is a Petri Net? In: Ehrig, H., Juhás, G., Padberg, J., Rozenberg, G. (eds.) APN 2001. LNCS, vol. 2128, pp. 1–25. Springer, Heidelberg (2001)CrossRef
12.
13.
Gurevich, Y.: Evolving algebras 1993: lipari guide. In: Börger, E. (ed.) Specification and Validation Methods, pp. 9–36. Oxford University Press, Oxford, (1995)
14.
Hense, A.V., Malz, R.: Comparison of the subject-oriented and the Petri net based approach for business process automation. In: S-BPM ONE 2015. ACM (2015)
15.
Hull, R., et al.: Introducing the guard-stage-milestone approach for specifying business entity lifecycles (invited talk). In: Bravetti, M. (ed.) WS-FM 2010. LNCS, vol. 6551, pp. 1–24. Springer, Heidelberg (2011)CrossRef
16.
17.
Kossak, F., et al.: A Rigorous Semantics for BPMN 2.0 Process Diagrams. Springer, Switzerland (2014)CrossRef
18.
Kühn, E., Craß, S., Joskowicz, G., Marek, A., Scheller, T.: Peer-based programming model for coordination patterns. In: De Nicola, R., Julien, C. (eds.) COORDINATION 2013. LNCS, vol. 7890, pp. 121–135. Springer, Heidelberg (2013)CrossRef
19.
20.
21.
Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978)CrossRefMATH
22.
Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann, Burlington (1996)MATH
23.
24.
Petri, C.A.: Kommunikation mit Automaten. PhD thesis, Institut für Instrumentelle Mathematik, Universität Bonn, Schriften des IMM Nr.2 (1962)
25.
26.
27.
Priese, L., Wimmel, H.: Theoretische Informatik. Petri-Netze. Springer, Heidelberg (2003)CrossRefMATH
28.
29.
Stärk, R.F., Schmid, J., Börger, E.: Java and the Java Virtual Machine: Definition, Verification, Validation. Springer, Heidelberg (2001)CrossRefMATH
30.
Winskel, G., Nielsen, M.: Models for concurrency. Handbook of Logic and the Foundations of Computer Science. Semantic Modelling, pp. 1–148. Oxford University Press, Oxford (1995)
31.
Zunino, R., Nikolic, \(\text{-}\!\!\text{D }\)., Priami, C., Kahramanogullari, O., Schiavinotto, T.: \(\ell \): an imperative DSL to stochastically simulate biological systems. In: Bodei, C., Ferrari, G.-L., Priami, C. (eds.) Degano Festschrift. LNCS, vol. 9465, pp. 354–374. Springer, Heidelberg (2015). doi:10.​1007/​978-3-319-25527-9_​23
Metadaten
Titel
Modeling Distributed Algorithms by Abstract State Machines Compared to Petri Nets
verfasst von
Egon Börger
Copyright-Jahr
2016
Buch
Abstract State Machines, Alloy, B, TLA, VDM, and Z

Print ISBN: 978-3-319-33599-5

Electronic ISBN: 978-3-319-33600-8

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-33600-8_1