Abstract
The model checking of applications of aspects is explained, by showing the stages and proof obligations when a collection of generic aspects (called a superimposition) is combined with a basic program. We assume that both the basic program and the collection of aspects have their own specifications. The Bandera tool for Java programs is used to generate input for model checkers, although any similar tool could be employed. New verification aspects and superimpositions are defined to modularize the proofs, and separate the proof-related code from the program and the aspects. This allows generating and activating a series of model checking tasks automatically each time a superimposition is applied to a basic program, achieving superimposition validation. A case study that monitors and checks an underlying bounded buffer program is presented.
Dedicated to Zohar: teacher, advisor, and friend, from whom I learned about the importance of both invariance and liveness in multiple aspects of verification and life.-Shmuel
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
M. Aksit, K. Wakita, J. Bosch, L. Bergmans, and A. Yonezawa. Abstracting Object Interactions Using Composition Filters. In ECOOP’93 Workshop on Object-Based Distributed Programming, LNCS 791, pages 152-184, 1994.
E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, 1999.
J. Hatcliff and M. Dwyer. Using the Bandera tool set to model-check properties of concurrent Java software. In CONCUR 2001, LNCS 2154, pages 39-58, Aug 2001.
J. Hatcliff and O. Tkachuk. The Bandera tools for model-checking Java source code: A user’s manual. Technical report, Kansas State University, Department of Computing and Information Sciences, March 2001. http://www.cis.ksu.edu/%7Esantos/bandera/tut/tut-html.tar.gz.
K. Havelund and T. Pressburger. Model checking Java programs using Java PathFinder. International Journal on Software Tools for Technology Transfer (STTT), 2(4), Apr 2000.
G. J. Holzmann and M. H. Smith. The model checker SPIN. IEEE trans. SE, 23(5):279–295, 1997.
R. Iosif and R. Sisto. dSpin: A dynamic extension of Spin. In Proc. of the 6th SPIN Workshop, LNCS 1680, pages 261-276, Sep 1999.
S. Katz. A superimposition control construct for distributed systems. ACM Trans. on Programming Languages and Systems, 15(2):337–356, Apr 1993.
G. Kiczales, E. Hilsdale, J. Hugunin, M. Kersten, J. Palm, and W. G. Griswold. An overview of AspectJ. In Proceedings ECOOP 2001, LNCS 2072, pages 327-353, Jun 2001. http://aspectj.org.
G. Kiczales, J. Lamping, A. Mendhekar, C. Maeda, C. Lopes, J.-M. Loingtier, and J. Irwin. Aspect-oriented programming. In Proceedings ECOOP’97, LNCS 1241, pages 220-242, Jun 1997.
K. L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic, 1993.
A. Pnueli, O. Shtrichman, and M. Siegel. The code validation tool(CVT)) — automatic verification of a compilation process. Software Tools for Technology Transfer, 2:192–201, 1999.
Z. Shtadler and O. Grumberg. Network grammars, communication behaviors and automatic verification. In Proc. of the international workshop on Automatic verification methods for finite state systems, pages 151-165. Springer-Verlag, 1990.
M. Sihman and S. Katz. Superimposition and aspect-oriented programming. BCS Computer Journal, vol. 46, no.5, 2003. Available at http://www.cs.technion.ac.il/~katz/cj.ps.
P. Tarr, H. Ossher, W. Harrison, and S. M. S. Jr. N degrees of separation: Multidimensional separation of concerns. In ACM ICSE’99, pages 107-119, May 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Katz, S., Sihman, M. (2003). Aspect Validation Using Model Checking. In: Dershowitz, N. (eds) Verification: Theory and Practice. Lecture Notes in Computer Science, vol 2772. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39910-0_18
Download citation
DOI: https://doi.org/10.1007/978-3-540-39910-0_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21002-3
Online ISBN: 978-3-540-39910-0
eBook Packages: Springer Book Archive