从软件工程中软件生命周期的角度分析,软件架构是软件的核心结构与行为,因而软件架构的设计是软件设计的核心,也是随后进行代码开发的基础。因此软件架构设计的重要性不言而喻。由于软件架构设计本身是一种建模活动,如何对软件架构设计的标准建模语言UML进行正确性验证是一个难题。传统软件验证方法有着不够精确、非自动化等不足。另外,对UML进行正确性验证需要得到UML的形式化语义,而UML本身是一种图形化的表示方法,不具有形式化的语义。因此本文将采用形式化方法来对UML模型进行形式化描述,即为其赋予等价的形式化语义,再根据其语义进行形式化验证。为了进一步精确描述UML模型的语义,为其提供OCL约束是一种主流方法。而OCL约束需要人手工编写,同样具有正确性难以保证、人员开销等问题,因此为UML模型自动生成OCL约束模板是一种很好的解决方法,生成的OCL模板可供软件设计人员参考,从而提高了软件工程的整体效率。本文也将对OCL约束自动生成进行研究。UML是软件设计过程事实上的标准建模语言。本文首先从历史发展、子图种类、建模工具和以XMI表示的UML四个角度对UML作了简要的介绍,并具体介绍了即将研究的两种UML子图：类图和状态图。同时介绍了形式化方法的基本概念和主要分支，并总结了国内外现有的对UML形式化的研究。最后介绍了UML的标准子语言OCL、采用的形式化语言情态演算和它的具体实现——逻辑编程语言Prolog,并进一步分析了从UML转换到情态演算的可行性,从理论上确定了给出的解决方案的正确性。本文随后给出了基于情态演算的UML形式化描述方法。首先分析了选择UML类图和状态图作为研究对象的意义,再分别对UML类图和状态图进行形式化描述：先是给出了两种子图的一种形式化语义结构；再分析了两种子图元素与数理逻辑和情态演算元素的对应关系；又提出了两种子图到数理逻辑语句和Prolog代码的转换算法,并以伪代码的形式给出。然后着重定义了UML模型的两种基本错误类型：领域无关的UML模型语法错误和领域相关的UML模型语义错误,并给出具体错误实例和自动生成的Prolog代码。进一步,本文讨论了如何实现对UML模型的OCL约束模板自动生成。首先强调了OCL约束自动生成的研究意义,同时给出了OCL约束的应用范围。从而进一步分析了如何在UML模型中提取OCL约束的目标应用对象,并给出了一种提取算法。最后给出了该提取算法的Perl示例代码的具体实现。作为上述理论的补充和可行性证明,后续章节详细介绍了以UML子图到情态演算的转换算法和OCL约束模板自动生成算法为基础而设计并实现的UML形式化验证原型工具USCVSC。首先建立了该原型工具的系统实现框架和代码框架。其次给出了该原型工具的用户界面,并详细描述了其中的4个基本子功能界面。最后说明了,通过此原型工具,可以实现UML模型语法检查和语义错误验证,以及OCL约束模板自动生成的综合性功能。最后,本文对USCVSC原型工具的使用进行了介绍,并结合一个大学教学系统和大学申请系统的实际案例来对原型工具的基本功能进行演示。先描述了该应用实例的特点,并用UML建模工具对其类图和状态图进行设计。接下来则利用USCVSC原型工具对预定义的UML模型错误进行验证：对于UML语法错误的检查可以在USCVSC原型工具中完成,对于UML语义错误的验证则需要USCVSC原型工具和Prolog解析器一起协同完成。最后演示了如何利用USCVSC原型工具为UML类图自动生成OCL约束模板,并给出了示例OCL约束语句。综上所述,本文以形式化语言情态演算为描述语言来对UML模型进行形式化验证以及自动生成OCL约束,并最终实现了原型工具。使得UML模型中多初始状态、监护条件中无逻辑运算符等语法错误得以发现,同时也能验证出UML模型中需求不完整和需求逻辑错误等语义错误。从而能帮助软件设计人员修正最初的UML模型设计,避免在软件工程后续阶段不必要的系统开销。最终达到使软件工程各阶段的整体效率得到提升的目标,为软件工程自动化做出了贡献。