图书管理系统之形式化及建模方法研究

黄小英

HUANG Xiao-ying

（广西工商职业技术学院，南宁 530003）

图书管理系统之形式化及建模方法研究

The study of formal and modeling methods for library management system

黄小英

HUANG Xiao-ying

（广西工商职业技术学院，南宁 530003）

UML是一种通用的图形化建模语言，在面向对象系统的分析与设计中，形成了一个统一的、公共的、具有广泛适用性建模语言，但它并不是形式化的建模语言，缺乏精确的表示语义，表达不严格。线性时序逻辑（LTL)是一种形式化语言，是并发或反应式程序动态语义，适合用来精确表示模型的动态语义。本文介绍UML的形式化建模方法，详细描述线性时序逻辑语言的语法及语义，并将形式化建模方法用在图书管理系统中。

形式化方法；LTL；UML；顺序图

0 引言

UML是一种标准的统一建模语言，这种语言是一种通用的图形建模语言，在面向对象系统的分析和设计中，它已成为了事实上的工业标准。然而，UML毕竟不是形式化的建模语言，它缺乏精确的表示语义，表达不严格，在对所建立的模型进行一致性检查和正确性分析方面，具有难以克服的缺陷，难于对系统进行进一步的求精和验证[1,5]。因此，结合UML和形式化语言对系统建模，成为近几年来软件工程的研究热点之一。

1 形式化方法简介

形式化方法（Formal Methods）是构造安全软件的重要途径之一，这种软件开发方法建立在数学基础上，通过形式化的方法来研究计算机等科学中的有关问题，对计算机系统进行分析和验证。在软件工程领域，形式化方法建模一般采用形式化规格说明语言来描述具体问题。线性时序逻辑是目前软件工程领域常用的形式化描述语言之一。

线性时序逻辑（Linear Temporal Logic，简称LTL）是并发或反应式程序动态语义的形式化描述语言[2]，其基础是一个包含有限个命题的命题集。时序逻辑可以追溯到很早以前，其核心思想是将时间看作一些列离散状态，时间的延续等同于状态间的传递。1977年，以色列的Amir Pnueli在他的论文中首次提出线性时序逻辑的概念。Pnueli在一阶谓词逻辑的基础上加入与时间有关的操作符，以对计算进行推理，据此验证程序的正确性。用LTL描述的语义具有直观性和自然性，更适于描述模型的动态语义。除此之外，LTL适合描述系统的某些不良性质永远不出现和描述某些良好性质永远保持，因此能更好地描述系统的安全性和活跃性，是构建安全软件的基础之一。

形式化方法和常规的软件工程方法的开发原则有所不同，形式化方法注重于能够直接设计出尽量正确的系统，而常规方法则一般都需要通过测试才能发现系统的错误。采用形式化方法可以提高系统的可靠性、可维护性和可复用性，因此需求分析的形式化程度对于提高软件工程的质量有极大的帮助。目前对UML建模的形式化研究大多数集中在UML的活动图和状态图方面，针对UML顺序图形式化的描述仍不多见[3]。因此，本文对UML顺序图形式化进行研究。采用线性时序逻辑形式化描述语言结合UML建模，定义图书管理系统顺序图的形式化语法，并给出顺序图语义描述。

2 线性实序逻辑LTL语法和语义

我们用一个四元组表示UML顺序图[2]，四元组的定义如下：

SD=

其中Obj、Msg、Loc分别表示顺序图中对象的集合、消息的集合以及位点的集合；F则表示从消息到位点的函数，即

其中，s表示发送消息，r表示接收消息。

LTL主要包含以下时序算子[2][4]：

直到算子µ：sµr代表s一直为真直到r为真；

等待算子ω：sωr代表s永远为真，或s一直为真直到r为真；

自从算子ξ：sξr代表在过去自从r为真后，s一直为真；

退回算子β：sβr代表在过去s一直为真，或自从r为真后，s一直为真；

任一时刻算子□：□s代表s永远为真，或s一直为真；

下一时刻算子○：○s代表s在下一时刻为真；

利用上述定义和算子，可以表示UML顺序图的基本交互事件的语义。

根据定义1，则用LTL定义的UML 顺序图的5种基本交互事件的语义如下：

1）当没有消息收发事件时，对象Oi的状态不改变。语义如下：

2）当对象Oi发送消息时，Oi的状态不改变。语义如下：

3）当对象Oi接收消息时，Oi的状态可能改变。语义如下：

4）当对象Oi将消息发送给对象Om时，Oi的状态不改变，Om的状态可能改变。语义如下：

5）当对象Oi从对象Om接收到消息时，Oi的状态可能改变，Om的状态不改变。语义如下：

3 图书管理系统UML顺序图的形式化描述

图书管理系统中比较重要的顺序图就是借书和还书顺序图，本文以图书管理系统的借书和还书为例，给出UML顺序图的形式化描述。

图书管理员处理借书顺序图如图1所示。

图1 图书管理员处理借书顺序图

图书的对象有借阅者、图书管理员、Lend Book Windows、Book和Loan，为便于书写，本文将这些对象分别记为r、mu、lw、b、l。形式化描述如下：

使用LTL对该顺序图主要事件进行形式化表示的语义描述如下：

还书的UML顺序图见图2，

图书管理员处理还书顺序图如图2所示。

图2 图书管理员处理还书顺序图

图书的对象有借阅者、图书管理员、Return Book Windows、Book和Loan，为便于书写，本文将这些对象分别记为r、mu、rw、b、l。形式化描述如下：

使用LTL对该顺序图主要事件进行形式化表示的语义描述如下：

4 结束语

UML是一种标准的对象建模语言，它的优点是有目共睹的，如UML可以提供多种元素来描述软件系统分析和设计的结果，提高了系统设计的可视化程度。然而，UML非形式化的特性使得它无法分析和验证系统模型的一致性和准确性。本文对UML的形式化建模作了一定的研究，并将线性时序逻辑语法用在图书管理系统的借书和还书顺序图中，以提高图书管理系统需求分析的准确性和安全性，为进一步形式化分析打下了基础。

[1] 戎玫,张广泉.形式化与可视化相结合的软件体系结构描述方法研究[J].计算机科学,2005,32(4):205-208.

[2] 戎玫,张广泉.UML顺序图的一种形式化描述方法[J].重庆师范大学学报(自然科学版),2007,24(3):528-532.

[3] 黄陇,于洪敏,陈致明.UML顺序图的结构化操作语义研究[J].计算机应用,2005,25(2):359-361.

TH166

A

1009-0134(2010)11(下)-0004-03

10.3969/j.issn.1009-0134.2010.11(下).02

2010-08-29

黄小英（1976 -），女，广西宁明人，讲师，工程硕士，研究方向为软件工程。