SpringerLink
Log in

Specification of Asynchronous Component Systems with Modal I/O-Petri Nets

  • Conference paper
  • First Online:
Trustworthy Global Computing (TGC 2013)

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

Included in the following conference series:

  • 563 Accesses

Abstract

Modal transition systems are an elegant way to formalise the design process of a system through refinement and composition. Here we propose to adapt this methodology to asynchronous composition via Petri nets. The Petri nets that we consider have distinguished labels for inputs, outputs, internal communications and silent actions and “must” and “may” modalities for transitions. The input/output labels show the interaction capabilities of a net to the outside used to build larger nets by asynchronous composition via communication channels. The modalities express constraints for Petri net refinement taking into account observational abstraction from silent transitions. Modal I/O-Petri nets are equipped with a modal transition system semantics. We show that refinement is preserved by asynchronous composition and by hiding of communication channels. We study compatibility properties which express communication requirements for composed systems and we show that these properties are decidable, they are preserved in larger contexts and also by modal refinement. On this basis we propose a methodology for the specification of distributed systems in terms of modal I/O-Petri nets which supports incremental design, encapsulation of components, stepwise refinement and independent implementability.

This work has been partially sponsored by the EU project ASCENS, 257414.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
EUR 29.95
Price includes VAT (Germany)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
EUR 42.79
Price includes VAT (Germany)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
EUR 53.49
Price includes VAT (Germany)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    \(\mathrm {val} (q)[a\mathrm {++}]\) (\(\mathrm {val} (q)[a\mathrm {--}]\) resp.) denotes the update of \(\mathrm {val} \) which increments (decrements) the value of \(a\) and leaves the values of all other channels unchanged.

  2. 2.

    i.e. there is a transition in \(\rho \) labelled by \({}^{\rhd }{a}\).

References

  1. de Alfaro, L., Henzinger, T.A.: Interface-based design. Engineering Theories of Software-intensive Systems, NATO Science Series: Mathematics, Physics, and Chemistry, vol. 195. Springer, pp. 83–104 (2005)

    Google Scholar 

  2. Beneš, N., Křetínský, J.: Modal process rewrite systems. In: Proceedings of the International Conference on Theoretical Aspects of Computing (ICTAC 2012), vol. LNCS 7521, pp 120–135, Springer (2012)

    Google Scholar 

  3. Bernardo, M., Ciancarini, P., Donatiello, L.: Architecting families of software systems with process algebras. ACM Trans. Softw. Eng. Meth. 11(4), 386–426 (2002)

    Article  Google Scholar 

  4. Bérard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P.: Systems and Software Verification: Model-Cheking Techniques and Tools. Springer, Heidelberg (2001)

    Google Scholar 

  5. Best, E., Devillers, R., Koutny, M.: Petri Net Algebra. Springer Monographs in Theoretical Computer Science (2001)

    Google Scholar 

  6. Brauer, W., Gold, R., Vogler, W.: A survey of behaviour and equivalence preserving refinements of Petri nets. Applications and Theory of Petri Nets, pp. 1–46 (1989)

    Google Scholar 

  7. Elhog-Benzina, D., Haddad, S., Hennicker, R.: Refinement and asynchronous composition of modal Petri Nets. In: Jensen, K., Donatelli, S., Kleijn, J. (eds.) Transactions on Petri Nets and Other Models of Concurrency V. LNCS, vol. 6900, pp. 96–120. Springer, Heidelberg (2012)

    Google Scholar 

  8. Ganty, P., Raskin, J.-F., Van Begin, L.: From many places to few: automatic abstraction refinement for Petri Nets, ATPN 2007. LNCS 4546, 124–143 (2007)

    Google Scholar 

  9. Haddad, S., Hennicker, R., Møller, M.H.: Channel properties of asynchronously composed Petri Nets. In: Colom, J.-M., Desel, J. (eds.) Petri Nets 2013. LNCS, vol. 7927, pp. 369–388. Springer, Heidelberg (2013)

    Google Scholar 

  10. Haddad, S., Hennicker, R., Møller, M.H.: Channel properties of asynchronously composed Petri Nets. Research Report LSV-13-05, Laboratoire Spécification et Vérification, ENS Cachan, France (2013)

    Google Scholar 

  11. Haddad, S., Hennicker, R., Møller, M.H.: Specification of asynchronous component systems with modal I/O-Petri Nets. Research Report LSV-13-16, Laboratoire Spécification et Vérification. ENS Cachan, France (2013)

    Google Scholar 

  12. Hennicker, R., Knapp, A.: Modal interface theories for communication-safe component assemblies. In: Cerone, A., Pihlajasaari, P. (eds.) ICTAC 2011. LNCS, vol. 6916, pp. 135–153. Springer, Heidelberg (2011)

    Google Scholar 

  13. Hüttel, H., Larsen, K.G.: The use of static constructs in a modal process logic. In: Logic at Botik 1989, pp. 163–180 (1989)

    Google Scholar 

  14. Jancar, P.: Undecidability of bisimilarity for Petri Nets and related problems. Theor. Comput. Sci. 148, 281–301 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  15. Larsen, K.G., Thomsen, B.; A modal process logic. In: 3rd Annual Symposium on Logic in Computer Science (LICS), IEEE Computer Society, pp. 203–210 (1988)

    Google Scholar 

  16. Lohmann, N., Massuthe, P., Wolf, K.: Operating guidelines for finite-state services. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol. 4546, pp. 321–341. Springer, Heidelberg (2007)

    Google Scholar 

  17. Raclet, J.-B.: Residual for component specifications. In: Proceedings of the 4th International Workshop on Formal Aspects of Component Software (FACS07), Sophia-Antipolis, France (2007)

    Google Scholar 

  18. Reisig, W.: Simple composition of nets. In: Franceschinis, G., Wolf, K. (eds.) Petri Nets 2009. LNCS, vol. 5606, pp. 23–42. Springer, Heidelberg (2009)

    Google Scholar 

  19. Schäfer, M., Vogler, W.: Component refinement and CSC-solving for STG decomposition. Theor. Comput. Sci. 388(1–3), 243–266 (2007)

    Article  MATH  Google Scholar 

  20. Souissi, Y.: On liveness preservation by composition of nets via a set of places. In: 11th International Conference on Applications and Theory of Petri Nets, LNCS 524, pp. 277–295 (1990)

    Google Scholar 

  21. Souissi, Y., Memmi, G.: Composition of nets via a communication medium. In: 10th International Conference on Applications and Theory of Petri Nets, LNCS 483, pp. 457–470 (1989)

    Google Scholar 

  22. Stahl, C., Wolf, K.: Deciding service composition and substitutability using extended operating guidelines. Data Knowl. Eng. 68(9), 819–833 (2009)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LSV, ENS Cachan & CNRS & Inria, Cachan, France

    Serge Haddad

  2. Ludwig-Maximilians-Universität München, Munich, Germany

    Rolf Hennicker

  3. Aalborg University, Aalborg, Denmark

    Mikael H. Møller

Authors
  1. Serge Haddad
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Rolf Hennicker
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Mikael H. Møller
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Serge Haddad .

Editor information

Editors and Affiliations

  1. Microsoft Research, Mountain View, California, USA

    Martín Abadi

  2. IMT Institute for Advanced Studies, Lucca, Italy

    Alberto Lluch Lafuente

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Haddad, S., Hennicker, R., Møller, M.H. (2014). Specification of Asynchronous Component Systems with Modal I/O-Petri Nets. In: Abadi, M., Lluch Lafuente, A. (eds) Trustworthy Global Computing. TGC 2013. Lecture Notes in Computer Science(), vol 8358. Springer, Cham. https://doi.org/10.1007/978-3-319-05119-2_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-05119-2_13

  • Published:

  • Publisher Name: Springer, Cham

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

  • Online ISBN: 978-3-319-05119-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation