Title :
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
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;
Conference_Titel :
Computer Science and Computational Technology, 2008. ISCSCT '08. International Symposium on
Conference_Location :
Shanghai
Print_ISBN :
978-1-4244-3746-7
DOI :
10.1109/ISCSCT.2008.358
