Abstract
Run-time verification is one of the most useful techniques for detecting faults. In this paper we show how to model the observable behavior of concurrently running object groups (coboxes) in SAGA (Software trace Analysis using Grammars and Attributes) which is a run-time checker that provides a smooth integration of the specification and the efficient run-time checking of both data- and protocol-oriented properties of message sequences. We illustrate the effectiveness of our method by an industrial case study from the eCommerce software company Fredhopper.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Agha, G.: Actors: A model of concurrent computation in distributed systems. MIT Press, Cambridge (1990)
Allan, C., Avgustinov, P., Christensen, A.S., Hendren, L., Kuzins, S., Lhoták, O., de Moor, O., Sereni, D., Sittampalam, G., Tibble, J.: Adding trace matching with free variables to aspectj. SIGPLAN Not. 40(10), 345–364 (2005)
Chen, F., Roşu, G.: MOP: an efficient and generic runtime verification framework. SIGPLAN Not. 42(10), 569–588 (2007)
Clarke, L.A., Rosenblum, D.S.: A historical perspective on runtime assertion checking in software development. ACM SIGSOFT Software Engineering Notes 31(3), 25–37 (2006)
Colombo, C., Pace, G.J., Schneider, G.: Larva — safer monitoring of real-time java programs (tool paper). In: SEFM 2005, pp. 33–37 (2009)
de Boer, F.S., de Gouw, S., Johnsen, E.B., Wong, P.Y.H.: Run-time checking of data- and protocol-oriented properties of java programs: An industrial case study. In: SAC (to appear, 2013)
DeLine, R., Fähndrich, M.: Typestates for Objects. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 465–490. Springer, Heidelberg (2004)
Din, C.C., Dovland, J., Johnsen, E.B., Owe, O.: Observable behavior of distributed systems: Component reasoning for concurrent objects. J. Log. Algebr. Program. 81(3), 227–256 (2012)
Hatcliff, J., Leavens, G.T., Leino, K.R.M., Müller, P., Parkinson, M.: Behavioral interface specification languages. ACM Comput. Surv. 44(3), 16:1–16:58 (2012)
Johnsen, E.B., Hähnle, R., Schäfer, J., Schlatte, R., Steffen, M.: ABS: A core language for abstract behavioral specification. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 142–164. Springer, Heidelberg (2011)
Johnsen, E.B., Owe, O.: An asynchronous communication model for distributed concurrent objects. SSM 6(1), 35–58 (2007)
Lee, L.: Fast context-free grammar parsing requires fast boolean matrix multiplication. J. ACM 49(1), 1–15 (2002)
Martin, M., Livshits, B., Lam, M.S.: Finding application errors and security flaws using pql: a program query language. SIGPLAN Not. 40(10), 365–383 (2005)
Nobakht, B., Bonsangue, M.M., de Boer, F.S., de Gouw, S.: Monitoring method call sequences using annotations. In: Barbosa, L.S., Lumpe, M. (eds.) FACS 2010. LNCS, vol. 6921, pp. 53–70. Springer, Heidelberg (2012)
Schäfer, J., Poetzsch-Heffter, A.: JCoBox: Generalizing active objects to concurrent components. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 275–299. Springer, Heidelberg (2010)
Sirjani, M., Movaghar, A., Shali, A., de Boer, F.S.: Modeling and verification of reactive systems using Rebeca. Fundam. Inform. 63(4), 385–410 (2004)
Valiant, L.G.: General context-free recognition in less than cubic time. J. Comput. Syst. Sci. 10(2), 308–315 (1975)
Wong, P.Y.H., Albert, E., Muschevici, R., Proença, J., Schäfer, J., Schlatte, R.: The ABS tool suite: modelling, executing and analysing distributed adaptable object-oriented systems. STTT 14(5), 567–588 (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
de Boer, F.S., de Gouw, S., Wong, P.Y.H. (2013). Run-Time Verification of Coboxes. In: Hierons, R.M., Merayo, M.G., Bravetti, M. (eds) Software Engineering and Formal Methods. SEFM 2013. Lecture Notes in Computer Science, vol 8137. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40561-7_18
Download citation
DOI: https://doi.org/10.1007/978-3-642-40561-7_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40560-0
Online ISBN: 978-3-642-40561-7
eBook Packages: Computer ScienceComputer Science (R0)