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.
Keywords
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Agha, G.: Concurrent object-oriented programming. Commun. ACM 33(9), 125–141 (1990)
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
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
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
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
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
Bhat, G., Cleaveland, R., Lüttgen, G.: A practical approach to implementing real-time semantics. Ann. Softw. Eng. 7(1), 127–155 (1999)
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
Chen, F., Roşu, G.: MOP: an efficient and generic runtime verification framework. In: ACM SIGPLAN Notices, vol. 42, pp. 569–588. ACM (2007)
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
Fisher, M.: An Introduction to Practical Formal Methods Using Temporal Logic. Wiley, Hoboken (2011)
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
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)
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)
Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978)
Le Lann, G.: Distributed systems-towards a formal approach. In: IFIP Congress, Toronto, vol. 7, pp. 155–160 (1977)
Magee, J., Kramer, J.: Concurrency: State Models and Java Programs, 2nd edn. Wiley, Hoboken (2006)
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
Mattern, F., et al.: Virtual time and global states of distributed systems. Parallel Distrib. Algorithms 1(23), 215–226 (1989)
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)
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
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
Spiliopoulou, E.: Concurrent and distributed functional systems. Ph.D. thesis, University of Bristol (2000)
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
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
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)