软件开发中的形式化方法
郑红军张乃孝
（北京大学计算机科学技术系，北京 100871）
摘要本文基于研究的角度，首先讨论了在软件开发过程各阶段使用形式化方法的可能及困难，进而研究了形式化方法在理论上和应用上的能力、局限性及其产生原因，以及由此产生的对形式化方法的讨论。最后，综合上述讨论，从形式化方法的实质出发，在方法上，对形式化方法的研究提出了几点建议，以及基于这些建议所能看到的形式化方法研究可能的一些发展方向。
关键词形式化方法软件开发
1 形式化方法
随着软件系统复杂度的不断增长，开发正确、可靠的软件，成为一个急待解决的问题。解决此问题的一个有前途、有希望的技术是形式化方法的应用。形式化方法建立在严格的数学基础上，其目标是希望能使系统具有较高的可信度和正确性，并能使系统具有良好的结构，使其易维护，关键是能较好地满足用户需求。
“形式化方法”一词虽然一直被广泛地应用，但在不同程度上，因理解不同，使其具有了不同的含义。一般说来，形式化方法是指具有坚实数学基础的方法，它是数学上的综合、分析技术的应用，用于开发计算机控制的系统，经常有推理工具的支持，它可提供一个用于模型设计和分析的一个严格而有效的途径。从形式系统和复杂问题的本质来看，还未有一个适于全面描述和分析一个复杂系统的形式系统。所以，可以说，一个“形式化方法”并不是系统设计者开发系统时可能选择使用的方法，而只是设计者在此过程中希望利用的一种工具之一[Wood* 1988]。
总体上，形式化方法大致可分为五类[Barroca* 1992]：
（1）基于模型的方法—给出系统（程序）状态和状态变换操作的显式但亦是抽象的定义，但对于并发没有显式的表示，如：Z和VDM[Jones 1990]。（2）代数方法—通过联系不同操作间的行为关系而给出操作的隐式定义，而不定义状态，同样，它亦未给出并发的显式表示，如：OBJ、CLEAR。（3）过程代数方法—给出并发过程的一个显式模型，并通过过程间允许的可观察的通讯上的限制（约束）来表示行为，如：CSP、CCS。
（4）基于逻辑的方法—有很多方法采用逻辑来描述系统的特性，包括程序行为的低级规范和系统时间行为的规范，如：时态逻辑[Galton 1992]。
-------------------------------------------------------------------
*本文受到国家自然科学基金项目和863-306项目资助
（5）基于网络的方法—根据网络中的数据流显式地给出系统的并发模型，包
括数据在网中从一个结点流向另一个结点的条件。如：Petri网、谓词变
换网。
在形式化方法的使用中，这些方法之间的区别并不总是那么清楚的，有些是结合多种方法的多个方面而形成的混成（hybrid）方法，大多数方法都以集合论和谓词逻辑作为其根本基础，所以，这些方法在技术上都有一些相似性。不过，在表达能力上，这些方法之间有着一定的不同，这也是上述分类的主要依据。
形式化方法可以两种不同的方式来使用。首先，它们可用于生成规范，然后将此规范作为传统系统开发的基础；第二，形式规范以上述方式产生，然后将其作为验证程序正确性的依据。在第一种情况，数学将被作为生成规范的主要工具。形式化规范的好处在于：精确、抽象、简明和可操纵。操作可以包括规范的一致性检查、原型的自动生成或通过证明的方法推导出规范的一些特殊性质。在第二种情况，具有与第一种情况类似的益处，除此之外，还可以利用形式化方法证明规范及其相应程序的正确性，以表明程序与其规范的一致性，这样，可以使软件开发有可能具有与数学证明同样的确定性。
虽然形式化方法在研究和应用上都取得了很大的进展，也越来越成为研究者和软件开发者感兴趣的方法，但在理论上和方法上（哲学上）仍有其自身的局限性，而且有关使用形式化方法开发大型软件系统和解决特殊问题的适用性及其适用程度问题还不很清楚[Garhart 1990][Ehrig 1995]。本文基于研究的角度，首先讨论了在软件开发过程各阶段使用形式化方法的可能及困难，进而研究了形式化方法在理论上和应用上的能力、局限性及其产生原因，以及由此产生的对形式化方法的讨论。最后，综合上述讨论，从形式化方法的实质出发，在方法上，对形式化方法的研究提出了几点建议，以及基于这些建议所能看到的形式化方法研究可能的一些发展方向。希望本文能有益于形式化方法的研究和应用，也希望有助于认清形式化方法的能力、局限性及适用性，以使形式化方法能更有效地发挥其内在的潜力，从而能够使形式化方法成为解决软件开发问题的有效途径之一。
2 形式化方法在软件开发过程中的应用
2.1 软件生命周期
软件生命周期涉及从初始概念到软件产品，以及产品的使用和维护阶段的软件开发过程。为讨论方便，我们采用生命周期的一个一般模型，此模型将软件开发的生命周期分为五个阶段：
（1）需求规范—描述系统及其操作环境，特别强调系统与环境间的接口。（2）系统规范—描述系统输入、输出以及它们之间的关系。系统规范是待开发系统的外部特性描述，不涉及系统的内部结构。
（3）详细设计—描述用于实现此系统的算法及数据结构。
（4）实现—程序源代码，规范的一种可实现映象。
下面，我们将分别讨论在上述五个阶段使用形式化方法的可能及其困难。
2.2 需求分析
需求分析是软件开发过程的第一阶段，它将用户的需求从初始概念转换为需求文档，需求分析的结果应描述系统及其操作环境，而且还应能描述不可计算的系统，需求文档是与用户交流思想的主要基础。然而，极少有专门面向需求的形式化方法。在需求阶段使用形式化方法将会更加完善形式化方法已知的益处，如：非二义性、完全性、一致性等，这样，形式化方法中的符号系统将会变得更全面、更完整，它不仅能描述功能性的需求，而且亦能描述非功能性的需求。但是，形式化方法中的符号系统还未将表达能力和直觉结合起来。使得符号系统对用户是可表达的（可接受的），同时又不失去形式化方法所特有的精确性，形式化方法距此还有很大的差距[Jackson 1994]。
2.3 系统规范
系统规范仍是属于需求范围。这一阶段主要描述系统而不涉及环境，它给出系统接口的精确定义，主要涉及系统应做什么(WHAT)，而不是如何做(HOW)的问题。这对于使用代数规范技术非常有利，它采用输入、输出间的关系来描述系统的行为。在此阶段，可以应用两种可能的形式技术：一个是发展代数技术以使其可应用于大型系统的规范（尚未见到代数规范应用于大型系统中的实例），这就要求此技术能将规范模块化[Ehrig 1991]；另一个是可能在技术上找到一条可以减少设计自由度的途径。
2.4 体系结构设计
体系结构设计阶段描述系统的接口、功能、结构的初步实现。体系结构这一概念更接近于面向模型的规范和过程代数。但面向模型的规范缺乏结构性。在此阶段应用形式化方法的主要问题是，没有能够完成需求阶段所有工作的方法或符号系统。目前，形式化方法的使用者必须选择适合其应用领域特点的方法，或使用一种折衷的方法，从不同的形式化方法中找到一个合适的方法来完成此阶段的工作。
2.5 详细设计
详细设计是由体系结构规范出发的精化过程。许多形式化方法都支持“精化”这一概念。精化可以使我们定义和验证同一系统的两个描述之间关系的正确性、一致性。详细设计中的保持结构观点与目前的精化技术是一致的，传统的精化技术主要应用于顺序系统，也有一些技术支持并发系统，如：CCS。就我们所知，目前尚未有可以同时支持并发和顺序方式的令人满意的形式化精化机制[Morris 1989]。从实用角度讲，为使形式化方法能够应用于详细设计和精化过程，有必要采用一种折衷的方法，基于一种特殊的基础，研究如何将各种形式的(Formal and Informal)规范联系起来。
2.6 实现
在此阶段，已有大量的关于形式处理的工作[Boiten* 1992][Dromey 1989]，即：
将一程序与其的规范形式地对应起来。这一技术即是所谓的构造方法，构造方法基于从低级规范推导出程序这一想法，将程序构造与验证统一起来，验证环境是基于与构造技术类似的数学基础，但它主要关心程序和规范之间的自动/辅助正确性证明[Muk 1995]。形式实现技术在顺序程序上应用较广，目前也有对并发程序方面的研究。这一技术的使用代价很高，所以主要用于高精确系统的开发，因为高精确系统中的一个很小的错误可能会引起极大的灾难。若要使形式实现技术能广泛地应用，还须对其做较大的改进，以提高其效率，降低其使用代价。
3 形式化方法的能力及其局限性
3.1 形式化方法的能力
我们首先从理论上讨论形式化方法的能力。规范是用于软件开发者与用户相互交流的主要媒体，它就象一种混合方言，虽然形式化方法使用者具有不同的背景，但他们都将也应该以同一种方式来解释它，这正是用于交流之语言所必备的条件。所以，一个交流媒体应该是清晰的，并且是无二义性的。规范的清晰和无二义性并不等于说它是精确、抽象或简明的，但规范的这五个性质是相互关联的。下面我们讨论一下这五个方面的关系，从中可以看出形式化方法的能力。
二义性问题，相对来讲还是比较容易处理的。形式符号系统具有一定的数学性质，所以它们非二义性的基础在于其内在的数学结构。越是复杂的数学概念，越是建立在更原始的概念之上，如：集合、命题逻辑。这就是说，形式符号系统可以具有合适的解释，并在理论上足以确保规范的一致性解释。
形式规范是由一些精确的定义组成的，因为其符号系统的含义是明确定义的。若将英语作为交流媒体，将很难得到精确的规范，对于其他符号系统，如：结构化方法所使用的符号系统，虽然也是精确的，但其只对结构性具有较强的表达能力，而对功能性则表达能力较弱。所以，使用形式化方法，能够得到比其他规范方法更精确的规范。精确规范的直接益处在于：它能减少规范中的二义性和误解释的可能性（危险）。精确是形式化方法或形式符号系统的一个特征，是产生无二义性规范的主要依据。另外，形式规范主要的语用益处在于：可以对形式规范进行较详细的构造性检查，因为对此规范中的具体内容的含义不会有争议，有争议的只是内容的完备性。换句话说，精确有助于确认和交流。
由于适当的形式机制的使用，使得规范的抽象性成为可能。抽象是人们处理复杂性的主要智力工具之一，而且通过忽视不感兴趣的部分，从而有助于清晰性。各种形式符号系统对于精确、抽象地表达概念具有各自不同的能力，但它们均可用于严密地描述概念，更重要的是，它们比自然语言的描述更严密、更精确、更抽象。规范的抽象、精确及简明性都有助于使规范更清晰，当然，良好的结构也有助于清晰性。在理论上，至于为什么形式化方法不能产生良好的结构还不清楚，但这似乎并不是形式化所固有的。
一般地，形式系统（框架）使得表示一个规范与其相应程序之间的映射成为
可能。前面曾提到形式规范的一个很有价值的特性：可操纵性。这就是说，可以在明确定义的规则的指导下，分析规范或或对形式规范进行变换。利用形式规范的可操纵性可以证明规范的一致性；可以推导出关于此规范的一些重要结果；还可以验证规范的实现过程，至少可以验证源代码相对于其规范的正确性。更一般地说，有可能将不同级别规范间的验证以及规范与程序间的验证问题简化为形式证明问题。这样，形式化方法就可以提供程序对应其规范的非常高的可信度。所以，可操纵性也有助于确认，并且由这种特性可以得到进一步的抽象（推导出的性质），同样，也有助于使得规范更清晰。
形式化方法在理论上的这些能力，使得它在应用上也具有一定的实力。现在从形式化方法应用的角度，简要地讨论一下形式化方法的上述能力在其应用中的表现。总的说来，在某种程度上，形式化方法的上述能力在其应用中均有体现。
一般来说，比较、分析各种不同软件开发方法的有效性是很困难的。形式化方法作为一种交流的形式，也许是最有效的形式。因为它很容易在规范上取得一致，也易于形成文档。虽然非二义性、清晰性等特性并不是形式化方法的全部实质，但它的确为用户与设计者提供了一个有效的交流方式，这一点可以从形式化方法应用于实际的软件开发中可以看出来。形式化方法在实际软件开发中的使用并不是非常广泛，但在其应用范围内，其效果还是可喜的。IBM的Hursley曾经发表通过在CICS中使用Z，使其开发费用降低了9%，同时在错误率上也有很大的、可观的改进，虽然所开发软件的形式规范部分只占一小部分[Craigen* 1995]。由此可以看出，形式化方法的使用对于改进软件的质量是非常重要的。不过，对于形式化方法在实际工业项目的应用，相对的就比较少了，形式化方法在安全系统软件上的应用实例更少。然而，值得庆幸的是，虽然形式化方法在实际应用中有一定的局限性，但上面讨论的形式化方法的能力在实际系统中都有具体的体现。虽然如此，形式化方法仍有其局限性，在理论上，最大的局限性大概要与二义性问题有关。在实际应用中，最大的问题与可操纵性有关，大部分是因为有效工具的缺乏所造成的。下面，我们将详细讨论这两个问题。
3.2 形式化方法的局限性
事实上，现有的形式化方法并不能完全与上面所述的理想情况一致，在很大程度上与目前方法及其支持工具的研究及开发状态有关，当然也有其他因素的影响。当前的形式化方法有许多弱点和局限性，毫无疑问，这在形式化方法的实际应用中也都有具体的表现[Craigen* 1995]。
形式化方法之最基本的弱点或局限性与规范确认问题有关。我们可根据“数学的必然性”由规范开始开发软件，但将总是怀疑初始规范的真实性（精确性）。显然，如果能够消除这种疑虑是极其有价值的，但证据表明，软件错误的主要来源正是规范。这就意味着，规范所使用的数学工具并不能足以保证规范的“安全”性。更宏观地讲，我们面临着一个权衡问题，就是要在投入形式开发的力量与投入研究验证高阶规范[Jing 1995]方法中的力量之间权衡。需要注意的是，可以使
用证明技术来辅助确认过程，如：通过由一个规范推导出其安全特性，但这只能简单地缩短形式化与现实世界之间的距离，而并不能消除它。所以，我们不能简单地依赖于形式化机制以取得证明规范的安全性。
第二个主要的局限性与规范的解释有关。对于形式规范，在其数学基础意义下，并不是只有一种解释。软件工程师可以根据计算模型解释；系统用户可以根据系统操作环境中的系统使用模型来解释。这样，二义性问题已不是形式规范在其内部逻辑中存在唯一模型的问题，而是不同领域、不同背景和知识下的各种解释的相容性问题。形式规范的确是比其他相对松散的规范二义性问题要少，但这并不能说明在其多种解释下不可能存在二义性问题，这就削弱了形式化方法的能力，但我们并不能因此而否定它。
形式化方法的一个基本问题是，所谓的非功能性需求和性质的规范在目前的形式化方法中很难规范清楚。为了能将形式规范与现实世界联系起来，也为了对规范的解释给以指导，可以对规范中的基本实体和其他基本概念给出较松散的描述。在处理规范时，大部分仍以形式化方法处理，在特殊情况下（非功能性描述）可以采用非形式化方法处理。这样，对于二义性和精确问题，形式化方法的真正局限性在于形式化方法只能减少对规范误解释和错误的机会，而不能消除它们。这就要求形式化方法的使用者应正确地看待形式规范，应认识到，形式规范的目的是增加其可信度，减少软件开发中的错误，但形式规范并不能完全保证其可信及无错误。形式规范的可信度在于对软件产品及其开发过程的理解，如果形式证明具有与形式规范同样高的效率，那么，以形式化方法开发出的产品的复杂度将是可观的。易言之，证明本身是非常复杂的并且亦难以理解。这就导致一个问题：形式证明的使用是能够提高还是降低对一个软件系统的理解度和可信度呢？这个问题是相当难回答的，因为在回答过程中，很难不受到当前程序验证工具的能力问题的影响。对于一个规范或程序，至少其停机问题是不可判定的，因此也就无法形式地证明其是否停机。虽然象这类不可判定问题在实际中并不常见，但形式化方法使用者必须认识到，在形式系统中，有一些问题即使是简单的，也是无法证明的。认识到这一点，对形式化方法的应用相当重要。
形式化方法中，形式规范起着一定的关键作用，但规范的使用者不易接受规范的形式化和规范中极难理解的名词、概念。象Z和CCS符号系统中所体现出的数学抽象，使得规范能够简洁和精确，但这类符号系统却对规范的清晰性没有多大好处。有许多人认为，清晰性和精确性是有其对立性的，其主要原因是，在实际应用中，我们过分地依赖于规范的非形式解释，而不是根据其内在逻辑来解释它们，以更好地理解规范之含义。一个与之相关的问题是，形式规范技术往往会有许多基本的数学背景，而这些背景又往往与实际问题没有直接关系。事实上，形式规范并不是真正的精确，因为关于形式化方法的符号系统和语义并未能定义的令人满意，就是Z也有很多版本，虽然现在在IFIP的努力下，得到一个Z的标准。当前的形式方法的研究与发展并不象理想情况那样好，尤其在协调形式化方法的表达能力、灵活性与定义的精确性之间的关系上有一定的困难。
另外一个主要问题是我们对工具及其应用应相信到什么程度。关键问题是对于复杂工具应相信到什么程度，尤其是那些比实际问题还复杂得多的工具。事实上，我们使用的编译器和定理证明器都要比实际应用程序复杂得多。因此，有必要对工具进行测试或证明，但这又产生了一个递归问题：对用于验证验证工具得的工具，我们应相信到什么程度呢？所以，形式化方法及其支持工具只是减少了开发的风险，如：通过规范的一致性检查，但它并未消除所有的风险，而且还可能引入了风险，尤其是在依赖和使用工具这一问题上。
最后，关于形式化方法的教育和训练问题亦是形式化方法中的主要问题。当然，如果软件开发者愿意接受教育和训练，那么，这一问题是易解决的，但情况并非象想象的那么理想。
4 关于形式化方法的讨论
正是由上面讨论的形式化方法的局限性，形式化方法的反对者对形式化方法提出了一些质疑。虽然有些意见是片面的，例如，在形式化方法的表达能力与支持工具的能力方面的质疑，但这些反对意见无疑是有益于形式化方法的研究与广泛的应用的。值得一提的是，上面提到的关于形式化方法的理论问题也影响着实际系统的开发，尽管早在1976年Gerhart和Yelowitz提出了形式验证程序的失败之处，但其问题的原因在于其证明过程的不适当，而不是证明本身有问题。许多反对者认为形式化方法及技术在本质上就是错误的，它不适于软件开发过程。另外一个问题是，我们认识到的形式化方法的局限性对其应用有多大的影响？我们认为，形式化方法的局限性并不影响形式规范本身作为交流和文档工具的价值，而验证、精化问题是一个实质性的问题[Clement 1992]，我们需要用其他方法来丰富精化的证明，并不是形式化方法本身有什么错误。现在并没有一个充分的精化技术完全支持形式化方法，这一点仍是一个很难的研究课题。
形式化方法是有争议的，其支持者认为形式化方法是对软件开发的一场革命，而其反对者则认为形式化方法不可能有多大的发展。因为大多数人对形式化方法并不是很熟悉，所以就很难断定哪一方是正确的，于是就造成了对形式化方法的一些误解和误用。[Hall 1990]以其研究和应用形式化方法的事实分析了当时对形式化方法认识的七个误区：
（1）形式化方法能够保证软件是完全正确的。事实是，形式化方法也是能够出错的。
（2）形式化方法的全部即是程序证明。事实是，形式化方法的全部是规范。（3）形式化方法只适用于safety-critical系统。事实是，形式规范有助于任何系统。
（4）形式化方法要求具有很高的数学基础。事实是，规范所需的数学是简单、容易的。
（5）形式化方法增加了开发的费用。事实是，从长远的观点来看，形式规范可以降低开发的费用。
（6）形式化方法对用户来说是不可接受的。事实是，形式规范可以帮助用户理解软件系统。
（7）形式化方法未能应用于真正的大型软件的开发中。事实是，形式化方法每天都应用于工业项目中。
最后Hall提出，虽然形式化方法不是“万灵药”，但它是一个有力的工具。Hall还针对上述七个误区，给出了形式化方法对的七点认识。
随着形式化方法的不断研究和发展，对形式化方法亦有了更新的认识，同时也在软件开发界产生了对形式化方法认识的新的误区。[Bowen* 1995]根据其使用形式化方法的切身经验及对形式化方法更深入的研究，又给出了另外七个误区，并以事实解释了误区的形成原因，及误区的错误所在。这七个误区分别是：（8）形式化方法延误开发过程。
（9）形式化方法缺乏工具。
（10）形式化方法代替了传统的工程设计方法。
（11）形式化方法只能应用于软件。
（12）形式化方法是不必要的。
（13）形式化方法并没有被支持。
（14）形式化方法的使用者总是使用形式化方法。
其结论与[Hall 1990]基本相同，即形式化方法并不是“万灵药”，而只是一种用于改进系统可靠性的方法之一。
对于形式化方法批评最激进的是对形式化方法几乎持完全否定态度的[Glass 1995a]。他对形式化方法以讽刺的口吻提出了四点质疑。我们认为，无论是误区还是讽刺的质疑，无疑是对形式化方法研究和应用的一个促进，并不能因此而“因噎废食”。由这些误区和质疑，也不难看出对形式化方法的一些“幼稚”的认识，以及由此而造成的许多误解。事实上，每一种方法都有其自身的理论背景和应用条件。同样，使用形式化方法亦要清楚其理论背景和应用条件，若将形式化方法应用于文学创作，这显然是不合时宜的。形式化方法的使用应限制在可形式化的范围之内。然而，现实世界中，并不是所有的实体都能够形式化的，这就提出了人工智能中的基本问题：常识（common sense）的表示问题，这一问题也是阻碍人工智能发展的重要因素之一。若能将常识形式化，那么，形式化方法的应用范围将能大大地扩大。在反对形式化方法的意见中，有很多是将形式化方法应用于不适用的情况而得到的结论，这也是对形式化方法认识之误区和质疑的主要来源。当然，也必须承认，形式化方法的确有其自身的局限性（如在第3节中所述），这也是任何一种方法所不可避免的。现在并没有足够的信息和证据用以客观地评价形式化方法和其他方法对软件和系统开发过程的贡献。
无论对形式化方法如何争论，我们有理由相信，形式化本身并没有错。形式化方法在技术上已显示出了可观的实力，同时我们也看到，它也限制了软件开发的范围，有些可用其他方法实现的问题，用形式化方法却无法实现或很难实现。这就要求我们能够“超越”形式化方法，深入认识软件开发过程，对软件开发中
的非精确、非形式化领域予以同样的重视，以科学的研究方法来研究形式化方法[Glass 1995b]。
5 关于形式化方法的几点建议及发展方向
基于上面对形式化方法的分析和讨论，我们提出对形式化方法的几点可能的改进，从而也就确定了形式化方法的一些发展方向。
（1）可重用的规范库及更易接受的符号系统将更有助于形式化方法的研究与应用。如：形式化方法与结构化方法符号系统的结合，即可将形式化方法
的严密性与结构化方法的结构性结合起来，使得规范更易理解，更易于
交流。在这方面，目前也有一些研究成果；对可重用规范的研究目前较
少[Cazin 1991]。当然，这一改进工作并不是短期内可以完成的。
（2）改进形式规范的语法、语义定义的质量，从而可以使得形式化方法更加“稳定”。象VDM和Z这样的形式化方法，就有许多版本。因此造成了形
式化方法的不稳定状况。目前已着手开始对VDM和Z进行标准化工作
了[Blyth* 1990]。
（3）加强规范语言中对并发控制和容错处理的表达能力，同时也要使精化技术能够处理这类并发机制和容错。这方面的改进也是长期的研究课题。（4）对于支持形式化方法的工具的可信度问题，一直是困扰形式化方法发展的重要因素之一，如何度量与提高支持工具的质量亦是一个长期的研究问
题。
（5） Bell实验室的P.T.Devanbu在第十六届软件工程国际会议中（1994）指出：目前大多数软件系统的容量和复杂度日益增大，需要对软件开发过程中
的各个阶段增强基于知识的描述和维护。基于知识的软件工程（KBSE）
研究范式正是形式化的知识表示和推理机制，支持多种软件开发过程。
随着KBSE的发展，该方式需要在基于知识的系统构造、维护、运行和
理解方面增强描述能力和推理能力，而描述逻辑可在终止性、形式化语
义和高效的推理过程诸方面提供有效的支持。
在此，我们只给出对形式化方法研究的一部分研究方向，而未能给出关于这些研究方向的研究方法。从总体来说，若要在以上各方面得以改进，完全依赖于形式化方法研究的前人结果是不现实的，必须开辟一条新的研究道路，尽力摆脱前人结果的束缚，这样才有可能超越形式化方法，使得形式化方法得到充分的利用。
另外，值得重视的是，形式化方法的研究与发展，也依赖于其他相关学科的发展，如：代数学、范畴论、逻辑、认识论、认知科学、人工智能等[Holloway 1995]。数学作为计算机科学发展的基础，同样对形式化方法的发展也起着至关重要的作用[Hoare 1993]。认识论、认知科学、人工智能等学科的研究能够促进对软件开发过程、智能型软件的形式开发，及知识表示等方面均有一定的重要影响。正如[Hartmanis 1994]中提到的，真正的计算机科学家应是一个全面的人才，而不应局限于其特定的领域，应有较强的理解力。同样，研究形式化方法也应考虑其相关学科的发展及其影响。
6 结论
本文以研究的态度，讨论了形式化方法的能力、局限性以及关于形式化方法的争论，从中可以窥见当前形式化方法的研究现状以及今后的一些发展方向，希望本文的讨论能够有助于正确认识形式化方法，以能提高形式化方法的效率。这也是本文主要目的。
形式化方法的研究涉及许多方面，本文不可能将这些方面全部阐述清楚，有许多文献已对形式化方法的其他方面进行了讨论，如：[Bowen* 1995]对形式化方法的使用提出了切实可行的十点建议，并指出若依此十点建议来使用形式化方法，将会体会到形式化方法的巨大益处。[Craigen* 1995]对形式化方法在大型软件开发中的应用作了一个客观的论述，其中有形式化方法应用于各种领域的十五个应用实例，对每个实例详细地叙述了项目的开发者、开发目的、开发内容、形式化方法在开发中的使用、项目产品的使用、开发中所使用的工具等。[Liu* 1995]对形式化方法在特殊领域中的应用方法及效果做了阐述。另外，本文也未对形式规范语言和具体的形式化方法及技术，如：VDM、Z、B等进行讨论，这些在[Craigen* 1995]中均有详细讨论。
对形式化方法近三十年来的研究和应用，已取得了一定的成果，但也应清醒地看到形式化方法在研究和应用中的困难和局限性，更重要的是，应注意对形式化方法研究的研究方法。对形式化方法的研究，我们认为，首先应认识到方法本身并不能解救我们[Loy 1993]，但它可以帮助我们。也就是说，要认清方法在软件开发中的地位，认识到新的方法和工具可以帮助我们，但它并不能解决根本问题。在这一认识的基础上，对软件开发过程的深入及实质性理解，对形式化方法的研究也具有很大的影响，试图通过形式化软件开发过程来研究形式化方法，我们认为是不可取的，因为软件开发过程本身是人的一种具有创造性的智力行为，在此过程中有智能的因素在起作用，如：人的直觉、常识等因素[Naur 1985]。另外，在研究模式上也应加以改进，目前的研究模式基本都是研究—推广式。这种模式实际上不符合人的认识过程，人类的认识过程是实践—认识—再实践的反复过程。因此，理想的、正确的研究模式应该是由真正的软件开发者在实际开发中提出问题，提出对形式化方法的要求，然后由研究者研究解决这些问题的可能性及方法，再将其应用于实际的软件开发过程中。这样，对形式化方法的研究就应有强大的经济支持及应用背景，以能使形式化方法充分发挥其应有的作用。当然，目前国内的研究状况很难达到上述要求，甚至在发达国家中也是不多见的。因此，一种可行的办法是，研究与开发并轨同行。研究者可以暂时不考虑其研究内容在今后是否有什么应用前景，就象纯数学的研究那样，同时开发者亦应不断地提出问题，以此来刺激研究者不断地纠正方向，使其研究渐渐地靠近应用，随着科学及其应用的不断发展，研究与应用必然会走到一起而合二为一。这时，将是科学的又一大进步，这也是科学发展的一种较现实的途径，对于形式化方法的研究也不例外。
最后，讨论一下关于形式化方法的使用和适用性问题。对于这一问题的争论，实际上来源于：到目前为止，还没有足够的证据及实例能够充分证明形式化方法可以在大型软件开发中发挥其效益[Floyd 1985]。当然，必须承认，形式化方法的研究者们的确在某些方面夸大了形式化方法的能力，形式化方法在理论上的能力是很可观的，也是清楚的，但对于其局限性，就有些难以将其阐述清楚。所以，最好是刺激形式化方法的使用以充分显示其价值，从而有可能越过其局限性。虽
然在某些方面夸大了形式化方法的能力，但在一定的领域内，开发者仍有使用形式化方法的强烈要求。当然，这一论断是对形式化方法之复杂现状的一种简单化。无论是研究还是使用形式化方法，都应认识到，软件工程是一种人类行为，所以，形式化方法不可能保证软件产品的正确性。如果能够愿意从失败中吸取教训，愿
意利用现有的最好的技术来检查我们的工作，通过适当的测试和工具，那么，我
们将能成功地使用形式化方法来开发高质量、高可信度的系统。总之，形式化方法的研究和使用，具有光明的前途，但也有其不可避免的曲折，任何一门学科的研究、发展都是如此。
主要参考文献
[Barroca* 1992] L.M.Barroca et al., Formal Methods: Use and Relevance for the Development of Safety-Critical Systems. The Computer Journal,
Vol. 35, No. 6
[Blyth* 1990] D.Blyth et al., The Case for Formal Methods in Standards. IEEE Software, September
[Boiten* 1992] E.A.Boiten et al., How to Produce Correct Software — An Introduction to Formal Specification and Program Development by
Transformation. The Computer Journal, Vol. 35, No. 6
[Bowen* 1995a] J.P.Bowen et al., Ten Commandments of Formal Methods. IEEE Computer, April
[Bowen* 1995b] J.P.Bowen et al., Seven More Myths of Formal Methods. IEEE Softwre, July
[Cazin 1991] J.Cazin, Construction and Reuse of Formal Program Development.
LNCS 494, TAPSOFT’91
[Clement 1992] T.Clement, The Role of Data Reification in Program Refinement. The Computer Journal, Vol. 35, No. 5
[Craigen* 1995] D.Craigen et al., Formal Methods Reality Check: Industrial Usage.
IEEE Trans. Soft. Engi., Vol. 21, No. 2
[Dromey 1989] G.Dromey, Program Derivation
[Ehrig 1991] H.Ehrig, On the Relationship Between Algebraic Module Specifications and Program Modules. LNCS 494, TAPSOFT’91 [Ehrig 1995] H.Ehrig, Theory and Practice of Software Development. EATCS, No.
57
[Floyd 1985] C.Floyd, On the Relevance of Formal methods to Software Development. LNCS 186, TAPSOFT’85
[Galton 1992] A.Galton, Logic as a Formal Method. The Computer Journal, Vol.
35, No. 5
[Gerhart 1990] S.L.Gerhart, Applications of Formal Methods: Developing Virtuoso Software. IEEE Software, September
[Glass 1995a] R.L.Glass, A Theory About Software’s Practice. J. Systems Software, Vol. 28
[Glass 1995b] R.L.Glass, Beyond Formal Method. J. Systems Software, Vol. 29 [Hall 1990] J.A.Hall, Seven Myths of Formal Methods. IEEE Software, September
[Hartmanis 1994] J.Hartmanis, On the Nature of Computer Science. CACM, Oct. [Hoare 1993] C.A.R.Hoare, Algebra and Models. Sof. Eng. Notes, Vol. 18, No. 1 [Holloway 1995] C.M.Holloway, Software Engineering and Epistemology. Soft. Engi.
Notes, Vol. 20, No. 2
[Jackson 1994] M.Jackson, Problems, Methods, and Specifications. Soft. Engi.
Journal, Nov.
[Jing 1995] Y.Jing, A Methodology for High-level Software Specification Construction. Soft. Engi. Notes, Vol. 29, No. 2
[Jones 1990] C.B.Jones, Systematic Software Development Using VDM.
[Liu* 1995] S.Y.Liu et al., The Practice of Formal Methods in Safety-Critical Systems. J. Systems Software, Vol. 28
[Loy 1993] P.Loy, The Method Won’t Save You. Soft. Engi. Notes, Vol. 18, No. 1
[Morris 1989] J.M.Morris, Laws of Data Refinement. Act Informatica, Vol.26 [Muk 1995] P.Mukherjee, Computer-aided Validation of Formal Specifications.
Soft. Engi. Journal, July
[Naur 1985] P.Naur, Intuition in Software Development. LNCS 186, TAPSOFT’85
[Wood* 1988] J.Woodcock et al., Software Engineering Mathematics. Pitman Publishing
Formal Methods in Software Development
Zheng Hongjun Zhang Naixiao
Department of Computer Science & Technology
Peking University, Beijing 100871
Abstract With a view to study on formal methods, this paper discusses a few possibilities and difficulties for applying formal methods to every stages during the process of software development. Then, the paper studies about capabilities, limitations and their causes of formal methods from the point of their theories and applications, also studies about some debates on formal methods. Lastly, based on the discussion above, the paper proposes, from the essences of formal methods, several suggestions and some possible directions, in terms of those suggestions, of the research on formal methods.
Keywords Formal methods Software development
对软件开发的理解和认识 专业：计算机科学与技术学号：2004110023 姓名：王贤才软件开发是一个把用户需要转化为软件需求，把软件需求转化为软件设计，用软件代码来实现软件设计，对软件代码进行测试，并签署确认它可以投入运行使用的过程。在这个过程中的每一阶段，都包含有相应的文档编制工作。 软件开发过程当中，遵循一定的流程，主要包括系统分析、系统设计、系统编码、系统测试以及系统的维护等几个阶段。依次概述如下： 1.系统分析 系统分析包括软件需求分析和系统可行性分析。软件需求分析就是回答做什么的问题。它是一个对用户的需求进行去粗取精、去伪存真、正确理解，然后把它用软件工程开发语言（形式功能规约，即需求规格说明书）表达出来的过程。系统可行性分析就是通过需求调查来确定此系统是否具有可行性。 2.系统设计 系统设计可以分为概要设计和详细设计两个阶段。实际上软件设计的主要任务就是将软件分解成模块。概要设计就是结构设计，其主要目标就是给出软件的模块结构，用软件结构图表示。详细设计的首要任务就是设计模块的程序流程、算法和数据结构，次要任务就是设计数据库，常用方法还是结构化程序设计方法。 3.系统编码 系统编码是指把软件设计转换成计算机可以接受的程序，即写成以某一程序设计语言表示的"源程序清单"。 4.系统测试 系统测试的目的不是验证软件的正确性，而是以较小的代价发现尽可能多的错误。测试从需求阶段开始，此后与整个开发过程并行，换句话说，伴随着开发过程的每一个阶段，都有一个重要的测试活动，它是预期内按时交付高质量的软件的保证。 5.系统维护 系统维护是指在已完成对软件的研制（分析、设计、编码和测试）工作并交付使用以后，对软件产品所进行的一些软件工程的活动。即根据软件运行的情况，对软件进行适当修改，以适应新的要求，以及纠正运行中发现的错误。编写软件问题报告、软件修改报告。在实际开发过程中，软件开发并不是从第一步进行到最后一步，而是在任何阶段，在进入下一阶段前一般都有一步或几步的回溯。在测试过程中的问题可能要求修改设计，用户可能会提出一些需要来修改需求说明书等。 我认为，软件开发是一个环环相扣的设计和实施过程，整个系统开发的过程当中，系统分析和设计是重中之重。只有把握好系统分析，才能使后续改动尽可能多的减少；只有把握好系统设计，才能保证软件的根基比较稳固。也即是它们很大程度上决定着软件开发的周期以及寿命。另外，完美的开发团队和开发过程的合理控制是软件成功开发关键要素之一。
快视信息软件开发流程规范： 用户需求：软件项目首先由客户经理(CM，Custom Management)接洽客户的较大的需求。这时的需求叫市场需求（或叫用户需求），客户经理会进行各个项目的安排，即对项目的启动时间和发布时间进行规划和设置。 项目经理(PM，Project Management)对客户经理负责。项目经理的需求是根据客户经理给的，项目经理不和用户（客户）直接接触（通过客户经理接触），负责和用户进行需求洽谈和沟通的是客户经理。一个项目的需求在一般情况下是不准变更的，如果有需求理解方面的不清楚可以进行沟通，但是需求是不变更的。如果用户有新的需求，一般规划在下一个版本中。因为需求变更了，这个目的时间就要进行调整，就不能按计划进行和完成。客户经理提交给项目经理的是需求规格说明书。 一、项目开工会 在项目经理领到客户经理分配给的需求后，做项目计划，具体做项目人员的确定、需求的分解（需求分解到每个人）、代码量的估计，项目各个阶段时间的划分和工作量的计划、质量指标的设定。这时项目经理需要输出的文档是项目需求分解任务书、项目计划PPT、及做好整个项目需要填写的一系列表格。然后组织项目组成员和客户经理CM、QA(质量审计经理)进行项目开工会。这时这个项目就算真正启动，计算工作量时，即计算这个项目总共花了多少个工时，工时是项目经理做计划的时间也算在内，再加上项目开工会和后续各个阶段总共花的总工时数，还有各个阶段开会所花的时间。在项目开工会上，各个成员就明确了这个项目是属于增强型项目，还是其他项目的项目性质，增强型项目的意思是说在原来上一版本的基础上又根据新的需求进行增强型开发。还有要明确项目最后开发出的新增代码量有多少，最后要明确每个人的需求任务，接下来着手进行SRS的写作。 二、SRS阶段：System/Software Requirment Specification 软件需求规格说明 在项目开工会后，项目组就开始按照在项目开工会上项目经理的需求任务分解的任务开始进行SRS的写作。 一般项目经理给你的一个子需求任务，你这时需要分解为更小的需求。一般一个需求的写作是按这样进行的。先简单介绍这个需求，然后把这个需求设计成黑盒的形式，即输入，处理过程、输出。这些都需要写详细，任何一个需求都写成这种形式，输入是什么，处理过程是什么，输出结果是什么。处理过程需要用Visio或者PPT画出处理流程图，流程图要很详细。每一步的各种情况都要表示和考虑到。对异常情况也要考虑和进行处理。还有要说明在原来的基础上怎么改动，具体方法要进行说明。设计的数据库表结构，要给出脚本，SQL语句，表结构需说明每个字段，哪些是主键，你在这个需求处理过程中哪里使用了哪些表，需要进行哪些操作，都需要说明。这里需要设计和编制《数据库设计说明书》文档。该文档中描述该系统中设计出的所有的数据库表结构和各字段类型。还有多个操作对象要画序列图表示出按时序的处理过程。这个SRS文档就相当于我们平时毕业设计或者一个题目的详细设计阶段达到的水平，甚至比它更详细。每个项目组成员都把自己的需求的SRS文档写出来之后放到配置库中，然后每个人对项目组其他成员的（非自己的）SRS文档进行Review（评审）,对每个SRS文档在每页发现或者纠正的错误数不能低于一定的数目，而且要保留批注记录，经过Review的（保留批注的）文档要放到配置库的Review文件夹下，这是进行项目质量指标收集的重要依据，是QA 进行调阅和审计的资料。项目经理要对SRS文档、SRS Review文档进行汇总。在汇总后组织项目组全体成员进行SRS阶段会议，对每个人写的SRS进行评审会议（讨论和提意见），对别人给你提的修改意见你要一一进行说明，说明为什么不改，怎么改的，是什么问题，问题严重程度属于什么级别，而且都要填表，也是QA进行审计的内容。开完会后如果每个人完成的都差不多，然后安排半天或者一天的时间进行返工，主要是进行修改文档，按在会上讨论的结果和别人给你的Review 文档结果（评审结果）进行准一修改和完善。然后再进行SRS阶段开会，如果都做的比较到位和具体、符合要求，即关闭SRS阶段。这时SRS阶段的花费的工时数和一些质量活动指标就出来了，比如你这个SRS文档写了几页，每页的错误数是多少，返工修改用了多少时间，然后这些这个比率也会自动计算出来。进而可以判断这个阶段的质量。每个项目组成员在每天工作完毕后都要进行Time Sheet 的填写，必须具体到半个小时，这是统计和分析的需要。填写必须真实。 三、UTP、STP阶段（UTP、STP写作） UTP Unit Test Plan 单元测试计划 STP System Test Plan
（1）软件开发过程是什么？ 软件开发过程是按照软件工业化的标准定义的心之所向，所向披靡 ?在软件开发中必须具有的一系列过程规范； ?软件开发过程是定义在软件中的软件需求、软件设计、软件编码、软件测试、软件部署的实现目标和规范化的管理方法论； ?软件开发过程是保证软件工业化生产的法典；?软件开发过程做的是：定义标准和为了达到标准的路； ?软件开发过程要改善的是：软件开发的效率和质量； ?软件开发过程的实现最重要的是：人。 （2）大多数软件项目失败的原因： a)不完整、不现实的项目需求 b)对需求的变更束手无策 c)脆弱的架构 d)采用不成熟的技术 e)测试的不充分性 f)拙劣的进度计划和评估 g)缺乏资源 h)不具备项目管理方法 i)缺少管理层的支持 （3）软件工程的三个要素：方法、工具和过程（4）A software project failed if It is delivered late It is runs over the budget It does not satisfy the customer’s need It is of poor quality Classical software development methods have not solved software crisis.传统的软件开发方法没有能够解决软件危机。 （5）A software engineer’s job: a)Make a working plan.制定工作计划 b)Carry out it.(Do their work according to this plan)按照此计划工作 c)Try his/her best to produce high-quality products.尽最大努力生产 出高质量产品 (6)3 Key aspects a)Quality products 高质量产品 b)Expected costs c)On agreed schedule （7）Summary of PSP PSP is a framework designed to teach software engineers to do better work Estimate and plan →track →improve quality Quality methods take time to learn and practice,but it will help you in you engineering career Establish goals →measure quality → understand the process → change and reure process → measure & analyze the results → recycle improving Identify the tasks you do (8)敏捷软件开发宣言 个体和交互胜过过程和工具 可以做到工具的软件胜过面面俱到的文档 客户合作胜过合同谈判 响应变化胜过遵循计划 敏捷开发的原则： 1、我们最优先要做的是通过尽早的、持续的交付有价值的软件来使客户满意。 尽早交付具有部分功能的系统和质量系统之间具有很强的相关性 2、即使到了开发的后期，也欢迎改变需求。敏捷过程利用变化来为客户创造竞争优势。 关于态度的声明，敏捷过程的参与者不惧怕变化，努力保持软件结构的灵活性。 3、经常性地交付可以工作的软件，交付的间隔可以从几周到几个月，交付的时间越短越好。 关注的目标是交付满足客户需要的东西。它们是敏捷实践区别其他过程的特征所在。 4、在整个项目开发期间，业务人员和开发人员必须天天都在一起工作。 有意义的、频繁的交互，必须对软件项目进行持续不断地引导。 5、围绕被激励起来的个人来构建项目。给他们提供所需要的环境和支持，并且信任他们能够完成工作。 人被认为是项目取得成功的最重要的因素。 6、在团队内部，最具有效果并且富有效率的传递信息的方法就是面对面的交谈。首要的、默认的沟通方式。 7、工作的软件是首要的进度度量标准。 敏捷项目通过度量当前软件满足客户需求的数量来度量开发速度。 8、敏捷过程提倡可持续的开发速度。责任人、开发者和用户应该能够保持一个长期、恒定的开发速度。不是 50米短跑，而是马拉松。以快速但是可持续的速度行进。 9、不断关注优秀的技能和好的设计会增强敏捷能力。
学习中心 姓名学号 西安电子科技大学网络教育 2012学年上学期 《软件形式化方法》期末考试试题 （综合大作业） 考试说明： 1．大作业于2012年06月09日下发，2012年06月23日交回。 2．试题必须独立完成，如发现抄袭、雷同均按零分计。 3．试题须手写完成，卷面字迹工整，不能提交打印稿。 一填空题（每空2分，合计30分） 1. 现代软件工程的软件定义包括、和。 2. 软件危机是指在计算机软件的开发和维护过程中所遇到的一系列严重的问题，其产生的原因主要包括：、、、；其本质特征是软件的和。 3. 模式是Z语言规格中一个重要的元素，模式是由、和 组成。 4. 形式化方法研究如何把（具有清晰数学基础的）严格性（描述形式、技术和过程等）融入软件开发的各个阶段；包括形式化规格、和三种活动，在软件开发的形式化规格中包含的三种规格为、和。 二有限状态机（10分） 对于图中所示有限状态机的状态转移图，给出其关系矩阵和状态转移表。
三Petri网（10分） 对图中所示Petri网进行化简。 四进程代数（10分） （1）计算进程PHONE的迹 PHONE = ring → answer → hungup→ STOP （2）给出迹投影结果
对软件需求分析的认识 自从学习了软件工程这门课程之后，我对软件及其开发有了更加浓厚的兴趣，同时我也认识到软件工程在软件开发中的重要性。目前国内软件在开发中还没有对软件开发的过程进行明确规定，文档不完整，也不规范，软件项目的成功往往归功于软件开发组的一些杰出个人或小组的努力。这种依赖于个别人员上的成功并不能为全组织的软件生产率和质量的提高奠定有效的基础，只有通过建立全过程的改善，采用严格的软件工程方法和管理，并且坚持不懈地付诸实践，才能取得全组织的软件过程能力的不断提高，使软件开发更规范合理。 软件工程理论认为，在软件生命周期中，需求分析（Requirements Analysis）是最重要的一个阶段。软件需求分析的质量对软件开发的影响是深远的、全局性的，高质量需求对软件开发往往起到事半功倍的效果，所谓“磨刀不误砍柴功”。在后续阶段改正需求分析阶段产生的错误将付出高昂的代价。而对于软件需求分析，简单的来说就是要决定“做什么，不做什么，达到用户所期望的效果”，就好比我们自己平常做一件事之前，都会有做好计划，软件开发亦不例外。用软件工程的定义来讲，它就是深入描述软件的功能和性能，确定软件设计的限制和软件同其它系统元素的接口细节，定义软件的其它有效性需求。下面是一些有关需求分析的有关知识： 一、现在很多管理类文档将需求分为合理需求和不合理需求两种类型，这种分类方式本身并没有错误，但在实际判断起来却很难，主要是无法清晰的界定合理和不合理的属性，用户和研发人员的出发点是不一样的，每个研发人员也都有各自的认识，很难确定合理与不合理的标准。因此将需求按重要程度进行分级，是必不可少的步骤。需求分类好了，自然就可以在以重要需求为出发点，兼顾次要需求的基础上来进行设计。在开发者与用户（代表）交流时，切记避免使用如“大概”、“应该”、“可能”等词语，这是初入行者和懒于写文档的人都容易出现这种问题，但结果是，概括性的语言无限放大了大家对需求的理解，造成歧义。所以，需求越具体、详细就越好，磨刀不误砍柴功。 二、需求分析是分多阶段的，理想的流程是需求交流—〉分析整理—〉需求确认—〉变更控制（用户追加或补充的需求内容才能称为需求变更），实际情况下该流程会多次循环往复，在这个过程当中，变更控制显得异常重要，它既是原需求的终止，又是新需求的开始，做好变更控制，往往事半功倍。因此，需求变更贯穿了需求说明书经过论证之后的所有软件管理过程。同时需求变更需要有专门的人员记录，这个人最好是项目组内部的人员，记录内容包括需求变更具体内容、发生于哪个阶段、以及由谁提出的等内容。项目经理需要每天关注需求变更记录，每周必须对需求变更产生的影响进行预估，并将预估结果记入到需求变更记录当中，以便于确定今后的工作计划。还有 三、分析员占有的位置 分析员通过需求分析，逐步细化对软件的要求，描述软件要处理的数据域，并给软件开发提供一种可转化为数据设计、结构设计和过程设计的数据和功能表示。在软件完成后，制定的软件规格说明还要为评价软件质量提供依据。 四、任务 开发软件系统最为困难的部分就是准确说明开发什么。最为困难的概念性工作便是编写出详细技术需求，这包括所有面向用户、面向机器和其它软件系统的接口。同时这也是一旦做错，将最终会给系统带来极大损害的部分，并且以后再对它进行修改也极为困难。目前，国内产品的庞杂，一家企业可能有几个系统并立运行，它们之间接口是系统开发人员最头痛的问题。对于商业最终用户应用程序，企业信息系统和软件作为一个大系统的一部分的产品
软件开发过程详解 软件开发过程即软件设计思路和方法的一般过程，包括设计软件的功能和实现的算法和方法、软件的总体结构设计和模块设计、编程和调试、程序联调和测试以及编写、提交程序。 生产一个最终能满足需求且达到工程目标的软件产品所需要的步骤。软件开发过程覆盖了需求、设计、实现、确认以及维护等活动。需求活动包括问题分析和需求分析。问题分析获取需求定义，又称软件需求规约。需求分析生成功能规约。设计活动一般包括概要设计和详细设计。概要设计建立整个软件系统结构，包括子系统、模块以及相关层次的说明、每一模块的接口定义。详细设计产生程序员可用的模块说明，包括每一模块中数据结构说明及加工描述。实现活动把设计结果转换为可执行的程序代码。确认活动贯穿于整个开发过程，实现完成后的确认，保证最终产品满足用户的要求。维护活动包括使用过程中的扩充、修改与完善。 1.需求分析 1.1 需求分析的特点和任务 需求分析是软件开发的第一步。获取需求的一个必不可少的结果是对项目中描述的客户需求的普遍理解。一旦理解了需求，分析者、开发者和客户就能探索出描述这些需求的多种解决方案。参与需求获取者只有在他们理解了问题之后才能开始设计系统，否则，对需求定义的任何改进，设计上都必须大量的返工。把需求获取集中在用户任务上—而不是集中在用户接口上—有助于防止开发组由于草率处理设计问题而造成的失误。有几种原因使需求分析变得困难：（1）客户说不清楚需求；（2）需求自身经常变动；（3）分析人员或客户理解有误。 需求获取、分析、编写需求规格说明和验证并不遵循线性的顺序，这些活动是相互隔开、增量和反复的。当你和客户合作时，你就将会问一些问题，并且取得他们所提供的信息（需求获取）。同时，你将处理这些信息以理解它们，并把它们分成不同的类别，还要把客户需求同可能的软件需求相联系（分析）。然后，你可以使客户信息结构化，并编写成文档和示意图（说明）。下一步，就可以让客户代表评审文档并纠正存在的错误（验证）。这四个过程贯穿着需求分析的整个阶段。需求获取可能是软件开发中最困难、最关键、最易出错及最需要交流的方面。需求获取只有通过有效的客户—开发者的合作才能成功。分析者必须建立一个对问题进行彻底探讨的环境，而这些问题与产品有关。为了方便清晰地进行交流，就要列出重要的小组，而不是假想所有的参与者都持有相同的看法。对需求问题的全面考察需要一种技术，利用这种技术不但考虑了问题的功能需求方面，还可讨论项目的非功能需求。确定用户已经理解：对于某些功能的讨论并不意味着即将在产品中实现它。对于想到的需求必须集中处理并设定优先级，以避免一个不能带来任何益处的无限大的项目。 1.2.需求分析的一般方法
软件开发方法述评 发信人:Joaquin(maverick),信区:SoftEng 标题:软件开发方法评述 发信站:BBS水木清华站(TueNov1821:18:341997) 60年代中期开始爆发了众所周知的软件危机。为了克服这一危机，在1968、1969年连续召开的两次著名的NATO会议上提出了软件工程这一术语，并在以后不断发展、完善。与此同时，软件研究人员也在不断探索新的软件开发方法。至今已形成八类软件开发方法。 一、Parnas方法 最早的软件开发方法是由Ｄ．Parnas在1972年提出的。由于当时软件在可维护性和可靠性方面存在着严重问题，因此Parnas提出的方法是针对这两个问题的。首先，Parnas提出了信息隐蔽原则：在概要设计时列出将来可能发生变化的因素，并在模块划分时将这些因素放到个别模块的内部。这样，在将来由于这些因素变化而需修改软件时，只需修改这些个别的模块，其它模块不受影响。信息隐蔽技术不仅提高了软件的可维护性，而且也避免了错误的蔓延，改善了软件的可靠性。现在信息隐蔽原则已成为软件工程学中的一条重要原则。 Parnas提出的第二条原则是在软件设计时应对可能发生的种种意外故障采取措施。软件是很脆弱的，很可能因为一个微小的错误而引发严重的事故，所以必须加强防范。如在分配使用设备前，应该取设备状态字，检查设备是否正常。此外，模块之间也要加强检查，防止错误蔓延。 Parnas对软件开发提出了深刻的见解。遗憾的是，他没有给出明确的工作流程。所以这一方法不能独立使用，只能作为其它方法的补充。 二、 SASA方法 1978年，E．Yourdon和L．L．Constantine提出了结构化方法，即SASD方法，也可称为面向功能的软件开发方法或面向数据流的软件开发方法。1979年TomDeMarco对此方法作了进一步的完善。 Yourdon方法是80年代使用最广泛的软件开发方法。它首先用结构化分析（SA）对软件进行需求分析，然后用结构化设计（SD）方法进行总体设计，最后是结构化编程（SP）。这一方法不仅开发步骤明确，SA、SD、SP相辅相成，一气呵成，而且给出了两类典型的软件结构（变换型和事务型），便于参照，使软件开发的成功率大大提高，从而深受软件开发人员的青睐。 三、面向数据结构的软件开发方法 Jackson方法
对软件开发的理解和认识作 业 -标准化文件发布号：（9456-EUATWK-MWUB-WUNN-INNUL-DDQTY-KII
对软件开发的理解和认识 专业：计算机技术 现在软件已经和我们的生活息息相关，渗透到各行各业，例如现在我们平时接触到的windows操作系统、玩的电子游戏、使用的财务软件、机场的售缥系统、医院的挂号系统、还有我们去唱歌的点歌系统等等都属于软件的范围。举一个例子来说，你肯定用过自动提款机吧？提款机本是一台实体机器，金属的，本身台机器是不会给您提供任何服务的，所有就需要有一套东西来提示您插卡、输入密码、取多少钱、拔卡等等步骤，这就叫做软件。然后告知我们是制作软件的，在IT业内称为软件开发。 软件工程把整个软件开发过程分为几个方面。只有每个方面都做好了，才有可能做成一个好的系统，这只是一个必要条件而非充分条件。每个阶段的产出就是文档，在瀑布开发模型里面，下一阶段所需要的信息来源于上一阶段的文档。 软件开发流程即软件设计思路和方法的一般过程，包括设计软件的功能和实现的算法和方法、软件的总体结构设计和模块设计、编程和调试、程序联调和测试以及编写、提交程序。 第一步：需求调研分析 1相关系统分析员向用户初步了解需求，然后用WORD列出要开发的系统的大功能模块，每个大功能模块有哪些小功能模块，对于有些需求比较明确相关的界面时，在这一步里面可以初步定义好少量的界面。
2 系统分析员深入了解和分析需求，根据自己的经验和需求用WORD或相关的工具再做出一份文档系统的功能需求文档。这次的文档会清楚例用系统大致的大功能模块，大功能模块有哪些小功能模块，并且还列出相关的界面和界面功能。 3 系统分析员向用户再次确认需求。 第二步：概要设计 首先，开发者需要对软件系统进行概要设计，即系统设计。概要设计需要对软件系统的设计进行考虑，包括系统的基本处理流程、系统的组织结构、模块划分、功能分配、接口设计、运行设计、数据结构设计和出错处理设计等，为软件的详细设计提供基础。 第三步：详细设计 在概要设计的基础上，开发者需要进行软件系统的详细设计。在详细设计中，描述实现具体模块所涉及到的主要算法、数据结构、类的层次结构及调用关系，需要说明软件系统各个层次中的每一个程序(每个模块或子程序)的设计考虑，以便进行编码和测试。应当保证软件的需求完全分配给整个软件。详细设计应当足够详细，能够根据详细设计报告进行编码。 第四步：编码 在软件编码阶段，开发者根据《软件系统详细设计报告》中对数据结构、算法分析和模块实现等方面的设计要求，开始具体的编写程序工作，分别实现各模块的功能，从而实现对目标系统的功能、性能、接口、界面等方面的要求。 第五步：测试
软件开发过程管理规范文件管理序列号：[K8UY-K9IO69-O6M243-OL889-F88688]
0 引言 如果要提高软件开发人员的开发质量，必须有相应的考核制度，有了制度后才能推动开发人员想方设法改善自已的开发质量。目前研发对软件开发的过程缺乏细粒度的度量，所以不能依据有效的度量数据来考核开发人员的工作绩效，大部份只是凭考核人主观意志来考核，不能形成对被考核人有效的说服力。此绩效考核办法旨在结合实际情况合理客观地评价开发效率和质量。 1 目的 对软件开发的过程所产生的软件项的质量和过程进行定量的评价，用评价的结果指导软件的开发过程，不断地提高软件开发质量水平，并依据度量记录来考核软件开发人员的工作绩效。 2 软件项包括 1）技术文档：主要包括：可行性分析报告、需求分析报告、软件功能规格说明、开发计划、系统设计报告、测试文档、用户手册、总结报告等； 2）计算机程序。 3 度量数据的来源 1）项目计划； 2）评审报告； 3）测试报告； 4）问题报告； 5）软件维护记录； 4 质量度量
4.1 度量指标 主要根据各类软件项检查表的检查指标来确定，例如，软件需求规格说明书检查表（见附录1），有10个检查指标，则根据具体项目检查侧重点不同，可从中选择相应的检查指标作为度量指标。 4.2 质量等级 1）软件项的质量等级的确定根据度量综合指标进行。 2）度量综合指标计算公式为：Total = ∑QiMi。 3）其中i=1,2,...n代表指标数量； 4）Q代表度量的指标； 5）M代表度量的指标Q在整个指标体系中所占的权重系数，对不同的开发项目可能不同，此系数根据开发的不同着重点给出。 度量指标权重系数表： 序号指标权重 1 指标1 权数1 2 指标2 权数2 3 指标3 权数3 4 指标4 权数4 5 指标5 权数5 加权平均分 1.0 6）质量评价：一般地，根据度量综合指标值，有以下评分标准。 质量评价计分标准表 序号得分质量评价
快速原型方法与软件开发中的风险管理 软件系统往往体现一定的功能，这些功能要符合一定的使用目的。现实世界是在不断变化的，而且变化的速度是越来越快，唯一不变的就是“变化”的主题。这一现实也就直接影响到了实现实际功能的软件系统，体现在需求、技术实现手段、应用环境等多个方面，这些都直接影响到了软件系统自身的稳定性。同时，由于快速变化这一事实，人们对于以后的预测能力也越来越有限，有时根本难以明确未来的需求，只能是根据环境的变化而随时调整，因此直接导致了软件生命周期越来越短这一现实，特别是应用软件，直接与这种变化紧密相连。 但是，软件开发往往需要一定的时间，一个软件系统从需求、设计、开发到投入使用，这一周期都不会很短，即从需求产生到实际能够投入使用这段时间，其本身就已经成为应用软件自身的风险，很可能当一个软件开发完成的时候，市场需求已经发生了变化，开发出来的软件已经不适用了。软件生命周期已经缩短，特别是应用软件，随着新业务的市场窗口变窄的趋势，其自身的寿命周期也在缩短。快速投放市场已经成为软件系统的首要因素。另一方面，由于快速变化的外部环境给软件产品带来的风险，成本控制也成为软件工程管理的一个重要方面，通过对需求变化的风险的评估来重新认识软件寿命周期，以合理的成本完成软件开发，也已经成为对软件产品管理者的一个挑战。 在传统的软件工程方法中，主要使用瀑布式顺序开发方法，包括需求分析和定义、系统设计、实现和单元测试、系统集成测试、运行维护等多个阶段，这一方法的优点是全面、严谨，但最大的缺陷，就是过程一旦启动就难以适
应变化。这一方法是基于一个重要的假设前提——能够提出明确的需求。当面对快速变化、甚至是根本不明确的需求时，这种假设根本上就不成立，因此这种传统的开发方法的缺点就越来越突出，特别是应用软件的开发，由于它与市场的联系更加紧密，使用这种传统的开发方法，已经难以为继。我们需要寻找一种更加快速、成本合理的软件开发方法。 快速原型方法就是这样一种开发更加迅速、更加成本合理的开发方法。在软件开发过程中，最关键的步骤就是确切定义出需求，明确软件要实现的功能是什么，而这恰恰也是最困难的过程，因为现在许多用户在初期只有一个隐约的、大致的考虑，根本不可能提出具体明确的需求。这种情况下，使用快速原型进行反复交流、细化需求，就成为一种更加有效的方法。一个软件的原型，主要是模拟重要的功能和界面，但是一般不考虑运行效率，也不考虑系统的健壮性，出错处理也考虑不多，它的目的只是为了实际描述概念中的结构，使用户能够检测与其概念的一致性和概念的可用性。 目前主要有两种快速原型方法： ·丢弃原型（Throw-away prototyping）。其目标只是为了明确需求，使用最简单的开发方法，以最低的成本实现一个可工作的系统，该系统只关注功能，不考虑开发工具、性能、容错、未来实际运行环境等。通过反复与客户交流和修改原型，使原型的功能能够充分体现客户需求。在明确了需求之后，原型就会被丢弃。以后软件的开发将根据明确了的需求按照传统的工程化方法来开发。 ·进化原型（Evolutionary prototyping）。其目标就是与客户一起工作，从一个原始的需求的轮廓开始，逐步改进，最终发展成为符合实际需要的系
学习中心_________ 姓名_____________ 学号 西安电子科技大学网络教育学院 模拟试题三 《软件形式化方法》期末考试试题 （120分钟） 题号一二三四五六七总分 题分 得分 一、填空题。（20分） 1. 软件危机是指在计算机软件的过程中所遇到的一系列严重的问题，应对软件危机的方式分为两种方法：和。对于软件开发组织和管理的规范化方法中，主要研究、和三个要素。 2. 形式化方法研究如何把（具有清晰数学基础的）（描述形式、技术和过程等）融入软件开发的各个阶段；包括、形式化验证和程序精化三种活动。形式化验证主要技术包含和；程序精化是将与相结合，研究从抽象的推演出具体的面向计算机的。 3. 模式是Z语言规格中一个重要的元素，模式是由、和 组成。 4. Larch方法是软件系统规格的一种；Larch方法的程序规格包括和与目标语言相关的两个部分。 二、利用有限状态机描述“AB协议”。（15分） AB协议包含发送端和接收端两个实体。发送端协议实体从发送方用户获取一个报文，将序号寄存器值赋给报文，然后向接收端协议实体发出报文，发送方发出报文之后启动超时时钟，等待认可报文。如果在给定的时间内未收到认可报文，则重发报文；如果收到认可报文，其序号与发出报文序号相同，则发送端实体从发送方用户获取下个报文。接收端协议实体在收到报文之后，如果报文无错误，则想发送端实体发送认可报文，然后将报文递交给接收方用户；如果接收的报文有错误或者序号不正确，则丢失报文。假定所用通道不会中断；报文重复n次后最终能够被接收；认可报文只要发出就能正确收到；报文不会损坏；序号寄存器初始化为0 。 三、构造下图所示Petri网的覆盖树。（10分） 四、利用CSP对“生产者-消费者”系统进行规格。（10分） 五、逻辑演算证明。（15分） （1）?(Q∨R) ∧(P?Q)├?P （2）(P?(Q?S)) ∧ (?R∨P) ∧Q├ R→S （3）($x)P(x)?("x)(P(x)úQ(x)?R(x)), ($x)P(x), ($x)Q(x)├ R(a)ùR(c) 六、如图中所示的Kripke结构，利用标号算法对公式进行模型检验。（15） （1）E((p ∧r) ?p) （2）A(p?q) = ?E(?(p?q))
第一条综述 为调动公司软件研发人员的工作积极性，提高软件的开发质量和开发效率，促进研发人员深入市场，及时跟踪软件产品的使用情况，在公司现有绩效考评制度基础上制定此制度。 第二条管理办法 公司软件项目实行目标管理。 第三条执行范围 1）本制度适用于从事软件项目开发的人员。 2）本制度适用于软件项目开发运行全生命周期，即需求调研、软件设计、软件开发及测试、软件运行维护。 第四条整体考核目标 1）品质 2）工期详见《软件项目立项申请表》。 第五条奖金成立
1、部门主管根据市场需求，填写《软件项目立项申请表》并经需求提出项目主管、技术总监、技术副总、董事长签字同意。 2、技术副总、董事长认为可立项软件，下发《软件项目立项申请表》填写，经技术总监、项目负责人确认工期及缺陷数目。 第六条奖金构成 1、基础奖金总额： 1）合同类项目：项目奖金的发放额度在项目合同签订后确定，原则上不得超过所研发的软件合同金额的8％，不低于合同金额的5％，具体额度由部门经理、总工程师、技术总监协商，董事长最终确定。 2）投入类项目：由公司直接投入项目，在明确项目内容后，部门经理、总工程师、技术总监计算项目人员工时，核算投入金额报技术副总、财务总监、董事长确认项目总投入额。原则上以软件投入总金额的10％作为项目开发奖金。 3）当发生大市场变化，需要重新确定奖金发放额度时，可由部门经理提出，经过技术总监、主任工程师、技术副总、总经理重新协商后，董事长最终确定。 2、奖金构成：
1）项目承担部门奖励（奖励1） 奖金总金额的60%为工期奖金；发放对象：项目设计、开发、测试参与人员。 奖金总金额的40%为品质奖金；发放对象：项目设计、开发、测试参与人员。 2）应用奖金（奖励2） 应用奖金（奖励2）=奖励1的5%-8%。发放对象：应用部参与人员。 3）维护奖金（奖励3） 维护奖金（奖励3）=奖励1的5%-8%。发放对象：运维部参与人员。 4）特殊奖励（奖励4） 特殊奖励（奖励4）=最高为奖金总金额的10%为特殊奖励； 第七条奖金浮动 1、工期奖金： 项目提前完成时，按比例增加奖金发放额度，滞后时按比例减少发放额度。增减上限为奖金基础数额的50%。比例计算方法为：浮动比例＝（计
我对软件工程的认识 随着软件危机的存在才慢慢地产生了对软件工程的认识，在软件开发和维护的过程中存在着很多严重的问题，一方面与软件本身的特点有关，另一方面也和软件开发与维护的方法不正确有关，逐渐地产生了软件工程。 软件危机的表现： i)软件开发成本难以控制、软件开发进度难以预测。 费用超支、进度拖延的情况屡屡发生。有时为了赶进度或压成本不得不采取一些权宜之计，这样又往往严重损害了软件产品的质量。 ii)软件的可靠性差，产品质量无法保证。 软件是逻辑产品，质量问题很难以统一的标准度量，因而造成质量控制困难。尽管耗费了大量的人力物力，而系统的正确性却越来越难以保证，出错率大大增加。 iii)生产出来的软件难以维护 很多程序缺乏相应的文档资料，程序中的错误难以定位，难以改正，有时改正了已有的错误又引入新的错误。随着软件的社会拥有量越来越大，维护占用了大量人力、物力和财力。 iiii)软件成本在计算机系统总成本中所占的比例居高不下，且逐年上升。 由于微电子学技术的进步和硬件生产自动化程度不断提高，硬件成本逐年下降，性能和产量迅速提高。然而软件开发需要大量的人力，软件成本随着软件规模和数量的剧增而持续上升。 iiiii)软件开发生产率提高的速度远远满足不了计算机应用迅速普及深入的需要。软件产品供不应求的状况使得人类不能充分利用现代计算机硬件所能提供的巨大潜力。 iiiiii)用户对产品功能难以满足。 开发人员和用户之间很难沟通、矛盾很难统一。往往是软件人员不能真正了解用户的需求，而用户又不了解计算机求解问题的模式和能力，双方无法用共同熟悉的语言进行交流和描述。
软件工程是将系统的、科学的和严密的方法应用于设计、开发、运行和维护软件，以及对这些方法本身的研究，也就是将工程应用于软件，它由方法、工具和过程三部分组成，而软件是计算机系统中程序、数据和文档的集合。程序是用程序设计语言描述的、适合计算机处理的语句序列，数据是使程序能够适当地处理信息的数据结构，文档是软件开发、使用和维护程序所需要的图文资料。软件具有个体化、规模庞大、维护复杂和长期性的特点。软件又分为应用软件和系统软件。应用软件是用户可以使用的各种程序设计语言，以及用各种程序设计语言编制的应用程序的集合，分为应用软件包和用户程序。而系统软件是指控制和协调计算机及外部设备，支持应用软件开发和运行的系统，是无需用户干预的各种程序的集合，主要功能是调度，监控和维护计算机系统；负责管理计算机系统中各种独立的硬件，使得他们可以协调工作。 软件工程的框架可以概括为：目标、过程和原则。 （1）软件工程目标：生产具有正确性、可用性以及开销合宜的产品。正确性指软件产品达到预期功能的程度。可用性指软件基本结构、实现及文档为用户可用的程度。开销合宜是指软件开发、运行的整个开销满足用户要求的程度。这些目标的实现不论在理论上还是在实践中均存在很多待解决的问题，它们形成了对过程、过程模型及工程方法选取的约束。 （2）软件工程过程：生产一个最终能满足需求且达到工程目标的软件产品所需要的步骤。软件工程过程主要包括开发过程、运作过程、维护过程。它们覆盖了需求、设计、实现、确认以及维护等活动。需求活动包括问题分析和需求分析。问题分析获取需求定义，又称软件需求规约。需求分析生成功能规约。设计活动一般包括概要设计和详细设计。概要设计建立整个软件系统结构，包括子系统、模块以及相关层次的说明、每一模块的接口定义。详细设计产生程序员可用的模块说明，包括每一模块中数据结构说明及加工描述。实现活动把设计结果转换为可执行的程序代码。确认活动贯穿于整个开发过程，实现完成后的确认，保证最终产品满足用户的要求。维护活动包括使用过程中的扩充、修改与完善。伴随以上过程，还有管理过程、支持过程、培训过程等。
快速原型法(rapid prototyping) 快速原型法是近年来提出的一种以计算机为基础的系统开发方法，它首先构造一个功能简单的原型系统，然后通过对原型系统逐步求精，不断扩充完善得到最终的软件系统。原型就是模型，而原型系统就是应用系统的模型。它是待构筑的实际系统的缩小比例模型，但是保留了实际系统的大部分性能。这个模型可在运行中被检查、测试、修改，直到它的性能达到用户需求为止。因而这个工作模型很快就能转换成原样的目标系统。 原型法有三个层次 第一层包括联机的屏幕活动,这一层的目的是确定屏幕及报表的版式和内容、屏幕活动的顺序及屏幕排版的方法; 第二层是第一层的扩展，引用了数据库的交互作用及数据操作,这一层的主要目的是论证系统关键区域的操作，用户可以输入成组的事务数据，执行这些数据的模拟过程，包括出错处理; 第三层是系统的工作模型，它是系统的一个子集，其中应用的逻辑事务及数据库的交互作用可以用实际数据来操作，这一层的目的是开发一个模型，使其发展成为最终的系统规模。 原型法的主要优点在于它是一种支持用户的方法，使得用户在系统生存周期的设计阶段起到积极的作用;它能减少系统开发的风险，特别是在大型项目的开发中,由于对项目需求的分析难以一次完成，应用原型法效果更为明显。原型法的概念既适用于系统的重新开发，也适用于对系统的修改;原型法不局限于仅对开发项目中的计算机方面进行设计，第三层原型法是用于制作系统的工作模型的。快速原型法要取得成功，要求有象第四代语言(4GL)这样的良好开发环境/工具的支持。原型法可以与传统的生命周期方法相结合使用，这样会扩大用户参与需求分析、初步设计及详细设计等阶段的活动，加深对系统的理解。近年来，快速原型法的思想也被应用于产品的开发活动中。 快速原型方法与开发的风险管理 软件系统往往体现一定的功能，这些功能要符合一定的使用目的。现实世界是在不断变化的，而且变化的速度是越来越快，唯一不变的就是“变化”的主题。这一现实也就直接影响到了实现实际功能的软件系统，体现在需求、技术实现手段、应用环境等多个方面，这些都直接影响到了软件系统自身的稳定性。同时，由于快速变化这一事实，人们对于以后的预测能力也越来越有限，有时根本难以明确未来的需求，只能是根据环境的变化而随时调整，因此直接导致了软件生命周期越来越短这一现实，特别是应用软件，直接与这种变化紧密相
软件工程中的形式化方法研究论文 早期软件系统规模较小,20世纪60年代之前,对软件系统的开发一直通过“手工”方式,具有个人化及技艺化的开发特点60年代中期,计算机的容量和速度有了显著提升,软件系统规模越来越大,软件开发生产率不再能满足现状,软件危机开始爆发60年代后期,针对“软件危机”提出两类解决办法:一是将工程化应用于软件的开发过程,即“软件工程”的出现和发展;二是建立严格的理论基础,采用形式化方法来指导软件开发过程经过近半个世纪的探索和应用,形式化方法这一领域已经取得了大量的研究成果 1形式化方法 1.1形式化方法 软件工程中的形式化方法就是通过严格的符号系统和数学模型来描述和验证一个目标软件系统的行为和特性,包括需求规格、设计和实现等形式化方法所使用的是严格的数学语言,其语法和语义都是无二义的、精确的 1.2主要研究内容 形式化方法的研究主要集中在形式规约(FormalSpecification)和建立在形式规约基础上的形式验证(FormalVerification)两个方 面形式规约是指通过具有精确语义的形式语言对程序功能进行描述 描述结果将作为程序设计和验证的重要依据形式验证是对现有的程 序系统进行验证,检查其是否符合规约的要求传统的验证方式是通过实验对系统进行查错,包括模拟(simulation)和测试(testing)
1.3形式化方法的分类 根据描述方式,可将形式化方法归为两类: (1)模型描述的形式化方法通过构造一个数学模型来直接描述系统或程序 (2)性质描述的形式化方法通过对目标软件系统中不同性质的描述来间接描述系统或程序根据表达能力,可将形式化方法大概分为五类[Barroca*1992]: (1)模型方法——对系统状态和改变系统状态的动作直接给出抽象定义,并进行显式描述该方法的缺陷是不能显式地表示并发 (2)代数方法——通过定义不同操作的关系,隐式地描述操作与模型方法相同,代数方法也不能显式地表示并发 (3)进程代数方法——通过一个显式模型来描述并发过程将并发性归结为非确定性,通过交错语义(interleavingsemantics)来表示系统行为如:CCS,CSP,ACP等 (4)逻辑方法——通过描述程序状态规范和时间状态规范的逻辑方法来描述系统特性,如:CTL,LTL (5)网络模型方法——通过独立描述网络中的每一个节点,显式地给出系统的并发模型如:Petri网 2软件方法学 2.1软件危机 60年代后期,软件系统的规模逐步增大,程序实现地复杂度也越来越高,可靠性问题成为越来越多人关注的焦点由于软件开发生产率