Abstract
Tracechecks are a formalism based on linear temporal logic (LTL) with variable bindings and pointcuts of the aspect-oriented language AspectJ for the purpose of verification. We demonstrate how tracechecks can be used to model temporal assertions. These assertions reason about the dynamic control flow of an application. They can be used to formally define the semantic interface of classes. We explain in detail how we make use of AspectJ pointcuts to derive a formal model of an existing application and use LTL to express temporal assertions over this model.
We developed a reference implementation with the abc compiler showing that the tool can be applied in practice and is memory-efficient.
In addition we show how tracechecks can be deployed as Java5 annotations, yielding a system which is fully compliant with any Java compiler and hiding any peculiarities of aspect-oriented programming from the user. Through annotations, the tracecheck specifications become a semantic part of an interface. Consumers of such a component can then take advantage of the contained annotations by applying our tool and have their use of this component automatically checked at runtime for compliance with the intent of the component provider.
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
Åberg, R.A., Lawall, J.L., Südholt, M., Muller, G., Meur, A.-F.L.: On the automatic evolution of an OS kernel using temporal logic and AOP. In: Proc. of Automated Software Engineering (ASE 2003). IEEE, Los Alamitos (2003)
Allan, C., Avgustinov, P., Simon, A., Hendren, L., Kuzins, S., Lhoták, O., de Moor, O., Sereni, D., Sittamplan, G., Tibble, J.: Adding Trace Matching with Free Variables to AspectJ. In: OOPSLA 2005, San Diego, California, USA (October 2005)
Armoni, R., Fix, L., Flaisher, A., Gerth, R., Ginsburg, B., Kanza, T., Landver, A., Mador-Haim, S., Singerman, E., Tiemeyer, A., Vardi, M.Y., Zbar, Y.: The ForSpec Temporal Logic: A new Temporal Property-Specification Language. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, p. 296. Springer, Heidelberg (2002)
Beer, I., Ben-David, S., Eisner, C., Fisman, D., Gringauze, A., Rodeh, Y.: The temporal logic sugar. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 363. Springer, Heidelberg (2001)
Bodden, E.: J-LO, a tool for runtime checking temporal assertions. Master’s thesis, RWTH Aachen University, Germany (2005), available from: http://www-i2.informatik.rwth-aachen.de/JLO/
Chilimbi, T.M.: Asymptotic Runtime Verification through Lightweight Continous Program Analysis (invited talk). In: Fifth Workshop on Runtime Verification (RV 2005). ENTCS. Elsevier, Amsterdam (to be published, 2005)
Clarke Jr, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Douence, R., Fradet, P., Südholt, M.: Composition, reuse and interaction analysis of stateful aspects. In: Murphy, G.C., Lieberherr, K.J. (eds.) Proc. of the 3rd intl. conf. on Aspect-oriented software development (AOSD 2004). ACM Press, New York (2004)
Douence, R., Fritz, T., Loriant, N., Menaud, J.-M., Ségura-Devillechaise, M., Südholt, M.: An expressive aspect language for system applications with arachne. In: Proc. of the 4th intl. conf. on Aspect-oriented software development (AOSD 2005). ACM Press, New York (2005)
Douence, R., Motelet, O., Südholt, M.: A formal definition of crosscuts. In: Yonezawa, A., Matsuoka, S. (eds.) Reflection 2001. LNCS, vol. 2192, p. 170. Springer, Heidelberg (2001)
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: ICSE 1999: Proceedings of the 21st intl. conf. on Software engineering. IEEE Computer Society Press, Los Alamitos (1999)
FarÃas, A., Südholt, M.: On components with explicit protocols satisfying a notion of correctness by construction. In: Meersman, R., Tari, Z., et al. (eds.) CoopIS 2002, DOA 2002, and ODBASE 2002. LNCS, vol. 2519. Springer, Heidelberg (2002)
Finkbeiner, B., Sipma, H.: Checking Finite Traces using Alternating Automata. Formal Methods in System Design 24(2), 101–127 (2004)
Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design patterns: Abstraction and reuse of object-oriented design. In: Nierstrasz, O. (ed.) ECOOP 1993. LNCS, vol. 707, pp. 406–431. Springer, Heidelberg (1993)
Holzmann, G.J.: The SPIN model checker: primer and reference manual. Addison-Wesley, Boston (2003)
Klose, K., Ostermann, K.: Back to the future: Pointcuts as predicates over traces. In: Foundations of Aspect-Oriented Languages workshop (FOAL 2005) (2005)
Pnueli, A.: The temporal logic of programs. In: Proc. of the 18th IEEE Symp. on the Foundations of Computer Science. IEEE Computer Society Press, Los Alamitos (1977)
Stolz, V., Bodden, E.: Temporal Assertions using AspectJ. In: Fifth Workshop on Runtime Verification (RV 2005). ENTCS. Elsevier, Amsterdam (to be published, 2005)
Vanderperren, W., Suvée, D., Cibrán, M.A., De Fraine, B.: Stateful Aspects in JAsCo. In: Gschwind, T., Aßmann, U., Nierstrasz, O. (eds.) SC 2005. LNCS, vol. 3628, pp. 167–181. Springer, Heidelberg (2005)
Walker, R.J., Viggers, K.: Implementing protocols via declarative event patterns. In: Taylor, R., Dwyer, M. (eds.) Proc. of the 12th ACM SIGSOFT Intl. Symp. on Foundations of Software Engineering. ACM Press, New York (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bodden, E., Stolz, V. (2006). Tracechecks: Defining Semantic Interfaces with Temporal Logic. In: Löwe, W., Südholt, M. (eds) Software Composition. SC 2006. Lecture Notes in Computer Science, vol 4089. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11821946_10
Download citation
DOI: https://doi.org/10.1007/11821946_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37657-6
Online ISBN: 978-3-540-37659-0
eBook Packages: Computer ScienceComputer Science (R0)