| 基于Statecharts的面向方面软件设计与验证 |
| |
| 引用本文： | 文欣秀,虞慧群.基于Statecharts的面向方面软件设计与验证[J].医学教育探索,2011(5):601-608. |
| |
| 作者姓名： | 文欣秀 虞慧群 |
| |
| 作者单位： | 华东理工大学信息科学与工程学院，上海 200237;华东理工大学信息科学与工程学院，上海 200237 |
| |
| 基金项目： | 国家自然科学基金(60773094);上海市曙光计划（07SG32） |
| |
| 摘 要： | 为了及时解决由于关注点横切所产生的“代码交织”与“代码散布”问题，提出了一种基于Statecharts的面向方面软件设计方法，并利用线性时态逻辑验证了编织过程的有效性。此外，为了验证方面Statecharts的介入是否破坏了基本Statechart的相关行为，引入扩展层次自动机解释面向方面Statechart的操作语义，使用线性时态逻辑描述系统的关键属性。最后通过一个案例证明了该设计方法的可行性。
|
| 关 键 词： | 面向方面 Statechart 线性时态逻辑 编织 模型检测 |
Aspect Oriented Software Design and Verification Based on Statecharts |
| |
| WEN Xin-xiu and YU Hui-qun.Aspect Oriented Software Design and Verification Based on Statecharts[J].Researches in Medical Education,2011(5):601-608. |
| |
| Authors: | WEN Xin-xiu and YU Hui-qun |
| |
| Institution: | School of Information Science and Engineering, East China University of
Science and Technology, Shanghai 200237, China;School of Information Science and Engineering, East China University of
Science and Technology, Shanghai 200237, China |
| |
| Abstract: | In order to solve the problems of code crosscutting and code tangling resulting from the crosscut of concerns, this paper proposed an aspect oriented software design method based on Statecharts, and further verified the effective of weaving process by utilizing linear time temporal logic. Furthermore, in order to verify whether the intervention of aspect Statecharts destroys the certain behaviors of base Statechart, this paper introduced the extended hierarchical automaton to explain the operational semantics of aspect oriented Statechart, and described the key properties of software system by utilizing the linear time temporal logic. Finally, a case study demonstrated the feasibility of the proposed method. |
| |
| Keywords: | aspect orientation Statechart linear time temporal logic weaving model checking |
|
| 点击此处可从《医学教育探索》浏览原始摘要信息 |
| 点击此处可从《医学教育探索》下载免费的PDF全文 |
