UML作为面向对象分析和设计建模语言的标准,有广泛的应用和扩展背景,通过UML的扩展机制使其支持面向方面状态图的建模,但UML建模的状态图采用的是自然语言描述及图表结构,缺乏形式化的精确语义,不利于系统的求精和验证,从而有必要引入形式化方法对其进行研究。本文首先说明了面向方面存在的优点,阐述了面向方面编程的核心思想,并通过形式化语言B的AOP扩充以及支持组件设计和AOP的形式化方法AO-RT-Z综述了最近几年在形式化面向方面的研究工作。然后通过UML扩展机制把面向方面状态图分成核心状态图和方面状态图,利用编织事件映射为织入方法将两者联系起来以实现面向方面状态图的建模,但原有的织入方法描述只适用于一个核心组件和一个方面。本文扩展了织入方法的描述,给出了一种描述多个方面同时织入核心组件或方面的方法,此方法说明了多个方面织入核心组件或者方面的次序,为复杂的面向方面状态图的建模奠定了基础。为了对面向方面的状态图进行进一步的求精和验证,本文给出一种通过CSP描述方面状态图的规则,通过规则对面向方面状态图中包含的6个典型的状态进行CSP定义,然后对有限缓冲和ATM自动取款两个实例进行面向方面状态图的建模和CSP的描述。为了检测描述的正确性,本文最后通过与CSP匹配的模型检测工具FDR对ATM自动取款机面向方面状态图的CSP描述进行验证,证明了CSP描述面向方面状态图的可行性和正确性。