什么是软件体系结构形式化方法？

1、面向模型的方法。在面向模型的方法中，对目标软件系统的说明是为其构造一个模型，该模型的构成成分是一些具有特性的数据抽象，如域、元组、集合、序列、包、映射等。

2、面向性质的方法。这种方法通过直接给出目标软件系统的一组特性来描述目标软件系统，通常是一组目标软件系统必须满足的形式公理。在面向性质的方法中，其形式规格说明仅描述目标软件系统的性质，而不涉及实现方法。

根据表达能力，形式化方法大致可分为五类名词解释：

1、基于模型的方法。给出系统状态和状态变换与操作的显式但亦是抽象的定义，但对于并发没有显式的表示，如基于模型的形式规约语言Z和VDM。

2、代数方法。通过联系不同操作间的行为关系而给出操作的隐式定义，而不定义状态，同样它亦未给出并发的显式的表示，如基于性质的代数规约语言OBJ， LARCH， CLEAR。

3、过程代数方法。给出并发过程的一个显式模型，并通过过程间允许的可观察的通讯上的限制来表示行为，如CSP， CCP。

4、基于逻辑的方法。有很多方法采用逻辑来描述系统的特性，包括程序允许的低级规范和系统时间行为的规范，如时态逻辑。

5、基于网络的方法。根据网络中数据流显式地给出系统的并发模型，包括数据在网中从一个结点流向另一个结点的条件。如Petri网、谓词变换网。

形式化方法的研究和应用己有30多年的历史。最初的产生是由Dikstra和Hoare在程序难验证方面的工作中和Scott，Strachey以及其他学者在程序语义方面的工作基础上发展起来的。

在软件开发过程中，用户需求的规格说明非常重要，其使用者包括用户、系统分析员、设计与编程人员、测试人员和验收人员。规格说明对这些人员来说是一个可靠的参照点；系统分析员接受用户的需求，产生目标软件系统的规格说明；设计与编程人员根据规格说明，进行模块设计并产生最终程序代码；测试人员和验收人员验证最终程序代码是否满足规格说明。