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

黃小英

HUANG Xiao-ying

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

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

The study of formal and modeling methods for library management system

黃小英

HUANG Xiao-ying

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

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

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

0 引言

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

1 形式化方法簡介

形式化方法（Formal Methods）是構造安全軟件的重要途徑之一，這種軟件開發(fā)方法建立在數學基礎上，通過形式化的方法來研究計算機等科學中的有關問題，對計算機系統(tǒng)進行分析和驗證。在軟件工程領域，形式化方法建模一般采用形式化規(guī)格說明語言來描述具體問題。線性時序邏輯是目前軟件工程領域常用的形式化描述語言之一。

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

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

2 線性實序邏輯LTL語法和語義

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

SD=

其中Obj、Msg、Loc分別表示順序圖中對象的集合、消息的集合以及位點的集合；F則表示從消息到位點的函數，即

其中，s表示發(fā)送消息，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）當沒有消息收發(fā)事件時，對象Oi的狀態(tài)不改變。語義如下：

2）當對象Oi發(fā)送消息時，Oi的狀態(tài)不改變。語義如下：

3）當對象Oi接收消息時，Oi的狀態(tài)可能改變。語義如下：

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

5）當對象Oi從對象Om接收到消息時，Oi的狀態(tài)可能改變，Om的狀態(tài)不改變。語義如下：

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

圖書管理系統(tǒng)中比較重要的順序圖就是借書和還書順序圖，本文以圖書管理系統(tǒng)的借書和還書為例，給出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是一種標準的對象建模語言，它的優(yōu)點是有目共睹的，如UML可以提供多種元素來描述軟件系統(tǒng)分析和設計的結果，提高了系統(tǒng)設計的可視化程度。然而，UML非形式化的特性使得它無法分析和驗證系統(tǒng)模型的一致性和準確性。本文對UML的形式化建模作了一定的研究，并將線性時序邏輯語法用在圖書管理系統(tǒng)的借書和還書順序圖中，以提高圖書管理系統(tǒng)需求分析的準確性和安全性，為進一步形式化分析打下了基礎。

[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 -），女，廣西寧明人，講師，工程碩士，研究方向為軟件工程。