Skip to main content
SpringerLink
Log in

Modeling Distributed Algorithms by Abstract State Machines Compared to Petri Nets

  • Conference paper
  • First Online:
Book cover Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ 2016)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9675))

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.

This work was partially supported by the European Commission funded project BIOMICS, Grant no. 318202.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    See the use of modes in [23] as a means to structure the set of states.

  2. 2.

    \(diff(p,q) = orderNumber(p)-orderNumber(q)\) for processes numbered \(1,2,\ldots ,\) in increasing order.

  3. 3.

    Not to be confused with the issue of a global vs local state view.

  4. 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. 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. 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. 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. 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. 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. 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. 11.

    This is already a form of mutual exclusion. For a genuine solution of the mutual exclusion problem for multiple writers see [19].

  12. 12.

    For a prominent example see [22, p. 346]. [20] uses the assumption only for concurrent atomic read/write operations of single digits.

  13. 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. 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. 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. 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. 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. 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. 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.

References

  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)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  4. Börger, E.: The ASM refinement method. Formal Aspects Comput. 15, 237–257 (2003)

    Article  MATH  Google Scholar 

  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)

    Article  MATH  Google Scholar 

  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

    Google Scholar 

  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

    Google Scholar 

  8. Börger, E., Schewe, K.-D.: Concurrent Abstract State Machines. Acta Informatica, pp. 1–24 (2015). http://link.springer.com/article/10.1007/s00236-015-0249-7, doi:10.1007/s00236-015-0249-7

    Google Scholar 

  9. Börger, E., Stärk, R.F.: Abstract State Machines. A Method for High-LevelSystem Design and Analysis. Springer, Heidelberg (2003)

    Book  MATH  Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  12. Fleischmann, A., Schmidt, W., Stary, C., Obermeier, S., Börger, E.: Subject-Oriented Business Process Management. Springer, Heidelberg (2012). http://www.springer.com/978-3-642-32391-1

    Book  Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  16. Jensen, K., Kristensen, L.M.: Coloured Petri Nets. Springer, Heidelberg (2009)

    Book  MATH  Google Scholar 

  17. Kossak, F., et al.: A Rigorous Semantics for BPMN 2.0 Process Diagrams. Springer, Switzerland (2014)

    Book  Google Scholar 

  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)

    Chapter  Google Scholar 

  19. Lamport, L.: A new solution of Dijkstra’s concurrent programming problem. Commun. ACM 17(8), 453–455 (1974)

    Article  MathSciNet  MATH  Google Scholar 

  20. Lamport, L.: Concurrent reading and writing. Commun. ACM 20(11), 806–811 (1977)

    Article  MathSciNet  MATH  Google Scholar 

  21. Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978)

    Article  MATH  Google Scholar 

  22. Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann, Burlington (1996)

    MATH  Google Scholar 

  23. Parnas, D.L.: The use of precise documentation in software development. Tutorial at FM 2006, August 2006. http://fm06.mcmaster.ca/t8.htm

  24. Petri, C.A.: Kommunikation mit Automaten. PhD thesis, Institut für Instrumentelle Mathematik, Universität Bonn, Schriften des IMM Nr.2 (1962)

    Google Scholar 

  25. http://www.informatik.uni-hamburg.de/TGI/PetriNets/

  26. Priese, L.: Automata and concurrency. TCS 25, 221–265 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  27. Priese, L., Wimmel, H.: Theoretische Informatik. Petri-Netze. Springer, Heidelberg (2003)

    Book  MATH  Google Scholar 

  28. Reisig, W.: Elements of Distributed Algorithms. Springer, Heidelberg (1998)

    Book  MATH  Google Scholar 

  29. Stärk, R.F., Schmid, J., Börger, E.: Java and the Java Virtual Machine: Definition, Verification, Validation. Springer, Heidelberg (2001)

    Book  MATH  Google Scholar 

  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)

    Google Scholar 

  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

    Google Scholar 

Download references

Acknowledgement

I thank over a dozen of colleagues who read and commented upon the many previous versions of this paper; I do not mention names so that the entire responsibility of what is stated in this paper remains mine.

Author information

Authors and Affiliations

  1. Dipartimento di Informatica, Università di Pisa, 56125, Pisa, Italy

    Egon Börger

Authors
  1. Egon Börger
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Egon Börger .

Editor information

Editors and Affiliations

  1. University of Southampton, Southampton, United Kingdom

    Michael Butler

  2. Software Competence Center, Hagenberg, Austria

    Klaus-Dieter Schewe

  3. Software Competence Center, Hagenberg, Austria

    Atif Mashkoor

  4. Software Competence Center, Hagenberg, Austria

    Miklos Biro

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Börger, E. (2016). Modeling Distributed Algorithms by Abstract State Machines Compared to Petri Nets. In: Butler, M., Schewe, KD., Mashkoor, A., Biro, M. (eds) Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2016. Lecture Notes in Computer Science(), vol 9675. Springer, Cham. https://doi.org/10.1007/978-3-319-33600-8_1

Download citation

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

  • Published:

  • Publisher Name: Springer, Cham

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

  • Online ISBN: 978-3-319-33600-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation