软件工程的形式化方法第六讲

软件工程中的形式化方法研究早期软件系统规模较小,20世纪60年代之前,对软件系统的开发一直通过“手工”方式,具有个人化及技艺化的开发特点。

60年代中期,计算机的容量和速度有了显著提升,软件系统规模越来越大,软件开发生产率不再能满足现状,软件危机开始爆发。

60年代后期,针对“软件危机”提出两类解决办法:一是将工程化应用于软件的开发过程,即“软件工程”的出现和发展;二是建立严格的理论基础,采用形式化方法来指导软件开发过程。

经过近半个世纪的探索和应用,形式化方法这一领域已经取得了大量的研究成果。

1形式化方法1.1形式化方法软件工程中的形式化方法就是通过严格的符号系统和数学模型来描述和验证一个目标软件系统的行为和特性,包括需求规格、设计和实现等。

形式化方法所使用的是严格的数学语言,其语法和语义都是无二义的、精确的。

1.2主要研究内容形式化方法的研究主要集中在形式规约(FormalSpecification)和建立在形式规约基础上的形式验证(FormalVerification)两个方面。

形式规约是指通过具有精确语义的形式语言对程序功能进行描述。

描述结果将作为程序设计和验证的重要依据。

形式验证是对现有的程序系统进行验证,检查其是否符合规约的要求。

传统的验证方式是通过实验对系统进行查错,包括模拟(simulation)和测试(testing)。

1.3形式化方法的分类根据描述方式,可将形式化方法归为两类:(1)模型描述的形式化方法。

通过构造一个数学模型来直接描述系统或程序。

(2)性质描述的形式化方法。

通过对目标软件系统中不同性质的描述来间接描述系统或程序。

根据表达能力,可将形式化方法大概分为五类[Barroca*1992]:(1)模型方法——对系统状态和改变系统状态的动作直接给出抽象定义,并进行显式描述。

该方法的缺陷是不能显式地表示并发。

(2)代数方法——通过定义不同操作的关系,隐式地描述操作。

与模型方法相同,代数方法也不能显式地表示并发。

软件工程形式化方法 z 语言软件工程是一个复杂而庞大的领域，要确保软件系统的正确性和可靠性，需要采用各种形式化方法。

形式化方法是一种严格、精确的描述和分析系统的方法，其中最著名的是Z语言。

1. 什么是形式化方法形式化方法是一种使用数学符号和形式化规范来描述和分析软件系统的方法。

它能够捕捉系统的各个方面，从而确保系统的正确性和可靠性。

形式化方法可以消除歧义和模糊性，提供严格的语法和语义定义，并进行可靠的推理和验证。

2. Z语言的引入和发展Z语言是一种基于数学集合论和一阶谓词逻辑的形式化规范语言。

它于20世纪70年代由牛津大学的J.R.阿兰·特拉弗斯和J.B.斯托拉兹提出，并继续在软件工程领域的学术界和实践中得到广泛应用。

3. Z语言的特点和优势- 精确性：Z语言使用严格的数学符号和形式化规范，可以精确地描述系统的各个方面，避免了自然语言的歧义和模糊性。

- 可读性：尽管Z语言使用了数学符号，但其符号系统和语法规则都经过严格定义，使得Z规范可以被可靠地解释和理解。

- 可验证性：Z语言规范的严格性使得系统的正确性验证变得可行。

通过形式化推理和模型检测等技术，可以对规范进行自动验证和分析。

- 模块化：Z语言支持模块化规范，可以将系统的不同部分进行独立的规范和验证，从而提高开发过程的灵活性和可重用性。

4. Z语言在软件工程中的应用- 需求分析和规约：Z语言可以用于对软件系统的需求进行精确描述和形式化规约，从而帮助开发人员和用户准确理解和交流需求。

- 设计规约和验证：Z语言可以用于对软件系统的设计进行精确描述和形式化规约，并进行验证和验证。

通过验证，可以发现设计冲突和错误，提高系统的可靠性。

- 系统建模和仿真：Z语言可以用于对软件系统进行形式化的建模和仿真。

通过建立形式化模型，可以进行系统行为的精确分析和评估，从而帮助设计和优化系统。

- 代码生成和自动化工具支持：Z语言可以作为设计工具中的一部分，与代码生成和其他自动化工具集成，从而提高开发效率和系统质量。

第六讲软件工程的形式化说明技术软件工程使用的描述技术有三类：非形式化技术、半形式化技术和形式化技术。

所谓非形式化技术的代表方法是用自然语言描述的需求规格说明；所谓半形式化技术的代表方法有数据流图、E-R图和UML等；所谓形式化技术的方法有很多，其中具有代表性的方法包括有：时序逻辑语言、有穷状态机、Petri网系统和Z语言等；所谓形式化规格说明语言的关键思想是把软件开发过程中的需求规格说明阶段和软件设计说明阶段分开,在需求规格说明阶段精确地描述软件“做什么”，而不涉及“怎么做”。

编写规格说明与编写计算机程序的不同之处在于规格说明是对目标软件系统的功能描述，而计算机系统则是实现目标软件系统功能的过程描述。

形式化和非形式化描述方法各有优缺点形式化描述的优点：1．使用形式化方法可以严格准确地描述出系统对象；2．使用形式化方法描述的系统可以向任意具体系统进行映射转换；3．可以对形式化描述的系统进行严格的数学证明分析；形式化描述的缺点：1．形式化描述方法难以使用；2．使用形式化描述一个庞大的实际系统存在许多困难，在实际应用中有许多问题本身就是模糊或非确定的无法使用严格的形式化方法进行描述；3．形式化描述的模型对于那些没有经过专门的训练用户来说很难理解；4．形式化说明的正确性证明费时费力；5．尚未出现支持形式化风格全过程的软件环境；非形式化方法的优点：1．描述的模型直观，容易理解；2．非形式的描述技术比较简单，容易学习；3．许多的应用只能使用非形式化的方法描述；非形式化方法的缺点：1．非形式化的描述可能存在矛盾、二意性和含糊性等问题；2．难以进行严格的证明工作；3．对于高可靠性的系统，使用该方法描述存在潜在的问题；本文介绍三种形式化方法：有穷状态机、Petri网、Z语言有穷状态机：使用一个六元组来准确地描述系统状态的变化的一种形式化方法。

当前状态+事件+谓词=>下一个状态Petri 网：Petri的背景：Petri网的首次提出是由德国科学家Petri于1962年在他的博士论文《用自动机通讯》中提出的使用网状结构模拟通讯系统。

软件工程中的形式化方法研究综述随着软件复杂度和规模的不断增长，传统的软件开发方法已经不能满足软件开发的需求。

为了提高软件开发的可靠性和效率，人们开始思考如何使用形式化方法对软件开发进行改进。

形式化方法一般指使用一些严格的数学描述和理论来验证软件系统的正确性。

在本文中，我们将对软件工程中的形式化方法进行研究综述。

一、形式化方法的概念和原理形式化方法是一种使用严格的逻辑和数学语言来描述和验证软件系统的方法。

它通过使用形式语言来表示软件系统的规范和要求，采用严格的数学推理和证明方法来验证软件系统的正确性。

形式化方法可以被看作一个理论框架，其中包括用于建模、验证和证明软件系统行为的各种技术和工具。

形式化方法的核心原理基于数学和逻辑思维的严密性。

其主要思想是将软件行为和要求形式化为数学形式，然后使用严格的数学推理和证明方法来验证软件系统的正确性。

形式化方法使用精确的语言和符号来描述软件系统的规范和要求，有效地避免了自然语言描述中的歧义和模糊性。

在使用形式化方法进行软件开发时，程序员需要将要求和规范转化为数学符号和逻辑公式，这有助于程序员更准确地理解系统的行为和需求。

形式化方法的基本步骤包括建立模型、定义规范、进行验证和证明。

建立模型是指将软件系统的行为形式化为一种数学模型。

定义规范是指将软件系统的要求和约束形式化为一种逻辑公式。

验证和证明是指使用数学推理和证明方法来证明软件系统符合规范和要求。

二、形式化方法在软件工程中的应用形式化方法在软件工程中的应用可以提高软件开发的可靠性、正确性和效率。

下面我们将讨论形式化方法在软件工程中的应用。

1. 需求分析在软件开发过程中，需求分析是非常重要的一个环节。

使用形式化方法可以帮助程序员更加准确地理解和描述系统的需求和约束。

通过使用数学符号和逻辑公式，程序员可以更加准确地定义和描述系统的需求，有助于程序员更好地掌握系统的行为和要求。

2. 设计在软件开发过程中，设计是一个非常关键的步骤。

软件开发中的形式化方法郑红军张乃孝（北京大学计算机科学技术系，北京 100871）摘要本文基于研究的角度，首先讨论了在软件开发过程各阶段使用形式化方法的可能及困难，进而研究了形式化方法在理论上和应用上的能力、局限性及其产生原因，以及由此产生的对形式化方法的讨论。

最后，综合上述讨论，从形式化方法的实质出发，在方法上，对形式化方法的研究提出了几点建议，以及基于这些建议所能看到的形式化方法研究可能的一些发展方向。

关键词形式化方法软件开发1 形式化方法随着软件系统复杂度的不断增长，开发正确、可靠的软件，成为一个急待解决的问题。

解决此问题的一个有前途、有希望的技术是形式化方法的应用。

形式化方法建立在严格的数学基础上，其目标是希望能使系统具有较高的可信度和正确性，并能使系统具有良好的结构，使其易维护，关键是能较好地满足用户需求。

“形式化方法”一词虽然一直被广泛地应用，但在不同程度上，因理解不同，使其具有了不同的含义。

一般说来，形式化方法是指具有坚实数学基础的方法，它是数学上的综合、分析技术的应用，用于开发计算机控制的系统，经常有推理工具的支持，它可提供一个用于模型设计和分析的一个严格而有效的途径。

从形式系统和复杂问题的本质来看，还未有一个适于全面描述和分析一个复杂系统的形式系统。

所以，可以说，一个“形式化方法”并不是系统设计者开发系统时可能选择使用的方法，而只是设计者在此过程中希望利用的一种工具之一[Wood* 1988]。

总体上，形式化方法大致可分为五类[Barroca* 1992]：（1）基于模型的方法—给出系统（程序）状态和状态变换操作的显式但亦是抽象的定义，但对于并发没有显式的表示，如：Z和VDM[Jones 1990]。

（2）代数方法—通过联系不同操作间的行为关系而给出操作的隐式定义，而不定义状态，同样，它亦未给出并发的显式表示，如：OBJ、CLEAR。

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