Advertisement

Distributed Coordination Runtime Assertions for the Peer Model

Conference paper
First Online:
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10852)

Abstract

Major challenges in the software development of distributed systems are rooted in the complex nature of coordination. Assertions are a practical programming mechanism to improve the quality of software in general by monitoring it at runtime. Most approaches today limit assertions to statements about local states whereas coordination requires reasoning about distributed states. The Peer Model is an event-based coordination programming model that relies on known foundations like shared tuple spaces, Actor Model, and Petri Nets. We extend it with distributed runtime invariant assertions that are specified and implemented using its own coordination mechanisms. This lifts the concept of runtime assertions to the level of coordination modeling. The concept is demonstrated by means of an example from the railway domain.

Keywords

Coordination model Runtime assertions Distributed systems Tuple space 
This is a preview of subscription content, log in to check access.

Notes

Acknowledgements

The authors would like to thank Anita Messinger for the discussions on train systems, and Stefan Craß for commenting this paper.

References

  1. 1.
    Abrial, J.-R.: Train systems. In: Butler, M., Jones, C.B., Romanovsky, A., Troubitsyna, E. (eds.) Rigorous Development of Complex Fault-Tolerant Systems. LNCS, vol. 4157, pp. 1–36. Springer, Heidelberg (2006).  https://doi.org/10.1007/11916246_1CrossRefGoogle Scholar
  2. 2.
    Agha, G.A.: ACTORS: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge (1990)Google Scholar
  3. 3.
    Arbab, F.: Reo: a channel-based coordination model for component composition. Math. Struct. Comput. Sci. 14(3), 329–366 (2004)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(2), 14:1–14:64 (2011)Google Scholar
  5. 5.
    Chao, H., Li, H., Song, X., Wang, T., Li, X.: On evaluating and constraining assertions using conflicts in absent scenarios. In: 26th IEEE Asian Test Symposium, ATS 2017, Taipei City, Taiwan, 27–30 November 2017, pp. 195–200 (2017)Google Scholar
  6. 6.
    Din, C.C., Owe, O., Bubel, R.: Runtime assertion checking and theorem proving for concurrent and distributed systems. In: MODELSWARD 2014 - Proceedings of the 2nd International Conference on Model-Driven Engineering and Software Development, Lisbon, Portugal, 7–9 January 2014, pp. 480–487 (2014)Google Scholar
  7. 7.
    El-Hokayem, A., Falcone, Y.: Monitoring decentralized specifications. In: Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2017, pp. 125–135. ACM (2017)Google Scholar
  8. 8.
    Falcone, Y., Jaber, M., Nguyen, T.H., Bozga, M., Bensalem, S.: Runtime verification of component-based systems in the bip framework with formally-proved sound and complete instrumentation. Softw. Syst. Model. 14(1), 173–199 (2015)CrossRefGoogle Scholar
  9. 9.
    Faruk Polat, R.A.: A multi-agent tuple-space based problem solving framework. J. Syst. Softw. 47(5), 11–17 (1999)CrossRefGoogle Scholar
  10. 10.
    Gelernter, D.: Generative communication in Linda. ACM Trans. Program. Lang. Syst. (TOPLAS) 7(1), 80–112 (1985)CrossRefGoogle Scholar
  11. 11.
    Gelernter, D., Carriero, N.: Coordination languages and their significance. Commun. ACM (CACM) 35(2), 96–107 (1992)CrossRefGoogle Scholar
  12. 12.
    Kamburjan, E., Din, C.C., Chen, T.-C.: Session-based compositional analysis for actor-based languages using futures. In: Ogata, K., Lawford, M., Liu, S. (eds.) ICFEM 2016. LNCS, vol. 10009, pp. 296–312. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-47846-3_19CrossRefGoogle Scholar
  13. 13.
    Kasuya, A., Tesfaye, T.: Verification methodologies in a TLM-to-RTL design flow. In: DAC 2007, pp. 199–204. ACM (2007)Google Scholar
  14. 14.
    Khosravi, R., Sirjani, M., Asoudeh, N., Sahebi, S., Iravanchi, H.: Modeling and analysis of Reo connectors using alloy. In: Lea, D., Zavattaro, G. (eds.) COORDINATION 2008. LNCS, vol. 5052, pp. 169–183. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-68265-3_11CrossRefGoogle Scholar
  15. 15.
    Kühn, E.: Reusable coordination components: reliable development of cooperative information systems. Int. J. Coop. Inf. Syst. 25(4), 1740001-1–1740001-32 (2016)CrossRefGoogle Scholar
  16. 16.
    Kühn, E.: Flexible transactional coordination in the peer model. In: Dastani, M., Sirjani, M. (eds.) FSEN 2017. LNCS, vol. 10522, pp. 116–131. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-68972-2_8CrossRefGoogle Scholar
  17. 17.
    Kühn, E., Mordinyi, R., Keszthelyi, L., Schreiber, C.: Introducing the concept of customizable structured spaces for agent coordination in the production automation domain. In: 8th International Conference on Autonomous Agents and Multiagent Systems (AAMAS), pp. 625–632. IFAAMAS (2009)Google Scholar
  18. 18.
    Mostafa, M., Bonakdarpour, B.: Decentralized runtime verification of LTL specifications in distributed systems. In: 2015 IEEE International Parallel and Distributed Processing Symposium, pp. 494–503, May 2015Google Scholar
  19. 19.
    Newsham, Z., de Oliveira, A.B., Petkovich, J.C., Rehman, A.S.U., Tchamgoue, G.M., Fischmeister, S.: Intersert: assertions on distributed process interaction sessions. In: 2017 IEEE International Conference on Software Quality, Reliability and Security (QRS) (2017)Google Scholar
  20. 20.
    Petri, C.A.: Kommunikation mit Automaten. Ph.D. thesis, Technische Hochschule Darmstadt (1962)Google Scholar
  21. 21.
    Pham, L.H., Thi, L.L.T., Sun, J.: Assertion generation through active learning. In: 39th IEEE International Conference on Software Engineering Companion, pp. 155–157. IEEE/ACM (2017)Google Scholar
  22. 22.
    Radschek, S.T.: A usable formal methods tool chain for safety critical concurrent systems design. Master’s thesis, TU Wien (2018, submitted)Google Scholar
  23. 23.
    Reichl, K., Fischer, T., Tummeltshammer, P.: Using formal methods for verification and validation in railway. In: Aichernig, B.K.K., Furia, C.A.A. (eds.) TAP 2016. LNCS, vol. 9762, pp. 3–13. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-41135-4_1CrossRefGoogle Scholar
  24. 24.
    Scheller, T., Kühn, E.: Automated measurement of API usability: the API Concepts Framework. Inf. Softw. Technol. 61, 145–162 (2015)CrossRefGoogle Scholar
  25. 25.
    Tjang, A., Oliveira, F., Martin, R.P., Nguyen, T.D.: A: an assertion language for distributed systems. In: Proceedings of the 3rd Workshop on Programming Languages and Operating Systems: Linguistic Support for Modern Operating Systems, PLOS 2006. ACM (2006)Google Scholar
  26. 26.
    Wang, C., He, F., Song, X., Jiang, Y., Gu, M., Sun, J.: Assertion recommendation for formal program verification. In: 41st IEEE Annual Computer Software and Applications Conference, COMPSAC 2017, Turin, Italy, 4–8 July 2017, vol. 1, pp. 154–159 (2017)Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2018

Authors and Affiliations

  1. 1.TU WienViennaAustria
  2. 2.Canadian International College – CICCairoEgypt

Personalised recommendations

Cite paper

Buy options