Skip to main content
SpringerLink
Log in

Verifying Properties of Systems Relying on Attribute-Based Communication

  • Chapter
  • First Online:
ModelEd, TestEd, TrustEd

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10500))

Abstract

AbC is a process calculus designed for describing collective adaptive systems, whose distinguishing feature is the communication mechanism relying on predicates over attributes exposed by components. A novel approach to the analysis of concurrent systems modelled as AbC terms is presented that relies on the UMC model checker, a tool based on modelling concurrent systems as communicating UML-like state machines. A structural translation from AbC specifications to the UMC internal format is provided and used as the basis for the analysis. Three different algorithmic solutions of the well studied stable marriage problem are described in AbC and their translations are analysed with UMC. It is shown how the proposed approach can be exploited to identify emerging properties of systems and unwanted behaviour.

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

Access this chapter

Log in via an institution
eBook
USD 16.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 16.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.

    Just consider that the email address(es) of the friend to whom this volume is dedicated were something like uucp: mcvax!utinu1!infed and earn: hiddink@hentht5.

  2. 2.

    UMC also supports an Operations section for the definition of synchronous events, which is however not relevant in our study.

  3. 3.

    FINAL is a shortcut for “not EX {true} true”.

  4. 4.

    $id and %id are used to match the identities of the sending and receiving components.

References

  1. AbC2UMC. http://github.com/ArBITRAL/AbC2UMC

  2. UMC. http://fmt.isti.cnr.it/umc

  3. UMC Docs. http://fmt.isti.cnr.it/umc/DOCS

  4. Abd Alrahman, Y., De Nicola, R., Loreti, M.: On the power of attribute-based communication. In: Albert, E., Lanese, I. (eds.) FORTE 2016. LNCS, vol. 9688, pp. 1–18. Springer, Cham (2016). doi:10.1007/978-3-319-39570-8_1

    Chapter  Google Scholar 

  5. Abd Alrahman, Y., De Nicola, R., Loreti, M.: Programming of CAS systems by relying on attribute-based communication. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 539–553. Springer, Cham (2016). doi:10.1007/978-3-319-47166-2_38

    Chapter  Google Scholar 

  6. ter Beek, M.H., Gnesi, S., Mazzanti, F.: From EU projects to a family of model checkers. In: De Nicola, R., Hennicker, R. (eds.) Software, Services, and Systems. LNCS, vol. 8950, pp. 312–328. Springer, Cham (2015). doi:10.1007/978-3-319-15545-6_20

    Chapter  Google Scholar 

  7. Biró, P., Norman, G.: Analysis of stochastic matching markets. Int. J. Game Theo. 42(4), 1021–1040 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  8. Bolognesi, T., Brinksma, E.: Introduction to the ISO specification language LOTOS. Comput. Netw. 14, 25–59 (1987). https://doi.org/10.1016/0169-7552(87)90085–7

    Google Scholar 

  9. Brinksma, E.: On the design of extended LOTOS, Doctoral Dissertation. University of Twente (1988)

    Google Scholar 

  10. De Nicola, R., Duong, T., Inverso, O., Trubiani, C.: AErlang at work. In: Steffen, B., Baier, C., Brand, M., Eder, J., Hinchey, M., Margaria, T. (eds.) SOFSEM 2017. LNCS, vol. 10139, pp. 485–497. Springer, Cham (2017). doi:10.1007/978-3-319-51963-0_38

    Chapter  Google Scholar 

  11. De Nicola, R., Duong, T., Inverso, O., Trubiani, C.: AErlang: empowering erlang with attribute-based communication. In: Jacquet, J.-M., Massink, M. (eds.) COORDINATION 2017. LNCS, vol. 10319, pp. 21–39. Springer, Cham (2017). doi:10.1007/978-3-319-59746-1_2

    Chapter  Google Scholar 

  12. De Nicola, R., Gorla, D., Pugliese, R.: On the expressive power of KLAIM-based calculi. Theor. Comput. Sci. 356(3), 387–421 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  13. De Nicola, R., Lluch Lafuente, A., Loreti, M., Morichetta, A., Pugliese, R., Senni, V., Tiezzi, F.: Programming and verifying component ensembles. In: Bensalem, S., Lakhneck, Y., Legay, A. (eds.) ETAPS 2014. LNCS, vol. 8415, pp. 69–83. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54848-2_5

    Chapter  Google Scholar 

  14. De Nicola, R., Vaandrager, F.W.: Three logics for branching bisimulation. J. ACM 42(2), 458–487 (1995). http://doi.acm.org/10.1145/201019.201032

    Article  MathSciNet  MATH  Google Scholar 

  15. Brinksma, E., Giuseppe Scollo, C.S.: LOTOS specifications, their implementations and their tests. In: Proceedings of IFIP WG6.1, Protocol Specification, Testing, and Verification VI, pp. 349–360 (1987)

    Google Scholar 

  16. Fantechi, A., Gnesi, S., Lapadula, A., Mazzanti, F., Pugliese, R., Tiezzi, F.: A logical verification methodology for service-oriented computing. ACM Transactions on Software Engineering and Methodology (TOSEM) (2012)

    Google Scholar 

  17. Gale, D., Shapley, L.S.: College admissions and the stability of marriage. Am. Math. Mon. 69(1), 9–15 (1962)

    Article  MathSciNet  MATH  Google Scholar 

  18. Groote, J.F., Reniers, M.A.: Algebraic process verification. Eindhoven University of Technology, Department of Mathematics and Computing Science (2000)

    Google Scholar 

  19. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall Inc., Upper Saddle River (1985)

    MATH  Google Scholar 

  20. ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: A state/event-based model-checking approach for the analysis of abstract system properties. Sci. Comput. Program. 76(2), 119–135 (2011)

    Article  MATH  Google Scholar 

  21. Kümmel, M., Busch, F., Wang, D.Z.: Taxi dispatching and stable marriage. Proc. Comput. Sci. 83, 163–170 (2016)

    Article  Google Scholar 

  22. Lu, S., Park, S., Seo, E., Zhou, Y.: Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. In: ACM Sigplan Notices, vol. 43, pp. 329–339. ACM (2008)

    Google Scholar 

  23. Manlove, D.F., Irving, R.W., Iwama, K., Miyazaki, S., Morita, Y.: Hard variants of stable marriage. Theor. Comput. Sci. 276(1–2), 261–279 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  24. Mateescu, R., Salaün, G.: Translating Pi-calculus into LOTOS NT. In: Méry, D., Merz, S. (eds.) IFM 2010. LNCS, vol. 6396, pp. 229–244. Springer, Heidelberg (2010). doi:10.1007/978-3-642-16265-7_17

    Chapter  Google Scholar 

  25. Milner, R. (ed.): A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1980)

    MATH  Google Scholar 

  26. Song, H., Compton, K.J.: Verifying \(\pi \)-calculus processes by promela translation. Technical report CSE-TR-472-03 (2003)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IMT School for Advanced Studies Lucca, Lucca, Italy

    Rocco De Nicola

  2. Gran Sasso Science Institute, L’aquila, Italy

    Tan Duong & Omar Inverso

  3. ISTI CNR, Pisa, Italy

    Franco Mazzanti

Authors
  1. Rocco De Nicola
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Tan Duong
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Omar Inverso
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Franco Mazzanti
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Rocco De Nicola .

Editor information

Editors and Affiliations

  1. RWTH Aachen University, Aachen, Germany

    Joost-Pieter Katoen

  2. University of Twente, Enschede, The Netherlands

    Rom Langerak

  3. University of Twente, Enschede, The Netherlands

    Arend Rensink

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this chapter

Cite this chapter

De Nicola, R., Duong, T., Inverso, O., Mazzanti, F. (2017). Verifying Properties of Systems Relying on Attribute-Based Communication. In: Katoen, JP., Langerak, R., Rensink, A. (eds) ModelEd, TestEd, TrustEd. Lecture Notes in Computer Science(), vol 10500. Springer, Cham. https://doi.org/10.1007/978-3-319-68270-9_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-68270-9_9

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-68269-3

  • Online ISBN: 978-3-319-68270-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation