邵丽丽

(菏泽学院 计算机与信息工程系，山东 菏泽 274015)

基于Petri网的电梯系统规格说明

邵丽丽

(菏泽学院 计算机与信息工程系，山东 菏泽 274015)

为克服非形式化技术描述系统规格说明带来的二义性，采用了一种形式化技术——Petri网来描述电梯系统的规格说明。Petri网技术是对离散并行系统的数学表示，适合于描述并发的计算机系统模型，可以正确的描述电梯系统。

Petri网;形式化技术;电梯系统

0 引言

按照形式化的程度的不同，可以把描述系统规格说明的方法划分成非形式化、半形式化和形式化方法3类。用自然语言描述的系统规格说明，是典型的非形式化方法;用数据流图、实体－联系图或状态图等图形方式建立模型，是典型的半形式化方法;用基于数学的方法描述系统性质，那就是形式化的技术。Petri网技术是形式化技术的一种，它既有直观的图形表达方式，也有严格的数学表述方式，能有效地描述并发活动，可以正确的描述系统的规格说明。

1 Petri网

1.1 Petri网的结构

一个Petri网包括4个元素:库所(Place)、变迁(Transition)、有向弧(Connection)、令牌(Token)，如图1所示。其中库所为圆形节点，变迁为短直线，有向弧是库所和变迁之间的箭头线，令牌是库所中的动态对象，可以从一个库所移动到另一个库所。

在图1中有一组库所 P 为{P1，P2，P3，P4}，一组变迁 T为{t1，t2}，两个用于变迁的输入函数:是由库所指向变迁的箭头表示，它们是:

两个用于变迁的输出函数:是由变迁指向库所的箭头表示，它们是:

一个经典的Petri网可以表示为一个四元组(库所，变迁，输入函数，输出函数)，如果使用更形式化的术语，一个Petri网可以表示为一个四元组C=(P，T，I，O)，任何图都可以映射到这样一个四元组上。……