More Web Proxy on the site http://driver.im/

Article

Aspect-oriented programming with model checking

Authors:

Naoyasu Ubayashi,

Tetsuo TamaiAuthors Info & Claims

AOSD '02: Proceedings of the 1st international conference on Aspect-oriented software development

Pages 148 - 154

https://doi.org/10.1145/508386.508405

Published: 22 April 2002 Publication History

Abstract

Aspect-oriented programming (AOP) is a programming paradigm such that crosscutting concerns including synchronization policies, resource sharing and performance optimizations over objects are modularized as aspects that are separated from objects. A compiler, called a weaver, weaves aspects and objects together into a program. In AOP, however, it is not easy to verify the correctness of a woven program because crucial behaviors are strongly influenced by aspect descriptions. In order to deal with such problem, this paper proposes an automatic verification approach using model checking that verifies whether the woven program contains unexpected behaviors such as deadlocks. The objectives of this paper are as follows: 1) to verify the correctness of AOP-based programs using model checking, 2) to provide AOP-based model checking frameworks.

References

[1]

Aksit, M. and Tripathi, A.: Data Abstraction Mechanisms in Sina/ST, Proc. OOPSLA'88, pp.265-275, 1988.

Digital Library

[2]

AspectJ. http://aspectj.org/.

[3]

The AspectJ Programming Guide, 2001.

[4]

Bandera. http://www.cis.ksu.edu/ santos/bandera/.

[5]

Beck, K.: Extreme Programming Explained: Embrace Change, Addison-Wesley, 1999.

Digital Library

[6]

Clarke, E., Grumberg, O., and Peled, D.: Model Checking, The MIT Press, 1999.

Digital Library

[7]

Corbett, J. C., Dwyer, M. B., Hatcliff, J., Laubach, S., Pasareanu, C. S., and Zheng, H.: Bandera: Extracting Finite-state Models from Java Source Code, Proc. ICSE 2000, 2000.

Digital Library

[8]

Czarnecki, K. and Eisenecker, U. W.: Generative Programming, Addison-Wesley, 2000.

Digital Library

[9]

Demeter Project. http://www.ccs.neu.edu/research/demeter/.

[10]

Elrad, T., Filman, R. E. and Bader A.: Aspect-oriented programming, Communications of the ACM, vol.44, no.10, pp.29-32, 2001.

Digital Library

[11]

Harrison, W. and Ossher, H.: Subject-oriented Programming, Proc. OOPSLA'93, pp.411-428, 1993.

Digital Library

[12]

Havelund, K.: Java PathFinder User Guide, 1999.

[13]

Holzmann, C. J. and Smith, M. H.: The Model Checker SPIN, IEEE trans. SE, vol.23, no.5, pp.279-295, 1997.

Digital Library

[14]

Jackson, D.: Aloca: the alloy constraint analyzer, Proceedings of ICSE 2000, 2000.

Digital Library

[15]

Kendall, E. A.: Role Model Designs and Implemantations with Aspect-oriented Programming, Proc. OOPSLA'99, pp.353-369, 1999.

Digital Library

[16]

Kiczales, G., Lamping, J., Mendhekar A., Maeda, C., Lopes, C., Loingtier, J. and Irwin, J.: Aspect-Oriented Programming, Proc. ECOOP'97, Lecture Notes in Computer Science, Springer, vol.1241, pp.220-242, 1997.

[17]

McMillan, K. L.: Symbolic Model Checking: An Approach to the State Explosion Problem, Kluwer Academic, 1993.

Digital Library

[18]

Meyer, B.: Object-Oriented Software Construction, 2nd Edition, Prentice Hall, 2000.

Digital Library

[19]

Nelson, T., Cowan, D. and Alencar, P.: Supporting Formal Verification of Crosscutting Concerns, Proc. REFLECTION 2001, Lecture Notes in Computer Science, Springer, vol.2192, pp.153-169, 2001.

Digital Library

[20]

K. Rustan M. Leino, Greg Nelson, and James B. Saxe: ESC/Java User's Manual, 2000.

[21]

Tamai, T.: Objects and roles: modeling based on the dualistic view, Information and Software Technology, Vol.41, No.14, pp.1005-1010, 1999.

[22]

Ubayashi, N. and Tamai, T.: Separation of Concerns in Mobile Agent Applications, Proc. REFLECTION 2001, Lecture Notes in Computer Science, Springer, vol.2192, pp.89-109, 2001.

Digital Library

Cited By

AlSobeh AMagableh A(2023)BlockASP: A Framework for AOP-Based Model Checking Blockchain SystemIEEE Access10.1109/ACCESS.2023.332506011(115062-115075)Online publication date: 2023
https://doi.org/10.1109/ACCESS.2023.3325060
Asteasuain FCalonge FGamboa P(2020)Exploiting Anti-scenarios for the Non Realizability ProblemComputer Science – CACIC 201910.1007/978-3-030-48325-8_11(157-171)Online publication date: 14-May-2020
https://doi.org/10.1007/978-3-030-48325-8_11
Le HTruong NNanthaamornphong A(2017)A Model-Based Method for Modeling and Verifying Event-Based Aspect-Oriented ApplicationsRecent Advances and Future Prospects in Knowledge, Information and Creativity Support Systems10.1007/978-3-319-70019-9_23(281-289)Online publication date: 2-Dec-2017
https://doi.org/10.1007/978-3-319-70019-9_23
Show More Cited By

Index Terms

Aspect-oriented programming with model checking
1. Software and its engineering
2. Theory of computation
  1. Logic
    1. Verification by model checking

Recommendations

Aspect-oriented modeling and verification with finite state machines
Special section on trust and reputation management in future computing systmes and applications

Aspect-oriented programming modularizes crosscutting concerns into aspects with the advice invoked at the specified points of program execution. Aspects can be used in a harmful way that invalidates desired properties and even destroys the conceptual ...
Cooperative aspect-oriented programming

Aspect-oriented programming (AOP) seeks to improve software modularity via the separation of cross-cutting concerns. AOP proponents often advocate a development strategy where programmers write the main application (base code), ignoring cross-cutting ...
Model Checking Aspect-Oriented Design Specification
COMPSAC '07: Proceedings of the 31st Annual International Computer Software and Applications Conference - Volume 01

Aspects can be used in a harmful way that invalidates desired properties. Rigorous specification and analysis of aspect design is thus highly desirable. This paper presents an approach to model-checking state-based specification of aspect-oriented ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

AOSD '02: Proceedings of the 1st international conference on Aspect-oriented software development

April 2002

162 pages

ISBN:158113469X

DOI:10.1145/508386

Conference Chair:
Harold Ossher
IBM T.J. Watson Research Center
,
Program Chair:
Gregor Kiczales
University of British Columbia

Copyright © 2002 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

University of Twente: University of Twente
PATO: Post Academisch Tecbnisch Onderwijs
KNAW: Koninklijke Nederlandse Akademie van Wetenschappen
CTIT: Centre for Telematics and Information Technology
IBMR: IBM Research
NWO: Dutch Orgartisation for Scientific Research
IPA: Institute for Software and Arithmetic
AITO: Association Internationale pour les Technologies Objets

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 22 April 2002

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

AOSD02

Sponsor:

University of Twente
PATO
KNAW
CTIT
IBMR
NWO
IPA
AITO

AOSD02: 1st International Conference on Aspect-Oriented Software Development

April 22 - 26, 2002

Enschede, The Netherlands

Acceptance Rates

Overall Acceptance Rate 41 of 139 submissions, 29%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

28
Total Citations
View Citations
1,968
Total Downloads

Downloads (Last 12 months)4
Downloads (Last 6 weeks)0

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

AlSobeh AMagableh A(2023)BlockASP: A Framework for AOP-Based Model Checking Blockchain SystemIEEE Access10.1109/ACCESS.2023.332506011(115062-115075)Online publication date: 2023
https://doi.org/10.1109/ACCESS.2023.3325060
Asteasuain FCalonge FGamboa P(2020)Exploiting Anti-scenarios for the Non Realizability ProblemComputer Science – CACIC 201910.1007/978-3-030-48325-8_11(157-171)Online publication date: 14-May-2020
https://doi.org/10.1007/978-3-030-48325-8_11
Le HTruong NNanthaamornphong A(2017)A Model-Based Method for Modeling and Verifying Event-Based Aspect-Oriented ApplicationsRecent Advances and Future Prospects in Knowledge, Information and Creativity Support Systems10.1007/978-3-319-70019-9_23(281-289)Online publication date: 2-Dec-2017
https://doi.org/10.1007/978-3-319-70019-9_23
Truscan DVain JKoskinen MIqbal J(2015)A Tool-Supported Approach for Introducing Aspects in UPPAAL Timed AutomataSoftware Technologies10.1007/978-3-319-25579-8_20(349-364)Online publication date: 17-Oct-2015
https://doi.org/10.1007/978-3-319-25579-8_20
Thüm TApel SKästner CSchaefer ISaake G(2014)A Classification and Survey of Analysis Strategies for Software Product LinesACM Computing Surveys10.1145/258095047:1(1-45)Online publication date: 1-Jun-2014
https://dl.acm.org/doi/10.1145/2580950
Xiao K(2013)Aspect-Oriented Dynamic Weaving Testing Based on Sequence DiagramsApplied Mechanics and Materials10.4028/www.scientific.net/AMM.336-338.1957336-338(1957-1963)Online publication date: Jul-2013
https://doi.org/10.4028/www.scientific.net/AMM.336-338.1957
Xu DEl-Ariss OXu WWang L(2010)Testing aspect-oriented programs with finite state machinesSoftware Testing, Verification and Reliability10.1002/stvr.44022:4(267-293)Online publication date: 13-Sep-2010
https://doi.org/10.1002/stvr.440
kumar Msharma AGarg S(2009)A study of aspect oriented testing techniques2009 IEEE Symposium on Industrial Electronics & Applications10.1109/ISIEA.2009.5356308(996-1001)Online publication date: Oct-2009
https://doi.org/10.1109/ISIEA.2009.5356308
Majumdar D(2009)Migration from Procedural Programming to Aspect Oriented ParadigmProceedings of the 24th IEEE/ACM International Conference on Automated Software Engineering10.1109/ASE.2009.41(712-715)Online publication date: 16-Nov-2009
https://dl.acm.org/doi/10.1109/ASE.2009.41
Xu DEl-Ariss OXu WWang L(2009)Aspect-oriented modeling and verification with finite state machinesJournal of Computer Science and Technology10.1007/s11390-009-9269-524:5(949-961)Online publication date: 1-Sep-2009
https://dl.acm.org/doi/10.1007/s11390-009-9269-5
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten