Abstract
We present CoMA (Conformance Monitoring by Abstract State Machines), a specification-based approach and its supporting tool for runtime monitoring of Java software. Based on the information obtained from code execution and model simulation, the conformance of the concrete implementation is checked with respect to its formal specification given in terms of Abstract State Machines. At runtime, undesirable behaviors of the implementation, as well as incorrect specifications of the system behavior are recognized.
The technique we propose makes use of Java annotations, which link the concrete implementation to its formal model, without enriching the code with behavioral information contained only in the abstract specification. The approach fosters the separation between implementation and specification, and allows the reuse of specifications for other purposes (formal verification, simulation, model-based testing, etc.).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Allan, C., Avgustinov, P., Christensen, A.S., Hendren, L.J., Kuzins, S., Lhoták, O., de Moor, O., Sereni, D., Sittampalam, G., Tibble, J.: Adding trace matching with free variables to AspectJ. In: Johnson, R.E., Gabriel, R.P. (eds.) OOPSLA, pp. 345–364 (2005)
Arcaini, P., Gargantini, A., Riccobene, E.: Runtime monitoring of Java programs by Abstract State Machines. TR 131, DTI Dept., Univ. of Milan (2010)
Arcaini, P., Gargantini, A., Riccobene, E., Scandurra, P.: A model-driven process for engineering a toolset for a formal method. Softw., Pract. Exper. 41(2), 155–166 (2011)
Barnett, M., Schulte, W.: Runtime verification of.NET contracts. The Journal of Systems and Software 65(3), 199–208 (2003)
Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Transactions on Software and Methodology (TOSEM) 20 (2011)
Börger, E., Stärk, R.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)
Chen, F., D’Amorim, M., Roşu, G.: A Formal Monitoring-Based Framework for Software Development and Analysis. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 357–372. Springer, Heidelberg (2004)
Chen, F., Roşu, G.: Mop: an efficient and generic runtime verification framework. In: Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object Oriented Programming Systems and Applications - OOPSLA 2007, Montreal, Quebec, Canada, page 569 (2007)
Colin, S., Mariani, L.: 18 Run-Time Verification. In: Broy, M., Jonsson, B., Katoen, J.-P., Leucker, M., Pretschner, A. (eds.) Model-Based Testing of Reactive Systems. LNCS, vol. 3472, pp. 525–555. Springer, Heidelberg (2005)
Darvas, A., Leino, K.R.M.: Practical Reasoning About Invocations and Implementations of Pure Methods. In: Dwyer, M.B., Lopes, A. (eds.) FASE 2007. LNCS, vol. 4422, pp. 336–351. Springer, Heidelberg (2007)
Delgado, N., Gates, A.Q., Roach, S.: A taxonomy and catalog of runtime software-fault monitoring tools. IEEE Transactions on Software Engineering 30(12), 859–872 (2004)
Gargantini, A., Riccobene, E., Scandurra, P.: A metamodel-based language and a simulation engine for Abstract State Machines. Journal of Universal Computer Science (JUCS) 14(12), 1949–1983 (2008)
Havelund, K., Roşu, G.: Efficient monitoring of safety properties. Int. J. Softw. Tools Technol. Transf. 6, 158–173 (2004)
Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice-Hall International, Englewood Cliffs (1998)
Kähkönen, K., Lampinen, J., Heljanko, K., Niemelä, I.: The LIME Interface Specification Language and Runtime Monitoring Tool. In: Bensalem, S., Peled, D.A. (eds.) RV 2009. LNCS, vol. 5779, pp. 93–100. Springer, Heidelberg (2009)
Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. SIGSOFT Softw. Eng. Notes 31, 1–38 (2006)
Lee, I., Kannan, S., Kim, M., Sokolsky, O., Viswanathan, M.: Runtime assurance based on formal specifications. In: Parallel and Distributed Processing Techniques and Applications, pp. 279–287 (1999)
Leucker, M., Schallhart, C.: A brief account of runtime verification. Journal of Logic and Algebraic Programming 78(5), 293–303 (2009)
Liang, H., Dong, J., Sun, J., Wong, W.: Software monitoring through formal specification animation. Innovations in Systems and Soft. Eng. 5, 231–241 (2009)
Weisstein, E.W.: Knight’s tour. from MathWorld–A Wolfram Web Resource
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Arcaini, P., Gargantini, A., Riccobene, E. (2012). CoMA: Conformance Monitoring of Java Programs by Abstract State Machines. In: Khurshid, S., Sen, K. (eds) Runtime Verification. RV 2011. Lecture Notes in Computer Science, vol 7186. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-29860-8_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-29860-8_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-29859-2
Online ISBN: 978-3-642-29860-8
eBook Packages: Computer ScienceComputer Science (R0)