The Research On Formal Description Method For Aspect-oriented Statechart Based On CSP

UML has an extensive application and expanding background as the standard of the object-oriented analysis and designing modeling language, and UML extending mechanism could support modeling aspect-oriented, but the state diagram modeled by UML applies the natural language description and chart structure, it lacks the formal accurate semantic and turns against the system's refinement and verification, so it is necessary to import formal method to research the UML statechart.First the paper explains the advantages of the aspect-oriented, expounds the core idea of the aspect-oriented program, and summarize some researches of the formal aspect-oriented by the AOP extension and supporting component design of the formal language B and the AOP formal method AO-RT-Z during recent years. Then through UML expanding mechanism, the aspect-oriented state diagram is divided into the core state diagram and the aspect state diagram which are combined to implement the aspect-oriented state diagram modeling in the use of weaving method mapped by the weave event, instead the previous weaving method description is only suitable for a core component and an aspect. The paper expands the weaving description and gives a method which could describe that many aspects weave core components or aspects. This method illustrates the sequence of the weaving core components or aspects by many aspects, and establishes the foundation for the modeling complicated aspect-oriented state diagram.In order to refine and verify the system, the paper gives a rule which CSP describes the aspect- oriented state diagram. Through the rule, six typical states in the oriented-aspect state diagram are defined as CSP, then and two examples, the limited buffer and ATM, are modeled as the oriented-aspect state diagram and gave CSP description. At last, for the correctness of the detective description, the paper verifies the description of ATM aspect-oriented state diagram described by CSP via FDR which is the modeling test tool matched with CSP, and proves the feasibility and validity of the oriented-aspect state diagram described by CSP.