软件开发的形式化方法

出版时间：2005-1  出版社：高等教育出版社  作者：古天龙  页数：265  
Tag标签：无  

前言

软件是计算机应用系统中不可分割的一个重要组成部分。在商务数据库管理、宇宙飞船、机器人、飞机控制、通信系统、核电站控制、制造自动化等系统中，软件发挥着不可替代的作用。但在软件设计和开发中会遇到不少困难和问题。严谨的软件开发和设计方法——形式化方法，为解决或部分解决这些困难提供了可行途径。形式化方法是基于严密的、数学上的形式机制的系统研究方法。客观地讲，有了数学的应用，就有了形式化方法。但是，一般认为形式化方法是始于20世纪60年代末的Floyd、Hoare和Manna等在程序正确性证明方面的研究，当时由于“软件危机”，人们试图用数学方法证明程序的正确性而发展成为了各种程序验证方法，但是受程序规模的限制，这些方法并未达到预期的应用效果。从20世纪80年代末开始，由于在硬件设计领域形式形式化方法的工业应用的结果，掀起了形式化方法和技术的学术研究和工业应用的热潮。在建立软件设计和开发的形式基础方面，研究人员已开展了大量的工作，建立了一些较为成熟并初步进入应用的方法和语言，例如：Statecharts、Petri 网、通信系统演算、程序正确性证明、时态逻辑、模型检验、Z、VDM、Larch等。从广义角度，形式化方法是软件开发过程中规格、设计及实现的系统工程方法。狭义地，形式化方法是软件规格和验证的方法，因此，形式化方法又分为形式化规格方法和形式化验证方法。形式化规格就是通过数学符号对系统及行为进行精确、简洁的描述。任何大型系统开发的前提都是需求规格。没有这样的规格，系统开发人员就没有一个系统用户的确切描述，这些用户就不得不从多个方面承担不明确规格带来的误错后果。精确的需求规格已被大多数工程学科所接受，计算机系统在精确性方面并不比任何其他工程任务差。然而，不幸的是，当今的软件工业实践在很大程度上还依赖于非形式文本和图形。形式化的另一个方面是设计的验证。程序是数学化的文本，这样就有可能解释程序和它们规格之间的形式关系。基于形式化方法，可以建立软件或程序在各种情形下性质及行为的描述。系统开发的步骤可以基于形式化规格，也可以针对形式化规格来验证。这样，在开发过程中就可以采用形式化验证以及时检查出误错。开发过程中尽早地消除误错是改善软件开发过程质量的关键之一，也是工业应用中采用形式化方法的一个重要理由。

内容概要

形式化方法是建立在严格数学基础上、具有精确数学语义的开发方法。从广义角度，形式化方法是软件开发过程中分析、设计及实现的系统工程方法。狭义地，形式化方法是软件规格和验证的方法。本书对软件开发中的形式化方法进行了介绍和讨论，内容涵盖了SE2004中关于“软件的形式化方法”的知识点，主要包括：有限状态机、Statecharts、Petri网、通信顺序进程、通信系统演算、一阶逻辑、程序正确性证明、时态逻辑、模型检验、Z、VDM、Larch等。　　本书可作为计算机、软件工程等专业高年级本科声或研究生的教学用书，也可供相关领域的研究人员和工程技术人员参考。

书籍目录

第1章　软件及其开发概述　1.1　软件开发的历史　1.2　软件危机　1.3　软件工程　1.4　形式化方法　习题第2章　有限状态机及其扩展　　2.1　有限状态机　2.2　Statecharts　习题第3章　Petri网　　3.1　位置/迁移Petri网　3.2　高级Petri网　习题第4章　进程代数　　4.1　通信顺序进程　　　4.2　通信系统演算　习题第5章　一阶逻辑　　5.1　命题逻辑　5.2　谓词逻辑　　5.3　程序正确性证明　习题第6章　时态逻辑　　6.1　模态逻辑　　6.2　线性时态逻辑　　6.3　计算树逻辑　　6.4　模型检验　习题第7章　Z　7.1　概述　　7.2　表示抽象　　7.3　操作抽象　　7.4　Z规格的例　习题第8章　VDM　8.1　概述　　8.2　表示抽象　　8.3　操作抽象　　8.4　VDM规格的例　习题第9章　Larch参考文献

章节摘录

第1章软件及其开发概述软件或者程序是计算机及其应用系统的一个重要组成部分。伴随着计算机的诞生和发展，软件及其开发经历了半个多世纪的历程。本章简要回顾了软件及其开发的历史；阐述了软件发展过程中的软件危机、软件工程、软件开发的形式化方法等。1.1软件开发的历史第一台通用电子数字计算机ENIAC于1946年2月15日诞生，与之相伴，出现了计算机软件（早期称为程序）。软件是计算机系统中与硬件相互依存的另一部分，它与硬件合为一体完成系统功能。在计算机发展的早期阶段（1946年到20世纪60年代中期），计算机系统还是以硬件为主，软件费用只占总费用的20％左右；到了计算机发展的第二个阶段（20世纪60年代中期到20世纪80年代初期），在硬件费用成倍下降的同时，软件费用却迅速上升，达到了总费用的60％以上；之后软件费用一直持续上升，其在计算机系统总费用中的比例一直上升到今天的80％以上。所谓软件开发，实际上就是把现实世界的需求反映成软件的模型化并予以实现的过程。在计算机发展的不同时期，人们对软件的认识不同，相应地，所进行的软件开发也具有不同的特点。软件及其开发大体经历了如下三个阶段：（1）程序设计阶段（1946年-1956年）自1946年2月15日第一台通用电子数字计算机ENIAC宣告研制成功，到1956年高级语言的诞生，是软件发展的第一个阶段。

编辑推荐

《软件开发的形式化方法》是由高等教育出版社出版。

用户评论 (总计3条)

•   国内的书，还是不错的
•   这本书的内容还挺全的，不错的，适合打基础
•   国内这类书籍的确不多，挺好