圖書管理系統之形式化及建模方法研究

黃小英

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