iBet uBet web content aggregator. Adding the entire web to your favor.
iBet uBet web content aggregator. Adding the entire web to your favor.



Link to original content: https://doi.org/10.1007/978-3-030-61470-6_14
A Dynamic Logic for Systems with Predicate-Based Communication | SpringerLink
Skip to main content
Springer Nature Link
Log in

A Dynamic Logic for Systems with Predicate-Based Communication

  • Conference paper
  • First Online:
Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles (ISoLA 2020)

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

Included in the following conference series:

Abstract

Attribute-based broadcast communication is a novel para-digm for modelling interactions in collective systems. Used by several new languages (such as SCEL, CARMA, and AbC), it enables senders and groups of receivers to interact by considering predicates over their current attribute values. In these languages systems are modelled by the parallel composition of components, each component being equipped with a local process description. In this paper we complement this local view by a global requirements specification format that allows us to specify abstract properties, like safety and liveness, as well as allowed and forbidden interaction scenarios. We propose a first-order dynamic logic whose atomic actions are tailored to the needs of systems of collaborating components with multi-cast communication. As implementation language we consider (a variant of) the AbC calculus and show how our global ensemble specifications can be realised with local process declarations. Our correctness notion relates the semantics of global specifications to the labelled transition system semantics of AbC systems.

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
$34.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
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

Similar content being viewed by others

Notes

  1. 1.

    We do not allow here that the set of existing component instances can change during a state transition. This could, however, be incorporated along the lines of  [11, 14]. The other parts of a component system state are anyway considered as fixed data types.

References

  1. Abd Alrahman, Y., De Nicola, R., Loreti, M.: A calculus for collective-adaptive systems and its behavioural theory. Inf. Comput. 268, 104457 (2019)

    Article  MathSciNet  Google Scholar 

  2. Abd Alrahman, Y., De Nicola, R., Loreti, M.: Programming interactions in collective adaptive systems by relying on attribute-based communication. Sci. Comput. Program. 192, 102428 (2020)

    Article  Google Scholar 

  3. Abeywickrama, D., Bicocchi, N., Mamei, M., Zambonelli, F.: The SOTA approach to engineering collective adaptive systems. Int. J. Softw. Tools Technol. Transfer 22, 399–415 (2020). https://doi.org/10.1007/s10009-020-00554-3

    Article  Google Scholar 

  4. Bortolussi, L., et al.: CARMA: collective adaptive resource-sharing Markovian agents. In: Bertrand, N., Tribastone, M. (eds.) Proceedings Thirteenth Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2015, EPTCS, vol. 194, pp. 16–31 (2015)

    Google Scholar 

  5. Bruni, R., Corradini, A., Gadducci, F., Melgratti, H., Montanari, U., Tuosto, E.: Data-driven choreographies à la Klaim. In: Boreale, M., Corradini, F., Loreti, M., Pugliese, R. (eds.) Models, Languages, and Tools for Concurrent and Distributed Programming. LNCS, vol. 11665, pp. 170–190. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-21485-2_11

    Chapter  Google Scholar 

  6. De Nicola, R., Loreti, M., Pugliese, R., Tiezzi, F.: A formal approach to autonomic systems programming: the SCEL language. ACM Trans. Auton. Adapt. Syst. (TAAS) 9(2), 1–29 (2014)

    Article  Google Scholar 

  7. Ebbinghaus, H.-D.: Über eine Prädikatenlogik mit partiell definierten Prädikaten und Funktionen. Arch. Math. Logik Grundlagenforschung 12, 39–53 (1969)

    Article  MathSciNet  Google Scholar 

  8. Forejt, V., Kwiatkowska, M., Norman, G., Parker, D.: Automated verification techniques for probabilistic systems. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol. 6659, pp. 53–113. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21455-4_3

    Chapter  Google Scholar 

  9. Harel, D., Kozen, D., Tiuryn, J. (eds.): Dynamic Logic. MIT Press, Cambridge (2000)

    MATH  Google Scholar 

  10. Havelund, K., Larsen, K.G.: The fork calculus. In: Lingas, A., Karlsson, R., Carlsson, S. (eds.) ICALP 1993. LNCS, vol. 700, pp. 544–557. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-56939-1_101

    Chapter  Google Scholar 

  11. Hennicker, R.: Role-based development of dynamically evolving esembles. In: Fiadeiro, J.L., Tutu, I. (eds.) Recent Trends in Algebraic Development Techniques - 24th IFIP WG 1.3 International Workshop, WADT 2018, Revised Selected Papers. LNCS, vol. 11563, pp. 3–24. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-23220-7_1

  12. Hennicker, R., Klarl, A.: Foundations for ensemble modeling – the Helena approach. In: Iida, S., Meseguer, J., Ogata, K. (eds.) Specification, Algebra, and Software. LNCS, vol. 8373, pp. 359–381. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54624-2_18

    Chapter  Google Scholar 

  13. Hennicker, R., Klarl, A., Wirsing, M.: Model-checking Helena ensembles with spin. In: Martí-Oliet, N., Ölveczky, P.C., Talcott, C. (eds.) Logic, Rewriting, and Concurrency. LNCS, vol. 9200, pp. 331–360. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23165-5_16

    Chapter  Google Scholar 

  14. Hennicker, R., Wirsing, M.: Dynamic logic for ensembles. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11246, pp. 32–47. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03424-5_3

    Chapter  Google Scholar 

  15. Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2008), pp. 273–284. ACM (2008)

    Google Scholar 

  16. Kernbach, S., Schmickl, T., Timmis, J.: Collective adaptive systems: challenges beyond evolvability. CoRR abs/1108.5643 (2011)

    Google Scholar 

  17. Klarl, A.: HELENA: Handling massively distributed systems with ELaborate ENsemble Architectures. Ph.D. thesis, LMU Munich, Germany (2016)

    Google Scholar 

  18. Latella, D., Loreti, M., Massink, M., Senni, V.: Stochastically timed predicate-based communication primitives for autonomic computing. In: Bertrand, N., Bortolussi, L. (eds.) QAPL 2014. EPTCS, vol. 154, pp. 1–16 (2014)

    Google Scholar 

  19. Nicola, R., et al.: The SCEL language: design, implementation, verification. In: Wirsing, M., Hölzl, M., Koch, N., Mayer, P. (eds.) Software Engineering for Collective Autonomic Systems. LNCS, vol. 8998, pp. 3–71. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-16310-9_1

    Chapter  Google Scholar 

  20. Pinciroli, C., Bonani, M., Mondada, F., Dorigo, M.: Adaptation and awareness in robot ensembles: scenarios and algorithms. In: Wirsing, M., Hölzl, M., Koch, N., Mayer, P. (eds.) Software Engineering for Collective Autonomic Systems. LNCS, vol. 8998, pp. 471–494. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-16310-9_15

    Chapter  Google Scholar 

  21. Vassev, E., Hinchey, M.: Engineering requirements for autonomy features. In: Wirsing, M., Hölzl, M., Koch, N., Mayer, P. (eds.) Software Engineering for Collective Autonomic Systems. LNCS, vol. 8998, pp. 379–403. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-16310-9_11

    Chapter  Google Scholar 

  22. Wirsing, M., Banâtre, J.-P., Hölzl, M., Rauschmayer, A. (eds.): Software-Intensive Systems and New Computing Paradigms. LNCS, vol. 5380. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-89437-7

    Book  MATH  Google Scholar 

  23. Wirsing, M., Hölzl, M., Koch, N., Mayer, P. (eds.): Software Engineering for Collective Autonomic Systems. LNCS, vol. 8998. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-16310-9

    Book  Google Scholar 

  24. Wirsing, M., Hölzl, M., Tribastone, M., Zambonelli, F.: ASCENS: engineering autonomic service-component ensembles. In: Beckert, B., Damiani, F., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2011. LNCS, vol. 7542, pp. 1–24. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-35887-6_1

    Chapter  Google Scholar 

  25. Würtz, R.P.: Organic Computing. UCS. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-77657-4

    Book  Google Scholar 

Download references

Author information

Authors and Affiliations

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

    Rolf Hennicker & Martin Wirsing

Authors
  1. Rolf Hennicker
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Martin Wirsing
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Rolf Hennicker or Martin Wirsing .

Editor information

Editors and Affiliations

  1. University of Limerick and Lero, Limerick, Ireland

    Tiziana Margaria

  2. TU Dortmund, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Hennicker, R., Wirsing, M. (2020). A Dynamic Logic for Systems with Predicate-Based Communication. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles. ISoLA 2020. Lecture Notes in Computer Science(), vol 12477. Springer, Cham. https://doi.org/10.1007/978-3-030-61470-6_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-61470-6_14

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-61469-0

  • Online ISBN: 978-3-030-61470-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation