Tracechecks: Defining Semantic Interfaces with Temporal Logic

  • Eric Bodden
  • Volker Stolz
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4089)


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.


Temporal Logic Regular Expression Linear Temporal Logic Execution Trace Linear Temporal Logic Formula 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Å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)Google Scholar
  2. 2.
    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)Google Scholar
  3. 3.
    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)CrossRefGoogle Scholar
  4. 4.
    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)CrossRefGoogle Scholar
  5. 5.
    Bodden, E.: J-LO, a tool for runtime checking temporal assertions. Master’s thesis, RWTH Aachen University, Germany (2005), available from:
  6. 6.
    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)Google Scholar
  7. 7.
    Clarke Jr, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  8. 8.
    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)Google Scholar
  9. 9.
    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)Google Scholar
  10. 10.
    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)CrossRefGoogle Scholar
  11. 11.
    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)Google Scholar
  12. 12.
    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)CrossRefGoogle Scholar
  13. 13.
    Finkbeiner, B., Sipma, H.: Checking Finite Traces using Alternating Automata. Formal Methods in System Design 24(2), 101–127 (2004)zbMATHCrossRefGoogle Scholar
  14. 14.
    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)CrossRefGoogle Scholar
  15. 15.
    Holzmann, G.J.: The SPIN model checker: primer and reference manual. Addison-Wesley, Boston (2003)Google Scholar
  16. 16.
    Klose, K., Ostermann, K.: Back to the future: Pointcuts as predicates over traces. In: Foundations of Aspect-Oriented Languages workshop (FOAL 2005) (2005)Google Scholar
  17. 17.
    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)Google Scholar
  18. 18.
    Stolz, V., Bodden, E.: Temporal Assertions using AspectJ. In: Fifth Workshop on Runtime Verification (RV 2005). ENTCS. Elsevier, Amsterdam (to be published, 2005)Google Scholar
  19. 19.
    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)CrossRefGoogle Scholar
  20. 20.
    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)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Eric Bodden
    • 1
  • Volker Stolz
    • 1
  1. 1.Software Modeling and Verification (MOVES)RWTH Aachen UniversityAachenGermany

Personalised recommendations