形式化开发方法-Petri网

《形式化开发方法-Petri网》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、软件工程形式化方法第5章形式化开发方法(1)内容安排软件开发的形式化方法形式化开发方法(1)–Petri网形式化开发方法(2)–时态逻辑形式化开发方法(3)–Z方法3软件开发的形式化方法软件开发的形式化方法定义软件开发的形式化方法（formalmethods）是建立在严格数学基础上，具有精确数学语义的开发方法简单地说，凡在系统研究中，应用了数学的方法，都是形式化方法本章所介绍的形式化开发方法是指软件规格说明数学建模、数学验证和数学程序求精4形式化方法与结构化和OO方法区别结构化和OO方法使用了大量的自然语言。自然语言的二义

2、性、不完整和抽象层次的混杂等问题的解决，必然使开发系统的质量不高、成本增加和进度拖长；尤其对安全性或其他质量因素要求极高的软件，任何微小的错误都可能带来灾难性的后果形式化的方法可以帮助软件开发人员开发出更为无二义性、完整的和准确的需求规格说明，进而通过严格的验证发现问题，以达到对软件质量、开发成本和开发进度的有效控制5形式化开发方法发展历史20世纪60年代末形式化方法与非形式化大致同步都是为解决当时出现的“软件危机”提出一般认为是Floyd、Hoare和Manna等在程序正确性证明方面的研究。但由于这些方法受程序规模的限制

3、而未能应用20世纪80年代末在硬件设计领域形式化方法的工业应用结果，又掀起了软件形式化开发方法的学术研究和工业应用的热潮，建立了一些较为成熟的方法和语言如Petri网、statecharts、通信顺序过程、通信系统演算、程序正确性证明、时态逻辑、模型验证、Z语言、VDM及Larch等6目前流行的形式化开发方法形式化规格说明建模形式化验证形式化程序求精7形式化规格说明建模操作类基于状态和转移Petri网、有限状态机和状态图描述类基于数学公理和概念基于逻辑的描述方法：命题线性时态逻辑（PLTL）、一阶线性时态逻辑（FOLTL）

4、、计算树逻辑（CTL）基于代数的描述方法：Z语言、VDM和Larch双重类兼有操作类和描述类两者的特点扩展状态机（ESM）、实时时态逻辑（RTTL）8形式化验证模型验证和定理证明模型验证是对规格说明所建立起来的模型状态空间进行搜索，以确认该系统模型是否具有所期望的某些性质定理证明是以逻辑公式作为系统及其性能的规格说明，其中逻辑由一个具有公理和推理规则的形式化系统给出。进行定理证明的过程就是应用这些公理或推理规则来证明系统是否具有所期望的性质9形式化程序求精形式化程序求精就是将自动推理与形式化规格说明相结合而形成的一门技术研

5、究如何从形式化的规格说明推演出具体的面向计算机的程序代码的全过程基本思想就是用一个抽象程度低和过程性强的程序，去代替一个抽象程度高和过程性弱的程序，并保证它们的功能和性质完全一致形式化程序求精与形式化规格说明和形式化验证三者是紧密联系和相辅相成10形式化开发方法主要问题对软件开发人员（包括管理人员和用户）的数学素质有较高的要求主要是离散数学中的集合、代数结构、数理逻辑等基础内容在软件工程中的具体应用对于原来一些数学背景较差的工程人员要花许多时间去学习和掌握。有的甚至还要克服对数学的畏惧心理在选择和应用形式化开发方法时应注意

6、的问题Bowan和Hinchley提出了“形式化法方法的十条戒律”11形式化开发方法(1)Petri网12什么是Petri网Petri网是一种网状结构的系统的描述和分析工具对于具有并发、异步、分布、并行、不确定性或随机性的信息系统，都可以利用这种工具构造出要开发的Petri网模型。然后对其进行分析，即可得到有关系统结构和动态行为方面的信息。根据这些信息就可以对要开发的系统进行评价和改进Petri网的提出由德国C.A.Petri在他的62年博士论文“Communicationwithautomata”中提出当时引起一些欧美科

7、学家的重视。他们在引用这种网状结构模拟和分析并行系统中称它为“PetriNets”。从此以后大家都称它为Petri网13Petri网介绍的内容示例-四季系统ΣPetri网的定义Petri网的基本原理-静态结构Petri网的基本原理-动态特征建模实例特性分析Petri网的特性分析方法改进Petri网及其应用时间网和随机网从Petri网到程序结构的转换14示例：四季系统Σ一年有四季，四季气候的变化该Σ系统可以由图形表示15系统Σ的Petri网图形表示16系统Σ的Petri网数学表示Σ=（P，T；F，M0）P={p1,p2,p3

8、,p4}T={t1,t2,t3,t4}F={（p1,t1）,（t1,p2）,（p2,t2）,（t2,p3）,（p3,t3）,（t3,p4）,（p4,t4）,（t4,p1）}M0=（0,0,0,1）17Petri网描述系统Σ的特点从四季系统Σ中，可以看出这种利用事物的因果关系对系统进行网状结构的描述，有以