Aspect-Oriented Programming with Model Checking

Naoyasu Ubayashi, Tetsuo Tamai

Research output: Chapter in Book/Report/Conference proceedingConference contribution

36 Citations (Scopus)

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.

Original languageEnglish
Title of host publication1st International Conference on Aspect-Oriented Software Development
EditorsG. Kinzales, G. Kiczales
Pages148-154
Number of pages7
Publication statusPublished - Dec 1 2002
Externally publishedYes
Event1st International Conference on Aspect-Oriented Software Development (AOSD 2002) - Enschede, Netherlands
Duration: Apr 22 2002Apr 26 2002

Publication series

Name1st International Conference on Aspect-Oriented Software Development

Other

Other1st International Conference on Aspect-Oriented Software Development (AOSD 2002)
CountryNetherlands
CityEnschede
Period4/22/024/26/02

Fingerprint

Aspect oriented programming
Model checking
Computer programming
Synchronization

All Science Journal Classification (ASJC) codes

  • Engineering(all)

Cite this

Ubayashi, N., & Tamai, T. (2002). Aspect-Oriented Programming with Model Checking. In G. Kinzales, & G. Kiczales (Eds.), 1st International Conference on Aspect-Oriented Software Development (pp. 148-154). (1st International Conference on Aspect-Oriented Software Development).

Aspect-Oriented Programming with Model Checking. / Ubayashi, Naoyasu; Tamai, Tetsuo.

1st International Conference on Aspect-Oriented Software Development. ed. / G. Kinzales; G. Kiczales. 2002. p. 148-154 (1st International Conference on Aspect-Oriented Software Development).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Ubayashi, N & Tamai, T 2002, Aspect-Oriented Programming with Model Checking. in G Kinzales & G Kiczales (eds), 1st International Conference on Aspect-Oriented Software Development. 1st International Conference on Aspect-Oriented Software Development, pp. 148-154, 1st International Conference on Aspect-Oriented Software Development (AOSD 2002), Enschede, Netherlands, 4/22/02.
Ubayashi N, Tamai T. Aspect-Oriented Programming with Model Checking. In Kinzales G, Kiczales G, editors, 1st International Conference on Aspect-Oriented Software Development. 2002. p. 148-154. (1st International Conference on Aspect-Oriented Software Development).
Ubayashi, Naoyasu ; Tamai, Tetsuo. / Aspect-Oriented Programming with Model Checking. 1st International Conference on Aspect-Oriented Software Development. editor / G. Kinzales ; G. Kiczales. 2002. pp. 148-154 (1st International Conference on Aspect-Oriented Software Development).
@inproceedings{f02ca56bc26c469d862df2bb92cbe630,
title = "Aspect-Oriented Programming with Model Checking",
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.",
author = "Naoyasu Ubayashi and Tetsuo Tamai",
year = "2002",
month = "12",
day = "1",
language = "English",
isbn = "158113469X",
series = "1st International Conference on Aspect-Oriented Software Development",
pages = "148--154",
editor = "G. Kinzales and G. Kiczales",
booktitle = "1st International Conference on Aspect-Oriented Software Development",

}

TY - GEN

T1 - Aspect-Oriented Programming with Model Checking

AU - Ubayashi, Naoyasu

AU - Tamai, Tetsuo

PY - 2002/12/1

Y1 - 2002/12/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=0141761303&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0141761303&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:0141761303

SN - 158113469X

T3 - 1st International Conference on Aspect-Oriented Software Development

SP - 148

EP - 154

BT - 1st International Conference on Aspect-Oriented Software Development

A2 - Kinzales, G.

A2 - Kiczales, G.

ER -