基于Statecharts的面向方面软件设计与验证

为了及时解决由于关注点横切所产生的“代码交织”与“代码散布”问题，提出了一种基于Statecharts的面向方面软件设计方法，并利用线性时态逻辑验证了编织过程的有效性。此外，为了验证方面Statecharts的介入是否破坏了基本Statechart的相关行为，引入扩展层次自动机解释面向方面Statechart的操作语义，使用线性时态逻辑描述系统的关键属性。最后通过一个案例证明了该设计方法的可行性。