Publication:
REAL-T: Time Modularization in Reactive Distributed Applications

Thumbnail Image
Files

Files

Primary REAL-T - Time Modularization in Reactive Distributed Applications.pdf (94.98 KB)
View Statistics
Reference Managers
Mendeley
Indexers
Google Scholar CORE
QR Code
QR Code
Authors

Authors

Pimienta, Camilo
Sanabria, Mateo
Díaz, Daniel
Garzón, Wilmer
Melo, Willson
Arboleda, Hugo
Benavides Navarro, Luis Daniel
Abstract (Spanish)
En este artículo, proponemos REAL-T, un lenguaje distribuido basado en eventos con soporte explícito para la manipulación del tiempo. El lenguaje introduce autómatas para la manipulación del tiempo operacional, construcciones de causalidad y lógica temporal lineal para predicados de tiempo declarativos, y un modelo de eventos de tiempo distribuido. Hemos desarrollado un compilador para el lenguaje y un marco de tiempo de ejecución dinámico. Para validar la propuesta estudiamos la detección de patrones complejos de vulnerabilidades de seguridad en escenarios de IoT.
Abstract (English)
In this paper, we propose REAL-T, a distributed event-based language with explicit support for time manipulation. The language introduces automata for operational time manipulation, causality constructs and Linear Temporal Logic for declarative time predicates, and a distributed-time aware event model. We have developed a compiler for the language and a dynamic run-time framework. To validate the proposal we study detection of complex patterns of security vulnerabilities in IoT scenarios.
Extent
15 páginas
URI: https://repositorio.escuelaing.edu.co/handle/001/1476
Collections

Collections

AD - CTG – Informática
References

Baier, C., Katoen, J.P.: Principles of Model Checking. MIT press, Cambridge (2008)

Ban, B., Grinovero, S.: JGroups (2011)

Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Program monitoring with LTL in EAGLE. In: 18th International Parallel and Distributed Processing Symposium 2004, April 2004

Benavides Navarro, L.D., Barrera, A., Garcés, K., Arboleda, H.: Detecting and coordinating complex patterns of distributed events with KETAL. Electron. Notes Theor. Comput. Sci. 281, 127–141 (2011)

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

Benton, N., Cardelli, L., Fournet, C.: Modern concurrency abstractions for c#. ACM Trans. Program. Lang. Syst. 26(5), 769–804 (2004)

Büchi, J.R.: Symposium on decision problems on a decision method in restricted second order arithmetic. Stud. Log. Found. Math. 44, 1–11 (1966)

Chen, F., Roşu, G.: Java-MOP: a monitoring oriented programming environment for Java. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 546–550. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31980-1_36

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

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

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

Giannakopoulou, D., Lerda, F.: From states to transitions: improving translation of LTL formulae to Büchi automata. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, pp. 308–326. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-36135-9_20

Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8(3), 231–274 (1987). https://doi.org/10.1016/0167-6423(87)90035-9

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)

Kiczales, G., et al.: Aspect-oriented programming. In: Akşit, M., Matsuoka, S. (eds.) ECOOP 1997. LNCS, vol. 1241, pp. 220–242. Springer, Heidelberg (1997).

Konur, S.: A survey on temporal logics for specifying and verifying real-time systems. Front. Comput. Sci. 7(3), 370–403 (2013)

Kröger, F., Merz, S.: Temporal Logic and State Systems. Springer, Berlin (2008). https://doi.org/10.1007/978-3-540-68635-4

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

Lee, I., Lee, K.: The internet of things (IoT): applications, investments, and challenges for enterprises. Bus. Horiz. 58(4), 431–440 (2015)

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. Transf. 14(3), 249–289 (2012)

Møller, A.: dk.brics.automaton – finite-state automata and regular expressions for Java (2017). http://www.brics.dk/automaton/

Naldurg, P., Sen, K., Thati, P.: A temporal logic based framework for intrusion detection. In: de Frutos-Escrig, D., Núñez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 359–376. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30232-2_23

Ousterhout, J.: Why threads are a bad idea (for most purposes). In: Invited talk Given at USENIX Technical Conference (1996). https://web.stanford.edu/~ouster/cgi-bin/papers/threads.pdf

Petri, C.A.: Fundamentals of a theory of asynchronous information flow. In: IFIP Congress (1962)

van Renesse, R., Birman, K.P., Maffeis, S.: Horus: a flexible group communication system. Commun. ACM 39(4), 76–83 (1996)

Robiah, Y., Rahayu, S.S., Shahrin, S., Faizal, M., Zaki, M.M., Marliza, R.: New multi-step worm attack model. arXiv preprint arXiv:1001.3477 (2010)