形式化软件开发方法

1、形式化软件开发方法第三组 2111301155 李林钢形式化方法的含义n从广义上讲，形式化方法是借助数学的方法形式化方法是借助数学的方法来解决软件工程领域的问题，主要包括建立来解决软件工程领域的问题，主要包括建立精确的数学模型以及对模型的分析活动。精确的数学模型以及对模型的分析活动。n狭义的讲，形式化方法是运用形式化语言，形式化方法是运用形式化语言，进行形式化的规格描述、模型推理和验证的进行形式化的规格描述、模型推理和验证的方法。方法。形式化方法的含义n就形式化建模而言，形式化表示必须包含一组定义其语法语义的形式化规则。这些规则可用于分析给定的表达式是否符合语法规定，或证明该表达式具有某种性质

2、。形式化方法的出发点 n形式化方法的出发点是数学逻辑方法数学逻辑方法，其目的是开发可靠的软目的是开发可靠的软件产品件产品。n从软件开发来讲，形式化方法目前并非软件开发的主流。从软件发展看，早期的软件是用于数值计算，程序语言侧重于函数和算法的描述，后来数据库的应用和数据结构逐渐变得重要。现在的软件更为复杂，因此，对象、组件、接口、通讯、开放等成为非常重要的概念。n从软件工程方法来讲，有一套描述这些概念的办法，比如说用图形、表格、逻辑、自然语言等，交叉使用以描述一个系统的各个方面。因此换一个角度来考虑，我们也可以以目前常用的软件开发方法为出发点，研究怎样将这些方法形式化，使软件系统的描述精确化，以

3、减少可能的误解所带来的问题；或以目前常用的软件开发过程为出发点，研究怎样在软件开发过程中增加一些形式化方法的应用，以提高软件的可靠性。 形式化方法的分类n形式化方法可以分为形式化描述形式化描述和建立在形式化描述基础之上的形式化开发形式化开发。n形式化的描述就是用形式化的语言(具有严格的语法语义定义的语言，如流程图，petri网等)做描述。n形式化的软件开发，就是用形式化的语言来描述软件需求和特征，并且通过推理验证来保证最终的软件产品是否满足这些需求和具备这些特征。n这样的验证当然得建立在严格的语法语义的基础之上的。在实际应用中，这是不容易做到的。形式化方法形式化方法研究的目的就是希望能够提供更

4、好的理论、方法和研究的目的就是希望能够提供更好的理论、方法和工具，扩大形式化方法的应用范围和使用价值。工具，扩大形式化方法的应用范围和使用价值。 形式化方法的意义 n形式化方法的意义在于它能帮助发现其它方法不容易发现的系统描述的不一致、不明确或不完整，有助于增加软件开发人员对系统的理解，因此形式化方法是形式化方法是提高软件系统，特别是提高软件系统，特别是Safety-Critical系统的安全性系统的安全性与可靠性的重要手段与可靠性的重要手段。最早的形式化方法是逻辑与逻辑推理，它的目标是使推理机械化。n从广义上讲，这一目标受到许多挫折，比如说逻辑系统的不完备性(incompleteness)、

5、逻辑系统的不可判定性(undecidability)、自动推理的难处理性(intractability)。但是在一些实际应用上，逻辑方法和自动推理还是起着非常大的作用。 形式化方法的作用 n形式化方法在软件开发中能够起到的作用是多方面的。n首先是对软件需求的描述对软件需求的描述，软件需求的描述是软件开发的基础。比如说一般非形式化的描述很可能导致描述的不明确和不一致，如果描述的不明确和不一致将导致设计、编程的错误，将来的修改所要付出的代价就非常大了，如果导致的错误没有被发现，则影响程序的可靠和使用。形式化方法则要求描述的明确性，而描述的不一致性也就相对易于发现。 形式化方法的作用n其次是对软件设

6、计的描述对软件设计的描述。软件设计的描述和软件需求的描述一样重要，形式化方法的优点对于软件需求的描述同样适用于软件设计的描述，另外由于有了软件需求的形式化描述，我们可以检验软件的设计是否满足软件的要求。n对于编程来讲对于编程来讲，我们可以考虑自动代码生成。对于一些简单的系统，形式化的描述有可能直接转换成可执行程序，这就简化了软件开发过程，节约了资源和减少了出错的可能性。另外，形式化方法可以用于程序的验证，以保证程序的正确性。n对于测试来讲对于测试来讲，形式化方法可用于测试用例的自动生成，这可以节约许多时间和在一定程度上保证测试用例的覆盖率。 形式化方法的争议和缺陷1.形式化方法中所包含的数学理

7、论数学理论，限制了大多数程序设计人员的学习和使用；2.认为采用形式化方法会延误项目开发周期、延误项目开发周期、增加开发费用增加开发费用；3.许多流行的形式化方法对于较小规模的项目是有效的，但却很难应用于一些大型系统很难应用于一些大型系统；4.形式化方法不能确保不能确保开发出完全正确的软件；5. 缺乏缺乏对软件生命周期内各个阶段提供全面支持的形式化方法；形式化方法的描述方式n形式化方法原则上就是用数学与逻辑的方法形式化方法原则上就是用数学与逻辑的方法描述和验证软件描述和验证软件。n从描述上讲，一方面是系统或程序的描述，另一方面是性质的描述。这些可以用一种或多种语言来描述。这些语言包括命题逻辑，一

8、阶逻辑，高阶逻辑，代数，状态机，并发状态机，自动机，计算树逻辑，线性时序逻辑，进程代数， -演算， -演算，特殊的程序语言，以及程序语言的子集等。形式化方法的描述方式n从验证来讲，主要有两类方法，一类是以逻辑推理为基础，另一类则以穷尽搜索为基础。逻辑推理有 natural deduction, sequent calculus, resolution 以及Hoare-logic 等方法。穷尽搜索方法统称为模型检测。这类方法与系统或程序以及系统性质的表示有很大的关系，比如说符号模型检测，其基本原理是用命题逻辑公式表示状态转换关系，用不动点算法计算状态的可达性以及这些状态是否满足某些性质。 软件形

9、式化方法的研究方向 n(1) 基础概念基础概念：复合、抽象、重用模型、数学理论组合、数据结构及算法。 n(2) 形式化方法与面向对象方法的结合：形式化方法与面向对象方法的结合：这方面的研究体现在两个方面：利用面向对象结构来提高形式符号的表达能力；使用形式化方法来分析面向对象的语义或提高这些标记符号的表达对象概念的能力。 n(3) 工具开发：工具开发：具有良好用户界面、易于学习和操作简单的形式化方法支撑工具（如原型开发工具Axure），对于形式化方法的推广应用是大有裨益的。追求通用的完善的形式化方法及其支撑工具是不现实的，侧重于如下某一个或几个方面准则的特色方法和工具是未来研究的重点。 关于形式化方法的几点建议及发展方向关于形式化方法的几点建议及发展方向 n基于上面对形式化方法的分析和讨论，我们提出对形式化方法的几点可能的改进，从而也就确定了形式化方法的一些发展方向。1.可重用的规范库及更易接受的符号系统将更有助于形式化方法的研究与应用。在这方面，目前也有一些研究成果；对可重用规范的研究目前较少。当然，这一改进工作并不是短期内可以完成的。2.改进形式规范的语法、语义定义的质量，从而可以使得形式化方法更加“稳定”。3.加强规范语言中对并发控制和容错处理的表达能力，同时也要使精化技术能够处理这类并发机制和容错。这方面的改进也是长期的研究课题。4.对于