黃小英

HUANG Xiao-ying

（廣西工商職業(yè)技術(shù)學(xué)院，南寧 530003）

圖書(shū)管理系統(tǒng)之形式化及建模方法研究

The study of formal and modeling methods for library management system

黃小英

HUANG Xiao-ying

（廣西工商職業(yè)技術(shù)學(xué)院，南寧 530003）

UML是一種通用的圖形化建模語(yǔ)言，在面向?qū)ο笙到y(tǒng)的分析與設(shè)計(jì)中，形成了一個(gè)統(tǒng)一的、公共的、具有廣泛適用性建模語(yǔ)言，但它并不是形式化的建模語(yǔ)言，缺乏精確的表示語(yǔ)義，表達(dá)不嚴(yán)格。線性時(shí)序邏輯（LTL)是一種形式化語(yǔ)言，是并發(fā)或反應(yīng)式程序動(dòng)態(tài)語(yǔ)義，適合用來(lái)精確表示模型的動(dòng)態(tài)語(yǔ)義。本文介紹UML的形式化建模方法，詳細(xì)描述線性時(shí)序邏輯語(yǔ)言的語(yǔ)法及語(yǔ)義，并將形式化建模方法用在圖書(shū)管理系統(tǒng)中。

形式化方法；LTL；UML；順序圖

0 引言

UML是一種標(biāo)準(zhǔn)的統(tǒng)一建模語(yǔ)言，這種語(yǔ)言是一種通用的圖形建模語(yǔ)言，在面向?qū)ο笙到y(tǒng)的分析和設(shè)計(jì)中，它已成為了事實(shí)上的工業(yè)標(biāo)準(zhǔn)。然而，UML畢竟不是形式化的建模語(yǔ)言，它缺乏精確的表示語(yǔ)義，表達(dá)不嚴(yán)格，在對(duì)所建立的模型進(jìn)行一致性檢查和正確性分析方面，具有難以克服的缺陷，難于對(duì)系統(tǒng)進(jìn)行進(jìn)一步的求精和驗(yàn)證[1,5]。因此，結(jié)合UML和形式化語(yǔ)言對(duì)系統(tǒng)建模，成為近幾年來(lái)軟件工程的研究熱點(diǎn)之一。

1 形式化方法簡(jiǎn)介

形式化方法（Formal Methods）是構(gòu)造安全軟件的重要途徑之一，這種軟件開(kāi)發(fā)方法建立在數(shù)學(xué)基礎(chǔ)上，通過(guò)形式化的方法來(lái)研究計(jì)算機(jī)等科學(xué)中的有關(guān)問(wèn)題，對(duì)計(jì)算機(jī)系統(tǒng)進(jìn)行分析和驗(yàn)證。在軟件工程領(lǐng)域，形式化方法建模一般采用形式化規(guī)格說(shuō)明語(yǔ)言來(lái)描述具體問(wèn)題。線性時(shí)序邏輯是目前軟件工程領(lǐng)域常用的形式化描述語(yǔ)言之一。

線性時(shí)序邏輯（Linear Temporal Logic，簡(jiǎn)稱LTL）是并發(fā)或反應(yīng)式程序動(dòng)態(tài)語(yǔ)義的形式化描述語(yǔ)言[2]，其基礎(chǔ)是一個(gè)包含有限個(gè)命題的命題集。時(shí)序邏輯可以追溯到很早以前，其核心思想是將時(shí)間看作一些列離散狀態(tài)，時(shí)間的延續(xù)等同于狀態(tài)間的傳遞。1977年，以色列的Amir Pnueli在他的論文中首次提出線性時(shí)序邏輯的概念。Pnueli在一階謂詞邏輯的基礎(chǔ)上加入與時(shí)間有關(guān)的操作符，以對(duì)計(jì)算進(jìn)行推理，據(jù)此驗(yàn)證程序的正確性。用LTL描述的語(yǔ)義具有直觀性和自然性，更適于描述模型的動(dòng)態(tài)語(yǔ)義。除此之外，LTL適合描述系統(tǒng)的某些不良性質(zhì)永遠(yuǎn)不出現(xiàn)和描述某些良好性質(zhì)永遠(yuǎn)保持，因此能更好地描述系統(tǒng)的安全性和活躍性，是構(gòu)建安全軟件的基礎(chǔ)之一。

形式化方法和常規(guī)的軟件工程方法的開(kāi)發(fā)原則有所不同，形式化方法注重于能夠直接設(shè)計(jì)出盡量正確的系統(tǒng)，而常規(guī)方法則一般都需要通過(guò)測(cè)試才能發(fā)現(xiàn)系統(tǒng)的錯(cuò)誤。采用形式化方法可以提高系統(tǒng)的可靠性、可維護(hù)性和可復(fù)用性，因此需求分析的形式化程度對(duì)于提高軟件工程的質(zhì)量有極大的幫助。目前對(duì)UML建模的形式化研究大多數(shù)集中在UML的活動(dòng)圖和狀態(tài)圖方面，針對(duì)UML順序圖形式化的描述仍不多見(jiàn)[3]。因此，本文對(duì)UML順序圖形式化進(jìn)行研究。采用線性時(shí)序邏輯形式化描述語(yǔ)言結(jié)合UML建模，定義圖書(shū)管理系統(tǒng)順序圖的形式化語(yǔ)法，并給出順序圖語(yǔ)義描述。

2 線性實(shí)序邏輯LTL語(yǔ)法和語(yǔ)義

我們用一個(gè)四元組表示UML順序圖[2]，四元組的定義如下：

SD=

其中Obj、Msg、Loc分別表示順序圖中對(duì)象的集合、消息的集合以及位點(diǎn)的集合；F則表示從消息到位點(diǎn)的函數(shù)，即

其中，s表示發(fā)送消息，r表示接收消息。

LTL主要包含以下時(shí)序算子[2][4]：

直到算子μ：sμr代表s一直為真直到r為真；

等待算子ω：sωr代表s永遠(yuǎn)為真，或s一直為真直到r為真；

自從算子ξ：sξr代表在過(guò)去自從r為真后，s一直為真；

退回算子β：sβr代表在過(guò)去s一直為真，或自從r為真后，s一直為真；

任一時(shí)刻算子□：□s代表s永遠(yuǎn)為真，或s一直為真；

下一時(shí)刻算子○：○s代表s在下一時(shí)刻為真；

利用上述定義和算子，可以表示UML順序圖的基本交互事件的語(yǔ)義。

根據(jù)定義1，則用LTL定義的UML 順序圖的5種基本交互事件的語(yǔ)義如下：

1）當(dāng)沒(méi)有消息收發(fā)事件時(shí)，對(duì)象Oi的狀態(tài)不改變。語(yǔ)義如下：

2）當(dāng)對(duì)象Oi發(fā)送消息時(shí)，Oi的狀態(tài)不改變。語(yǔ)義如下：

3）當(dāng)對(duì)象Oi接收消息時(shí)，Oi的狀態(tài)可能改變。語(yǔ)義如下：

4）當(dāng)對(duì)象Oi將消息發(fā)送給對(duì)象Om時(shí)，Oi的狀態(tài)不改變，Om的狀態(tài)可能改變。語(yǔ)義如下：

5）當(dāng)對(duì)象Oi從對(duì)象Om接收到消息時(shí)，Oi的狀態(tài)可能改變，Om的狀態(tài)不改變。語(yǔ)義如下：

3 圖書(shū)管理系統(tǒng)UML順序圖的形式化描述

圖書(shū)管理系統(tǒng)中比較重要的順序圖就是借書(shū)和還書(shū)順序圖，本文以圖書(shū)管理系統(tǒng)的借書(shū)和還書(shū)為例，給出UML順序圖的形式化描述。

圖書(shū)管理員處理借書(shū)順序圖如圖1所示。

圖1 圖書(shū)管理員處理借書(shū)順序圖

圖書(shū)的對(duì)象有借閱者、圖書(shū)管理員、Lend Book Windows、Book和Loan，為便于書(shū)寫(xiě)，本文將這些對(duì)象分別記為r、mu、lw、b、l。形式化描述如下：

使用LTL對(duì)該順序圖主要事件進(jìn)行形式化表示的語(yǔ)義描述如下：

還書(shū)的UML順序圖見(jiàn)圖2，

圖書(shū)管理員處理還書(shū)順序圖如圖2所示。

圖2 圖書(shū)管理員處理還書(shū)順序圖

圖書(shū)的對(duì)象有借閱者、圖書(shū)管理員、Return Book Windows、Book和Loan，為便于書(shū)寫(xiě)，本文將這些對(duì)象分別記為r、mu、rw、b、l。形式化描述如下：

使用LTL對(duì)該順序圖主要事件進(jìn)行形式化表示的語(yǔ)義描述如下：

4 結(jié)束語(yǔ)

UML是一種標(biāo)準(zhǔn)的對(duì)象建模語(yǔ)言，它的優(yōu)點(diǎn)是有目共睹的，如UML可以提供多種元素來(lái)描述軟件系統(tǒng)分析和設(shè)計(jì)的結(jié)果，提高了系統(tǒng)設(shè)計(jì)的可視化程度。然而，UML非形式化的特性使得它無(wú)法分析和驗(yàn)證系統(tǒng)模型的一致性和準(zhǔn)確性。本文對(duì)UML的形式化建模作了一定的研究，并將線性時(shí)序邏輯語(yǔ)法用在圖書(shū)管理系統(tǒng)的借書(shū)和還書(shū)順序圖中，以提高圖書(shū)管理系統(tǒng)需求分析的準(zhǔn)確性和安全性，為進(jìn)一步形式化分析打下了基礎(chǔ)。

[1] 戎玫,張廣泉.形式化與可視化相結(jié)合的軟件體系結(jié)構(gòu)描述方法研究[J].計(jì)算機(jī)科學(xué),2005,32(4):205-208.

[2] 戎玫,張廣泉.UML順序圖的一種形式化描述方法[J].重慶師范大學(xué)學(xué)報(bào)(自然科學(xué)版),2007,24(3):528-532.

[3] 黃隴,于洪敏,陳致明.UML順序圖的結(jié)構(gòu)化操作語(yǔ)義研究[J].計(jì)算機(jī)應(yīng)用,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 -），女，廣西寧明人，講師，工程碩士，研究方向?yàn)檐浖こ獭?/p>