第六讲 软件工程的方法

第六讲软件工程的形式化说明技术软件工程使用的描述技术有三类：非形式化技术、半形式化技术和形式化技术。所谓非形式化技术的代表方法是用自然语言描述的需求规格说明；所谓半形式化技术的代表方法有数据流图、E-R图和UML等；所谓形式化技术的方法有很多，其中具有代表性的方法包括有：时序逻辑语言、有穷状态机、Petri网系统和Z语言等；所谓形式化规格说明语言的关键思想是把软件开发过程中的需求规格说明阶段和软件设计说明阶段分开，在需求规格说明阶段精确地描述软件“做什么”，而不涉及“怎么做”。编写规格说明与编写计算机程序的不同之处在于规格说明是对目标软件系统的功能描述，而计算机系统则是实现目标软件系统功能的过程描述。形式化和非形式化描述方法各有优缺点形式化描述的优点：使用形式化方法可以严格准确地描述出系统对象；使用形式化方法描述的系统可以向任意具体系统进行映射转换；可以对形式化描述的系统进行严格的数学证明分析；形式化描述的缺点：形式化描述方法难以使用；使用形式化描述一个庞大的实际系统存在许多困难，在实际应用中有许多问题本身就是模糊或非确定的无法使用严格的形式化方法进行描述；3.形式化描述的模型对于那些没有经过专门的训练用户来说很难理解；形式化说明的正确性证明费时费力；尚未出现支持形式化风格全过程的软件环境；非形式化方法的优点：描述的模型直观，容易理解；非形式的描述技术比较简单，容易学习；许多的应用只能使用非形式化的方法描述；非形式化方法的缺点：非形式化的描述可能存在矛盾、二意性和含糊性等问题；难以进行严格的证明工作；对于高可靠性的系统，使用该方法描述存在潜在的问题；本文介绍三种形式化方法：有穷状态机、Petri网、Z语言有穷状态机：使用一个六元组来准确地描述系统状态的变化的一种形式化方法。当前状态+事件+谓词=＞下一个状态Petri网：Petri的背景：Petri网的首次提出是由德国科学家Petri于1962年在他的博士论文《用自动机通讯》中提出的使用网状结构模拟通讯系统。Petri网有时又被称为网论。Petri的知识结构包括有基本网系统为主的特殊网论和通用网论。Petri网的本质是：将系统的动态行为表现为资源的流动。程序系统的动态特性分为两类：安全性和进展性。安全性要求所有可能的状态均具有一定的性质，并要求变化服从给定的规律，其关心的是可能性；进展性要求某些特定的状态一定能够达到的，其关心的是必然性；有时人们也提到描述系统性质的活性，其等同于进展性；基本网论（EN_系统）基本网系统中的状态元素被称为条件，变迁元素被称为事件。事件的发生改变条件的状态，引起信息在网上的流动。条件/事件系统（C/E_系统）非形式地说，满足一定要求的基本网系统就是一个C/E—系统；为简单网；每个条件都有机会成真，也有机会成假；每个事件都有机会发生；C/E—系统是通用网论的基础。基本网论和条件/事件网论是构成其他各级网系统的基础，C/E—系统是通用网论的基础。库所/变迁系统（P/T_系统）P表示库所，T代表变迁，该系统是最早期的Petri网的形式，主要以研究资源流动为特征。是以孤立的网系统为对象，以寻求分析技术和应用方法为目标的“特殊”网系统。P_元被称为库所（place）；T_元被称为变迁；P_元中的黑点个数被称为资源的数量，每个黑点被称为托肯（token）又被称为标记和令牌；带箭头的连线表示资源流动的方向；箭头上的数字表示组装所需或产生该种资源的数量，称为弧上的权；K表示库所的容量；

实例一：火车调度系统设计实例二：处理两个进程的同步问题进程得到资源占用资源运行释放资源不使用资源运行PR1厂LOCKR—处理11tUNLOCKR—处理12—PR2厂LOCKR—处理21—UNLOCKR—处理22—j实例三：生产流水线系统（来分析什么是冲突、饿死和死锁）通用网论Petri网的通用网论主要研究内容是：以网系统的全体作为研究对象，研究其分类及各分类之间的关系，发展了以并发论，同步论和网逻辑、网拓扑和信息流结构为主要研究内容的理论体系。网逻辑（enlogy）:是以推论为基础的直观语义框架。研究的系统中不能够发生的事件与系统行为的关系。这些事件是由于一完备化操作构造而得的。同步论：为各种同步现象（发送、传递和接收信息的这些动作之间的同步）提供定量的描述，与网逻辑结合使用是一种有效的系统规范设计工具。信息流结构：通俗地说就是信息流图的网表示，是沟通网论和其他学科的界面网拓扑（nettopology）:空间的拓扑结构是区分离散数学和连续数学的基础。拓扑空间的连续映射既是连续数学的主要研究工具，同时又是连续数学的主要研究对象。由于实际应用中的网系统一般都只有有限多个节点，在通常的拓扑意义下不可能连续的。必须有适用于网系统拓扑，即网拓扑。并发论：如果ab和ba的后果是一样的，a和b就并行，或a与b并行则ab和ba效果一样。Z语言：背景Z语言是70年代末至80年代初由英国Oxford大学研究组PRG的JeanRaym