基于時序描述邏輯的UML順序圖形式化研究①

冉 婕,謝樹云,漆麗娟

(云南昭通學院 物理與信息工程學院,昭通 657000)

引言

統一建模語言(Unified Modeling Language,UML)[1,2]是OMG(Object Management Group)提出的標準對象建模語言,又稱標準建模語言,是支持模型化和軟件系統開發的圖形化語言,而且它從不同的角度表達軟件設計中的動態和靜態信息,但UML是一種半形式化的語言,缺乏精確的語義,不能對系統的交互行為進行形式化分析及論證[3].多數的UML建模工具不能提供完善的管理框架,UML模型的形式化是一個亟待解決的問題.

描述邏輯[4](Decription Logic,DL)是基于概念和角色(即類和屬性)的知識表示形式,是對概念化知識進行表示和推理的邏輯形式.傳統的DL能描述靜態結構知識,但不能表述動態的時序特征,將描述邏輯用時序算子對其進行擴展,可得到表示動態和時序語義的時序描述邏輯.

UML順序圖描述對象間的動態交互能力,體現對象間消息傳遞的時序特征,將時序描述邏輯應用于UML順序圖,為UML順序圖的形式化提供了更好的研究方法.不同學者研究了順序圖的多種形式化方法,文獻[5]給出了一種五元組SD=＜Obj,Msg,Loc,Evn,F>的順序圖的形式化定義及推理過程;文獻[6]給出了UML順序圖的一種符合BNF范式的形式化方法,并提出將順序圖轉化為Petri網模型的方法;文獻[7]給出了UML順序圖的形式化定義并從隊列的角度進行了其特性分析;文獻[8]對UML2.0順序圖的最大順序片段形式化,并應用交互操作符得到了順序圖的時序描述邏輯語義.本文在文獻[8]的基礎上增加了選擇交互和循環操作符并提出了UML順序圖六元組的形式化描述方法,通過時序描述邏輯的□、◇和○三種不同算子得到UML2.0順序圖的時序描述邏輯語義.

1 UML與DL

UML是面向對象的標準化建模語言,能描述靜態與動態的知識系統并對其建模.DL是基于對象的知識的形式化表示,具有很強的表達能力和可判定性,能保證推理算法的終止,并返回正確的結果.UML與DL的相同點為:二者都能描述靜態和動態領域的知識,但表現形式略有區別.UML的順序圖描述了對象之間的交互關系,反映交互過程中對象傳遞消息的時序關系;傳統的描述邏輯只能描述靜態領域的知識,而無法描述具有動態與時序特征的知識,在DL中增加動態算子可擴展成為動態描述邏輯,增加時態算子可擴展成為時態描述邏輯,擴展后,DL可表示具有動態與時序特征的知識.UML與DL的不同點為:UML是一種半形式化的語言,其圖形化的建模元素是非形式化的,不具備可判定推理能力;而DL是基于一階謂詞邏輯的完全形式化的語言,具有很強的表達和可判定推理能力.因此可以對描述邏輯進行時序擴展,然后用擴展后的時序描述邏輯對UML進行形式化,就可將二者的優勢有機地結合起來.

2 UML順序圖

UML的順序圖是一種詳細表示對象間以及對象與系統外部的參與者之間動態聯系的圖形文檔[9].順序圖表示了由時間安排的一系列消息,著重表示對象間消息傳遞的先后順序.每個分類角色顯示為一條生命線,代表整個交互期間上的角色.消息則顯示為生命線之間的箭頭.UML順序圖以二維圖表來顯示交互.縱向是時間軸,時間自上而下.橫向顯示單個對象的分類角色.每個對象用方框表示,對象的名字在方框內部,并在名字的下方加下劃線.每個分類角色表現為垂直列－生命線.在角色存在的時間內,生命線顯示為虛線;在角色的過程激活時間內,生命線顯示為雙線.消息顯示為從一個角色生命線出發至另一個角色生命線的箭頭,箭頭以時間順序在圖中從上到下排列.

在UML2.0中增加了交互片段的概念[10],片段是順序圖的局部內容,是順序圖中的一個分區域.交互片段包含一般交互片段和組合交互片段,組合片段的類型由交互操作符表示,包含表示選擇(alt)、引用(ref)、并發(par)、循環(loop)、可選(opt)、序列(seq)、暫停(break)、否定(neg)等.

UML2.0順序圖主要描述對象間消息傳遞的時間順序,它的基本動作是消息的發送和接收,圖1是C語言標準源程序的編輯、編譯、連接及執行過程的UML順序圖,該圖可看作由兩種基本動作(發送消息和接收消息)和循環及選擇等2種基本類型的組合片段組合而成.因此,在下文所定義的語法中只包含這兩種基本的交互操作符.

圖1 C語言程序執行過程的UML順序圖

3 UML2.0順序圖語法

定義1.最大順序片段是順序圖上的一個域[8],它包含一組連貫的消息序列和生命線,由內附于組合段的矩形和交互操作組成.

圖1中包括兩個最大順序片段,其一的主要操作符是循環(loop),是順序圖中的第一個消息到第一個組合片段上的一個片段,另一片段的主要操作符是選擇(alt),是順序圖中上一個組合的下邊界到順序圖最后一個消息的片段.這兩個最大順序片段是獨立的.

定義2.根據UML2.0的規范,UML2.0的順序圖可表示為一個六元組形式SD={Obj,Msg,Loc,Evn,F,InterOpr},其中,Obj為對象集合;Msg為消息集合;Loc=＜Obj,i>為位點的集合,位點是生命線上發送和接收消息的點,i是不同對象上的位點的集合;Evn為事件的集合,在對象的激活期內,事件可以產生消息;F:Msg×{s,r}→Loc為從消息到位點的一個函數關系;InterOpr是UML2.0順序圖上的交互操作符.

如圖1所示的C語言運行過程的順序圖六元組表示SD={Obj,Msg,Loc,Evn,F,InterOpr},則有:

Msg={M1,M2,M3,M4,M5,M6,M7,M8},可詳細地描述為Msg={(Edit Command,1),(Compile Command,2),(Syntax Error,3),(Link Command,4),(Link Error,5),(Run Command,6),(Error Result,7),(Correct Result,8)}

一個正確設計的順序圖應滿足以下幾點:① 順序圖能正常終止,即能夠到達終止狀態;② 順序圖中不能出現死鎖,即順序圖中存在死鎖狀態并且該狀態不是終止狀態;③ 順序圖的執行路徑滿足某些約束條件,如消息M2必須出現在消息M1之后.圖1按上述要求進行設計.

4 UML順序圖的時序描述邏輯語義

傳統的DL不能表示動態和時序的知識,采用時序算子對DL進行擴展,則能描述動態和時態的知識.文獻[8,11] 對描述邏輯作了簡單的時序擴展,這些時序描述邏輯提供了有限的表達能力,無法滿足UML順序圖的形式化需要.

時序描述邏輯(Temporal Description Logics,TDLs)也即“命題線性時態邏輯系統”(Proposition Linear Temporal Logic,PLTL)是非經典邏輯的分支學科,主要研究將含有時態動詞的語句形式化,并對其進行推理.時序邏輯主要有四個操作算子:□(always in the future),◇(eventually),〇(at the next moment)和μ(until).其中□、◇和〇(at the next moment)是一元操作算子,μ是二元操作算子.對描述邏輯的擴展主要體現在語法、語義及其定義上.本文重點考慮PLTL中的3個主要一元算子:□,◇和〇.

4.1 PLTL的形式化定義

在PLTL中定義如下:

(1)命題變元P是合式公式;

(2)若w、w1和w2是合式公式,則┐w、w1∧w2、w1∨w2、w1→w2、w1≡w2都是合式公式;□W、◇W、○W也都是合式公式;

(3)每個合式公式均可通過有限次應用(1)、(2)獲得.

PLTL中包含的公理和推理規則,具體為:

推理規則1(重言規則).若u是命題重言式(tautology),則├u.

推理規則2(假言推理規則).若├u→v且├u,則├v.

推理規則3(口引入規則).若├u,則├□u.

應用上述公理和推理規則,經過有窮步驟,可推導出一系列合式公式,即PLTL的定理.

在下文的描述中,主要以部分公理為例,而對于推理規則及其應用將是下一步研究的重點.

4.2 PLTL的語義描述

交互操作符將UML順序圖分成一個或多個最大順序片段,并對其分別定義PLTL語義,得到UML順序圖的時序描述邏輯語義.

定義3.順序圖SD中的一個最大順序片段的有序關系為Q,Q:Loc×Loc滿足:

(1)對于?Obj∈Loc,i∈Loc,有(Obj,i)→○?(Obj,i+1).

(2)對于?Msg,如果?(Obj,i),(Obj′,i′)∈Loc,((Obj,i)=F(Msg,s))∧((Obj′,i′)=F(Msg,r))則(Obj,i)→○?(Obj′,i′),表示消息接收總在消息發送之后.

(3)若(Obj,i)與(Obj′,i′)和(Obj1,i1)與(Obj′1,i′1)分別對應于消息的發送和接收點,當Obj=Obj1且(Obj,i)→○?(Obj1,i1),則(Obj′,i′)→○?(Obj1,i1).

(4)若(Obj,i),(Obj1,i1),(Obj2,i2),∈Loc,且(Obj,i)→○?(Obj1,i1)和(Obj1,i1)→○?(Obj2,i2),則(Obj,i)→○?(Obj2,i2).

定義4(交互操作符的PLTL語義).

(1)當InterOpr.type=alt時 :Msg→○?(M1∨M2∨···∨Mn),Msg→○?(M1∧M2∧···∧Mn),其中,Msg是alt的上一個最大順序片段,M1∨M2∨···∨Mn=True,M1∧M2∧···∧Mn=False,表示相應的條件有且僅有一個成立.

(2)當InterOpr.type=loop時:(≥m(Msg→Msg))∧(≤n(Msg→○?Msg)),其中,m,n表示循環的最大次數和最小次數.

本文中僅討論alt和loop交互操作符,故對其它交互操作符的PLTL語義未作描述.

5 實例分析

本節給出用PLTL描述圖1的結果,首先對圖1作補充說明:

圖1是C語言程序執行過程的順序圖,現對其執行過程闡述如下:C語言程序的執行過程從新建源程序開始,包括對源程序的修改,圖中由M1(Edit Command)實現,然后對源程序進行編譯,由M2(Compile Command)實現,在編譯過程中會進行語法檢測(Syntax Check),若出現語法錯誤M3(Syntax Error),則應重新編輯,并再次編譯,此過程可重復多次,圖中由loop順序片段實現,直到編譯成功生成目標程序,然后將目標程序進行連接,由M4(Link Command)實現,若出現連接錯誤M5(Link Error),則修改后重新連接,最終生成可執行文件,運行該文件,若無算法錯誤,則得到正確的結果(Correct Result),并回到最初的狀態進行下一算法,若出現算法錯誤,則得到錯誤的結果(Error Result),回到編輯狀態,繼續上述過程,圖中由alt順序片段實現.綜上,則圖1的時序描述邏輯語義示例為:

即:

通過對C語言程序執行過程的分析,說明從源程序的創建到最終程序的運行結果是可行的,轉換是正確的.

6 結論

本文結合UML順序圖的交互操作符,提出了一種基于時序描述邏輯六元組的形式化方法,通過時序描述邏輯的□、◇和○算子給出了UML順序圖的時序描述邏輯語義.對DL的時態擴展,既描述了領域的靜態知識,又能描述領域的時序關系,增強了其描述能力.相對于其他方法,時序描述邏輯具有完備、可判定的推理算法,為下一步建立自動推理技術提供了基礎.在本文的后續研究工作中,將進一步探討包含μ算子的UML 順序圖的形式化方法,對其推理規則作初步的研究,并進一步驗證其可行性.