A Formal Description Method for Aspect-Oriented Statechart Based on CSP

Author

Wang, Bin ; Zhu, Chunhua ; Sheng, Jinfang

Author_Institution

Sch. of Inf. Sci. & Eng., Central South Univ., Changsha, China

Volume

2

fYear

2008

fDate

20-22 Dec. 2008

Firstpage

750

Lastpage

753

Abstract

Aspect-oriented software development method solves crosscutting problem by separating concerns and aspect-oriented software can be modeled by extending UML. This paper proposes a method to describe the aspects and core components as well as weaving between them through introducing aspect into UML statechart. Then the extended UML statechart is described in formal semantics of CSP, a kind of process algebra, which introduces formal dynamic semantics into UML and makes it possible to verify and prove the model in a formal way. The ATM system is used as an example to illustrate the efficiency of the aspect-oriented statechart described in CSP. Finally, FDR, a model checker, is used to perform verification of the CSP code for the ATM system.

Keywords

Unified Modeling Language; communicating sequential processes; object-oriented programming; program verification; software engineering; ATM system; FDR; aspect-oriented software development method; aspect-oriented statechart; communicating sequential process code verification; core components; crosscutting problem; extended UML statechart; formal description method; formal dynamic semantics; model checker; process algebra; Algebra; Computer science; Cryptography; Doped fiber amplifiers; Information science; Object oriented modeling; Packaging; Programming; Unified modeling language; Weaving; CSP; aspect-oriented statechart; formal semantics; weaving;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Science and Computational Technology, 2008. ISCSCT '08. International Symposium on

Conference_Location

Shanghai

Print_ISBN

978-1-4244-3746-7

Type

conf

DOI

10.1109/ISCSCT.2008.358

Filename

4731731