《软件架构理论与实践》 —3.5.4　第4层：形式化模型

3.5.4　第4层：形式化模型

第4层是形式化模型。在目前通用的软件架构建模方法中，通常还是非形式化方法。然而这种非形式化方法并不能很好地描述不同系统的组成部分之间的一些特性，已经难以适应软件架构建模的进一步发展。因此，在软件架构的建模过程中必须要有具备精确描述能力的形式化方法和研究工具。目前在软件架构建模领域，形式化方法的关注热点主要集中在使用形式化规格说明语言进行建模和基于UML形式化建模这两方面。表3-3对这两个研究热点进行了比较分析。

表3-3　两个形式化研究热点的比较

形式化建模的理论基础是形式化规格说明语言，这种语言采用数学的形式描述系统将要“做什么”，用带有精确定义的形式语言来描述程序的功能，它是设计与实现程序的出发点，也作为验证程序是否正确的依据。关于形式化规格说明语言的研究主要分为以下两类：

1）基于模型的方法：其基本思想是利用一些已知特性的数学抽象来为目标软件系统的状态特征和行为特征构造模型。如Z语言、B语言、VDM、Petri网等都是基于模型的方法。每一种基于模型的方法都会提出一套自己的规范，然后采用数学方法来说明规范，但是规范所使用的数学工具并不能保证规范是正确的。当然也可以使用证明技术来辅助确认，但这也只能简单地缩短形式化方法与现实世界之间的距离，并不能消除它。

2）代数方法：它为目标软件系统的规格说明提供了一些特殊的机制，包括描述抽象概念并进行进程间连接和推理的方法。如CSP、CCS、CLEAR等都是代数方法。代数方法对开发人员的要求很高，对于架构的描述往往难以理解，导致架构只能为“小众”服务，同时代数方法可扩展性差，对架构进行修改后需要重新进行代数计算和验证，代价很大。

由于形式化建模方法本身的局限性，研究人员逐渐把视线转移到UML模型的形式化上。鉴于UML建模的龙头地位，基于UML模型的形式化无论在理论上还是应用上都较易普及。UML的语法结构采用形式化规格说明，是精确的；但是其语义部分采用自然语言描述，缺乏精确性，使得不能对UML模型进行分析和论证。目前，对UML语义的形式化研究主要有以下三种思路：

1）对UML核心语法进行形式化，使得UML成为精确的语言：其目标是运用浅显的数学知识将UML发展为一种精确的（形式化的）建模语言[79]。这种方法通过对UML核心语法进行形式化，使得UML符合形式化规格说明语言的要求。它是在元模型层次上进行的，可保证在此基础上建立的UML模型层和用户对象层有可靠的数学模型基础，为构造、操纵和细化UML模型提供一种通用的办法。在此基础上建立的UML模型具有可靠的数学基础，便于细化和验证，但这种思路的实现难度较大，而且核心语法进行形式化处理后，存在与现有的各种UML图形不匹配的问题。

2）约束语言方法：此方法的思想是通过设置一个好的约束来消除语义歧义性，比如扩展OCL以加强其约束能力而达到精确性，但这种方法经常需要获取难以得到的元模型数据。

3）形式化转换方法：利用形式化语言在不丢失或者少丢失信息的前提下，把对象模型转换为具有一致性管理过程和强有力的工具支持的形式注释[80]。可以将UML相关图形转换成Z语言、B语言、XYZ/E、Petri网等不同的形式化语言，以提高UML的准确性，为精确建模提供良好的基础。由于前两种方法难度极大或要获得难以得到的元模型数据，因而进行研究的学者和机构比较少，取得的成果也非常少，现在研究最多的是第3种方法。