Abstract
Software systems specifications are often described as a set of typical scenarios. Some of the desired scenarios are crosscut by other requirements, called aspects, also naturally described as scenarios. Aspect descriptions are independent of the description of the non-aspectual scenarios, but the crosscutting relationship between them has to be specified, so for each aspect a description of its join-points is provided. When aspectual scenarios are added to the system, we need to prove that every execution is equivalent to one in which the aspectual scenarios occur as blocks of operations immediately at their join-points, and all the other operations form a sequence of non-aspectual scenarios, interrupted only by the aspectual scenarios. We extend an existing method of automatic verification for non-aspect systems to the case of systems with scenario-based aspect specifications. A prototype implementation based on Cadence SMV is also extended accordingly.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Glusman, M., Katz, S.: A mechanized proof environment for the convenient computations proof method. Formal Methods in System Design 23, 115–142 (2003), http://www.cs.technion.ac.il/Labs/ssdl/pub/conv_PVS
Glusman, M., Katz, S.: Model checking conformance with scenario-based specifications. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 328–340. Springer, Heidelberg (2003)
Harel, D., Marelly, R.: Come, let’s play: Scenario-based programming using LSC’s and the play-engine. Springer, Heidelberg (2003)
Hatcliff, J., Dwyer, M.: Using the Bandera Tool Set to model-check properties of concurrent Java software. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 39–58. Springer, Heidelberg (2001)
Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. International Journal on Software Tools for Technology Transfer (STTT) 2(4) (2000)
Araújo, J., Whittle, J., Kim, D.: Modeling and composing scenario-based requirements with aspects. In: The 12th IEEE International Requirements Engineering Conference (RE 2004), Kyoto, Japan, September 2004, pp. 58–67 (2004)
Kiczales, G., Hilsdale, E., Hugunin, J., Kersten, M., Palm, J., Griswold, W.G.: An overview of AspectJ. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol. 2072, pp. 327–353. Springer, Heidelberg (2001)
Krishnamurthi, S., Fisler, K., Greenberg, M.: Verifying aspect advice modularly. In: SIGSOFT FSE, 2004, pp. 137–146 (2004)
Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems - safety. Springer, Heidelberg (1995)
McMillan, K.L.: Getting started with SMV, Cadence Labs (March 1999)
Peled, D.: Software reliability methods. Springer, Heidelberg (2001)
Rumbaugh, J., Jacobson, I., Booch, G.: The Unified Modeling Language reference manual, vol. 2. Addison-Wesley, Reading (2004)
Sereni, D., de Moor, O.: Static analysis of aspects. In: AOSD 2003, pp. 30–39 (2003)
Sihman, M., Katz, S.: Superimposition and aspect-oriented programming. BCS Computer Journal 46(5), 529–541 (2003), http://www.cs.technion.ac.il/~katz/cj.ps
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Katz, E., Katz, S. (2005). Verifying Scenario-Based Aspect Specifications. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds) FM 2005: Formal Methods. FM 2005. Lecture Notes in Computer Science, vol 3582. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11526841_29
Download citation
DOI: https://doi.org/10.1007/11526841_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27882-5
Online ISBN: 978-3-540-31714-2
eBook Packages: Computer ScienceComputer Science (R0)