Skip to main content

Towards Real-Time Semantics for a Distributed Event-Based MOP Language

  • Conference paper
  • First Online:
New Trends in Model and Data Engineering (MEDI 2018)

Abstract

This paper investigates rewriting logic as a suitable means to model the semantics of distributed and concurrent systems implemented using Monitoring Oriented Programming (MOP) frameworks. MOP tools close the gap between specification and implementation, allowing several formal specifications and concrete implementations to be combined into a single executing system. To address real-time monitoring of modern distributed applications, we recently proposed REAL-T, a reactive event-based distributed programming language with explicit support for distributions and time manipulation. REAL-T allows programmers to instrument distributed applications to monitor and enforce specific behavior. It also supports requirements of modern reactive applications (responsiveness, resiliency, elasticity and asynchronous communication). The REAL-T programming model is very flexible, making the semantic specifications very challenging.

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

Access this chapter

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

References

  1. Agha, G.: Concurrent object-oriented programming. Commun. ACM 33(9), 125–141 (1990)

    Article  Google Scholar 

  2. Basu, A., Bensalem, S., Bozga, M., Bourgos, P., Sifakis, J.: Rigorous system design: the BIP approach. In: Kotásek, Z., Bouda, J., Černá, I., Sekanina, L., Vojnar, T., Antoš, D. (eds.) MEMICS 2011. LNCS, vol. 7119, pp. 1–19. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-25929-6_1

    Chapter  Google Scholar 

  3. Benavides Navarro, L.D., Douence, R., Núñez, A., Südholt, M.: LTS-based semantics and property analysis of distributed aspects and invasive patterns. In: Leuven, K.U. (ed.) Workshop on Aspects, Dependencies and Interactions. Technical Report, Belgium, vol. CW 517, pp. 36–45, July 2008. https://doi.org/10.1007/978-3-642-02047-6, https://hal.archives-ouvertes.fr/hal-00469648

    Google Scholar 

  4. Benavides Navarro, L.D., Douence, R., Südholt, M.: Debugging and testing middleware with aspect-based control-flow and causal patterns. In: Issarny, V., Schantz, R. (eds.) Middleware 2008. LNCS, vol. 5346, pp. 183–202. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-89856-6_10

    Chapter  Google Scholar 

  5. Benavides Navarro, L.D., et al.: REAL-T: time modularization in reactive distributed applications. In: Serrano, C.J., Martínez-Santos, J. (eds.) CCC 2018. CCIS, vol. 885, pp. 113–127. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-98998-3_9

    Chapter  Google Scholar 

  6. Bensalem, S., Bozga, M., Delahaye, B., Jegourel, C., Legay, A., Nouri, A.: Statistical model checking QoS properties of systems with SBIP. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7609, pp. 327–341. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-34026-0_25

    Chapter  Google Scholar 

  7. Bhat, G., Cleaveland, R., Lüttgen, G.: A practical approach to implementing real-time semantics. Ann. Softw. Eng. 7(1), 127–155 (1999)

    Article  Google Scholar 

  8. Charron-Bost, B., Mattern, F., Tel, G.: Synchronous, asynchronous, and causally ordered communication. Distrib. Comput. 9(4), 173–191 (1996). https://doi.org/10.1007/s004460050018

    Article  MathSciNet  Google Scholar 

  9. Chen, F., Roşu, G.: MOP: an efficient and generic runtime verification framework. In: ACM SIGPLAN Notices, vol. 42, pp. 569–588. ACM (2007)

    Google Scholar 

  10. Clavel, M., et al.: The maude 2.0 system. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 76–87. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-44881-0_7

    Chapter  Google Scholar 

  11. Fisher, M.: An Introduction to Practical Formal Methods Using Temporal Logic. Wiley, Hoboken (2011)

    Book  Google Scholar 

  12. Fontana, P., Cleaveland, R.: A menagerie of timed automata. ACM Comput. Surv. 46(3), 40:1–40:56 (2014). https://doi.org/10.1145/2518102

    Article  MATH  Google Scholar 

  13. Furia, C.A., Mandrioli, D., Morzenti, A., Rossi, M.: Modeling time in computing: a taxonomy and a comparative survey. ACM Comput. Surv. 42(2), 6:1–6:59 (2010)

    Article  Google Scholar 

  14. Haydar, M., Boroday, S., Petrenko, A., Sahraoui, H.: Propositional scopes in linear temporal logic. In: Proceedings of the 5th International Conference on Novelles Technologies de la Repartition (NOTERE 2005) (2005)

    Google Scholar 

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

    Article  Google Scholar 

  16. Le Lann, G.: Distributed systems-towards a formal approach. In: IFIP Congress, Toronto, vol. 7, pp. 155–160 (1977)

    Google Scholar 

  17. Magee, J., Kramer, J.: Concurrency: State Models and Java Programs, 2nd edn. Wiley, Hoboken (2006)

    MATH  Google Scholar 

  18. Mallet, F.: Clock constraint specification language: specifying clock constraints with UML/MARTE. Innov. Syst. Softw. Eng. 4(3), 309–314 (2008). https://doi.org/10.1007/s11334-008-0055-2

    Article  Google Scholar 

  19. Mattern, F., et al.: Virtual time and global states of distributed systems. Parallel Distrib. Algorithms 1(23), 215–226 (1989)

    MathSciNet  Google Scholar 

  20. Meredith, P.O., Jin, D., Griffith, D., Chen, F., Roşu, G.: An overview of the mop runtime verification framework. Int. J. Softw. Tools Technol. Transfer 14(3), 249–289 (2012)

    Article  Google Scholar 

  21. Meseguer, J.: Twenty years of rewriting logic. J. Log. Algebr. Program. 81(7), 721–781 (2012). https://doi.org/10.1016/j.jlap.2012.06.003, http://www.sciencedirect.com/science/article/pii/S1567832612000707, Rewriting Logic and its Applications

    Article  MathSciNet  Google Scholar 

  22. Roşu, G.: From rewriting logic, to programming language semantics, to program verification. In: Martí-Oliet, N., Ölveczky, P.C., Talcott, C. (eds.) Logic, Rewriting, and Concurrency. LNCS, vol. 9200, pp. 598–616. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23165-5_28

    Chapter  MATH  Google Scholar 

  23. Spiliopoulou, E.: Concurrent and distributed functional systems. Ph.D. thesis, University of Bristol (2000)

    Google Scholar 

  24. Tabareau, N.: A theory of distributed aspects. In: Proceedings of the 9th International Conference on Aspect-Oriented Software Development, AOSD 2010, pp. 133–144. ACM, New York (2010). https://doi.org/10.1145/1739230.1739246

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Luis Daniel Benavides Navarro .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Sanabria, M., Alfonso, W.G., Benavides Navarro, L.D. (2018). Towards Real-Time Semantics for a Distributed Event-Based MOP Language. In: Abdelwahed, E., et al. New Trends in Model and Data Engineering. MEDI 2018. Communications in Computer and Information Science, vol 929. Springer, Cham. https://doi.org/10.1007/978-3-030-02852-7_20

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-02852-7_20

  • Published:

  • Publisher Name: Springer, Cham

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

  • Online ISBN: 978-3-030-02852-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics