第２Ｏ卷第６期 牡丹江大学学报 Ｖｏ１．２０ Ｎｏ．６ ２０１１年６月 Ｊｏｕｒｎａ １ ｏｆ Ｍｕｄａｎｊ ｉａｎｇ Ｕｎｉｖｏｒ ｓ ｉ ｔｙ Ｊｕｎ． ２Ｏ１１ 文章编号：１００８．８７１７（２０１ １）０６—０１０７－０２ 、 基于形式化技术的电梯系统规格说明 邵 丽 丽 （菏泽学院计算机与信息工程系，山东菏泽２７４０１５） 摘要：为克服非形式化技术描述系统规格说明带来的二义性，本文采用一种形式化技术——有穷状态机来描 述电梯系统的规格说明，有穷状态机技术准确、无歧义，可以正确地描述一个系统。 关键词：形式化技术；有穷状态机；电梯系统 中图分类号：ＴＵ８５７文献标识码：Ａ 引言 ｎ部电梯按照约束条件ｃ１，ｃ２和ｃ３在楼层间移动。 按照形式化的程度的不同，可以把描述系统规格说 ｃ１：每部电梯内有ｍ个按钮，每个按钮代表一个楼 明的方法划分成非形式化、半形式化和形式化方法三类。 层。当按下一个按钮时该按钮指示灯亮，同时电梯驶向 用自然语言描述的系统规格说明，是典型的非形式化方 相应的楼层，到达按钮指定的楼层时指示灯熄灭。 法；用数据流图、实体一联系图或状态图等图形方式建 ｃ２：除了大厦的最低层和最高层之外，每层楼都有 立模型，是典型的半形式化方法；用基于数学的方法描 两个按钮分别请求电梯上行和下行。这两个按钮之一被 述系统性质，那就是形式化的技术。 按下时相应的指示灯亮，当电梯到达此楼层时灯熄灭， 一、有穷状态机 电梯向要求的方向移动。 一个有穷状态机包括５个部分：状态集Ｊ、输入集Ｋ、 ｃ３：当对电梯没有请求时，它关门并停在当前楼层。 转换函数Ｔ、初态ｓ和终态集Ｆ。如果使用更形式化的 三、形式化规格说明 术语，一个有穷状态机可以表示为一个５元组（Ｊ，Ｋ， 现在使用有穷状态机技术对电梯系统进行规格说 Ｔ，Ｓ，Ｆ），其中： 明。这个问题中有两个按钮集。ｎ部电梯中的每一部都 Ｊ是一个有穷的非空状态集； 有ｍ个按钮，一个按钮对应一个楼层。因为这ｍ×ｎ个 Ｋ是一个有穷的非空输入集； 按钮都在电梯中，所以称它们为电梯按钮。此外，每层 Ｔ是一个从（Ｊ－Ｆ）×Ｋ到Ｊ的转换函数； 楼有两个按钮，一个请求向上，另一个请求向下，这些 ＳＥＪ，是一个初始状态； 按钮称为楼层按钮。 Ｆ Ｊ，是终态集。 １．电梯按钮的规格说明 为了对系统进行规格说明，通常需要使用扩展的有 电梯按钮的状态转化图如图１所示。令ＥＢ（ｅ，ｔ）表示 穷状态机，即在前述的５元组中加入第６个组件——谓 按下电梯ｅ内的按钮并请求到ｆ层去。 词集Ｐ，从而把有穷状态机扩展为１个６元组，其中每 个谓词都是系统全局状态Ｙ的函数。转换函数Ｔ现在是 一个从（Ｊ—Ｆ）×Ｋ×Ｐ到Ｊ的函数。用有穷状态机技术 表示的状态转换规则的形式如下： 图ｌ 电梯按钮的状态转换图 当前状态＋事件＋谓词＝ 下个状态。 图１中有两个状态，分别是： 二、电梯系统 ＥＢＯＮ（ｅ，ｆ）：电梯按钮ｅ，Ｉ）打开； 下面是用自然语言描述的对电梯系统的需求：在一 ＥＢＯＦＦ（ｅ￣：电梯按钮（ｅ，Ｄ关闭。 幢ｍ层的大厦中需要一套控制ｎ部电梯的产品，要求这 图１中包含了两个事件，分别是： 收稿日期：２０１０．１２．２３ 作者简介：邵丽丽（１９７９一）， 女，山东曹县人，菏泽学院计算机系讲师，硕士，研究方向：软件工程与智 能管理。 １０７ ＥＢＰ（ｅ，ｆ）：电梯按钮（ｅ，ｆ）被按下； ＥＡＦ（ｅ，Ｄ：电梯ｅ到达ｆ层。 定义谓词Ｖ（ｅ，ｆ１，它的含义是电梯ｅ停在ｆ层。 根据图１，使用谓词ｖ（ｅ，ｆ），形式化转换规则为： ＥＢＯＦＦ（ｅ，ｆ）＋ＥＢＰ（ｅ，ｆ）＋ｎｏｔ ｖ（ｅ，０＝＝＞ＥＢＯＮ（ｅ，ｆ），反之， ＥＢＯＮ（ｅ，０＋ＥＡＦ（ｅ山＝＝＞ＥＢＯＦＦ（ｅ，ｆ） 图３中包含了３个可触发状态发生改变的事件，分 别是： ＤＣ（ｅ，Ｉ）：电梯ｅ在楼层ｆ关上门； ＳＴ（ｅ，ｆ）：电梯ｅ靠近ｆ层时触发传感器，电梯控制 器决定在当前楼层电梯是否停下； ＲＬ：电梯按钮或楼层按钮被按下进入打开状态，登 录需求。 由于电梯的状态非常复杂，包含多个子状态，例如： 关门、电梯加速、电梯减速、停止、开门、过一段时间 ２．楼层按钮的规格说明 楼层按钮的状态转化图如图２所示，令ＦＢ（ｄ，ｆ）表示 ｆ层请求电梯向ｄ方向运动的按钮， 图２楼层按钮的状态转化图 图２中有两个状态，分别是： ＦＢＯＮ（ｄ，ｆ）：楼层按钮（ｄ，１）打开； ＦＢＯＦＦ（ｄ，ｆ）：楼层按钮（ｄ，｛）关闭。 图２中包含了两个事件，分别是： ＦＢＰ（ｄ．ｆ）：楼层按钮（ｄ，ｆ）被按下； ＥＡＦ（１…ｎ，０：电梯１或…或ｎ到达ｆ层；其中１…ｎ 表示或为１或为２…或为ｎ。 定义谓词：ｓ（ｄ，ｅ ，它的含义是电梯ｅ停在ｆ层并且 移动方向由ｄ确定为向上（ｄ＝ｕ）或向下（ｄ＝Ｄ）或待定 （ｄ＝Ｎ）。 根据图２，使用谓词Ｓ（ａ，ｅ＇ｆ），形式化转换规则为： ＦＢＯＦＦ（ｄ，ｆ）＋ＦＢＰ（ｄ，ｆ）＋ｎｏｔ ｓ（ｄ，１…ｎ，ｆ）＝＝＞ＦＢＯＮ（ｄ，ｆ）， 反之 ＦＢＯＮ（ｄ，ｆ）＋ＥＡＦ（１…ｎ．０＋Ｓ（ｄ，１…ｎ，１） ＦＢＯＦＦ（ｄ＇１）， 其中，ｄ＝Ｕ ｏｒＤ。 ３．电梯的状态及其转化规则 为了描绘电梯的状态转化图，下面定义电梯的３个 状态： Ｍ（ｄ，ｅ，０：电梯ｅ正沿ｄ方向移动，即将到达的是第 ｆ层； ｓ（ａ，ｅ，Ｉ）：电梯ｅ停在ｆ层，将朝ｄ方向移动（尚未 关门）； Ｗ（ｅ，０：电梯ｅ在ｆ层等待（已关门）。 电梯的状态转换图如图３所示： 图３电梯的状态转化图 １０８ 自动关门等。所以本文给出的电梯状态转换规则仅发生 在关门之时。 Ｓ（Ｕ，ｅ．ｆ）＋ＤＣ（ｅ，ｆ）＝ Ｍ（Ｕ，ｅ』＋１） ＳｆＤ，ｅ．０＋ＤＣ（ｅ，ｆ）＝＝＞ｎ（Ｄ，ｅＳ－１） Ｓ（Ｎ，ｅ，０＋ＤＣ（ｅ，ｆ）＝＝＞Ｗ（ｅ 第一条规则表明，如果电梯ｅ停在ｆ层准备向上移 动，且门已经关闭，则电梯将向上一楼层移动。第二条 和第三条规则，分别对应于电梯即将下降或者没有待处 理的请求的情况。 四、小结 有穷状态机方法采用了一种简单的格式来描述系统 的规格说明： 当前状态＋事件＋谓词＝ 下个状态。 这种方法是建立在严格的数学基础上的方法，具有 严谨的逻辑性，所以基于形式化技术的电梯系统规格说 明能够克服传统的非形式化技术描述的规格说明中的不 完整性、二义性和不一致性，并可以有效地保证下一步 电梯系统设计工作的正确性。尽管有穷状态机方法为系 统做需求分析规格说明提供了很好的技术，但它有个缺 点就是在开发一个大型系统时，三元组（即状态、事件、 谓词）的数量会迅速增长。这是我们在实践中需要注意 的地方。 参考文献： 川Ｉ张海藩．软件工程导论（第５版）【Ｍ】．北京：清华大学 出版社。２００８． 【２】姚全珠，崔杜武，李海刚．管理信息系统开发中的形式化 需求分析方法研究【Ｊ】．西安理工大学学报，２００２，ｌ８（３）： ２３ １－２３４． ［３】姚全珠，王江．基于ＵＭＬ的软件形式化需求分析与验 证［Ｊ】计算机工程，２０１０，３６（１３）：３０－３３． 【４吕蕴华，４］张三元，叶修梓．ＣＡＤ系统中嵌套有穷状态自 动机的设计与实现【Ｊ】．现代机械，２００３，（３）：３３－３４，４５．
