软件工程（八）

PETRI网

并发系统中遇到一个主要问题：定时问题。定时问题通常是由不好的设计或有错误的实现引起的，而这样的设计或实现通常又是由于不好的规格说明造成的。如果规格说明不恰当，则有导致不完善的设计或实现的危险。

概念：

PETRI网的组成



Petri网包含4种元素：

1）一组位置P，上例 P＝{P1,P2,P3,P4}

在图中用圆圈代表位置

2）一组转换T，上例 T＝{t1,t2}

在图中用短直线表示转换

3）输入函数I，上例 I（t1）={P2,P4}

I（t2）={P2}

4）输出函数O，上例O（t1）={P1}

O（t2）={P3,P3}

更形式化的Petri网结构，是一个4元组（P，T，I，O）

PETRI网是由Carl Adam Petri发明的。最初只有自动化专家对Petri网感兴趣，后来，Petri网在计算机科学中也得到广泛的应用。

如：性能评价

操作系统

软件工程

Z语言

在形式化的规格说明语言中，Z语言赢得广泛赞誉，使用Z语言需要具备集合论、函数、数理逻辑等方面的知识。

简介：

用Z语言描述的、最简单的形式化规格说明含有4部分：

给定的集合、数据类型及常数

状态定义

初始状态

操作

给定的集合

一个Z规格说明从一系列给定的初始化集合开始。

所谓初始化集合：就是不需要详细定义的集合，这种集合用带方括号的形式表示。

例如：

[ Button]

状态定义

一个Z规格说明由若干个“格（schema）”组成，每个格含有一组变量说明和一系列限定变量取值范围的谓词。

例如：

Button有4个子集：

floor_buttons(楼层按钮的集合)

elevator_buttons(电梯按钮的集合)

buttons(电梯问题中所有按钮的集合)

pushed(所有被按的按钮的集合)

初始状态

抽象的初始状态是指系统第一次开启时的状态。

操作

如果一个原来处于关闭状态的按钮被按下，则该按钮启动。这个按钮就被添加到pushed集中。

Z语言的语法规定，当一个格被用在另一格中，要在它的前面加上三角形符号△作为前缀，因此Push_Button的第一行最前面有一个三角形符号作为个Button_State的前缀。

基于数学的形式化说明技术，目前还没有在软件产业界广泛应用；

应该把形式化方法与传统方法有机结合。

欢迎关注我的微信个人订阅号



每天多学一点0.0