本文提出一种基于Object-Z的形式化面向方面建模语言以及建模方法。形式化语言中的方面规范提供了观察基本模块和方面模块的行为、并描述它们相互关系的方法。而编织机制则将这两类模块系统地集成为一个完整的系统模型。该方法能有效地简化系统建模、提高系统模型的可复用性，也为进一步验证系统性质提供了理论基础。主要工作包括以下三个方面： 1.提出在Object-Z形式化语言基础上扩展的面向方面建模语言的语法以及语义，并使用说明方面优先级的合成模式来解决编织时可能出现的冲突。 2.结合软件工程中的建模方法以及面向方面软件开发的特性，形成基于形式化方法的面向方面建模的步骤和基本的方法框架，并通过一个具体案例来演示基于形式化的面向方面建模方法。 3.根据形式化语言中的规格说明判断模型的正确性，以确保软件的质量。