陳慧峰　余曉菲　蔣建民

摘 要：UML（統(tǒng)一建模語言）活動(dòng)圖廣泛用于軟件開發(fā)過程，然而它是半形式化的模型，不能進(jìn)行推理，無法保證其正確性。為了保證它的正確性，必須先把它轉(zhuǎn)化為形式化模型再進(jìn)行檢測(cè)?，F(xiàn)有工作已將活動(dòng)圖轉(zhuǎn)換成變遷系統(tǒng)、進(jìn)程代數(shù)、Petri網(wǎng)等模型，需要增加或丟失大量信息。本文提出一種新的方法，該方法直接將活動(dòng)圖轉(zhuǎn)換成被稱為依賴結(jié)構(gòu)的形式化模型，不會(huì)增加或減少活動(dòng)圖的任何信息。基于依賴結(jié)構(gòu)模型我們首先討論了檢測(cè)活動(dòng)圖的正確性方法，然后介紹相應(yīng)的工具；最后用一個(gè)實(shí)例來詳細(xì)說明檢測(cè)過程。該工作有助于軟件工程師正確地使用UML活動(dòng)圖對(duì)軟件系統(tǒng)進(jìn)行分析和設(shè)計(jì)。

關(guān)鍵詞：活動(dòng)圖；形式化模型；正確性

中圖分類號(hào)：TP311.5 文獻(xiàn)標(biāo)識(shí)碼：A

Abstract：UML activity diagrams are widely used in the software development process.But since they are semi-formal models，we can neither reason nor guarantee their correctness.In order to ensure their correctness，they must be transformed into formal models and then can be detected.Existing work has transformed activity diagrams into formal models such as transition systems，process algebras and Petri nets.However，these models need to add or decrease a large amount of information.In this paper，a new method is proposed，which directly transforms activity diagrams into formal models called dependency structures without adding or decreasing any information.Based on the dependency structure models，we first present a method of checking the correctness of a UML activity diagram and then introduce a corresponding tool.Finally，an example was used to demonstrate the checking process in detail.This work is helpful for software engineers to properly use UML activity diagram to analyze and design software systems.

Keywords：activity diagram；formal models；correctness

1 引言（Introduction）

統(tǒng)一建模語言（UML）[1]是國(guó)際對(duì)象管理組織（OMG）認(rèn)可的面向?qū)ο筌浖臉?biāo)準(zhǔn)化建模語言。它具有簡(jiǎn)單、統(tǒng)一的特點(diǎn)，而且能表達(dá)軟件設(shè)計(jì)中的動(dòng)態(tài)和靜態(tài)信息，目前已成為軟件開發(fā)可視化領(lǐng)域建模語言的工業(yè)標(biāo)準(zhǔn)。在軟件系統(tǒng)的開發(fā)過程中，UML可以在軟件開發(fā)整個(gè)生命周期中使用。實(shí)踐證明，正確地使用UML可以幫助設(shè)計(jì)者縮短設(shè)計(jì)時(shí)間，減少開發(fā)成本。

UML活動(dòng)圖作為統(tǒng)一建模語言最重要的組成部分之一，它廣泛用于軟件系統(tǒng)的開發(fā)過程，它貫穿于需求分析到系統(tǒng)建成后測(cè)試的各個(gè)階段。當(dāng)前，在軟件開發(fā)過程中許多工程師不能規(guī)范使用活動(dòng)圖，這導(dǎo)致無法正確地進(jìn)行需求分析和設(shè)計(jì)，以致于整個(gè)軟件開發(fā)項(xiàng)目失敗，浪費(fèi)了大量的時(shí)間和金錢。因此需要規(guī)范、正確地使用UML活動(dòng)圖。

本文給出了UML活動(dòng)圖形式化定義，由此可以確定給定的UML活動(dòng)圖的規(guī)范性，并將活動(dòng)圖轉(zhuǎn)換為稱為“依賴結(jié)構(gòu)”的形式化模型，基于形式化模型可以檢測(cè)該活動(dòng)圖的正確性。在本文中，我們開發(fā)了一個(gè)原型工具，并用一個(gè)實(shí)例詳細(xì)演示了檢測(cè)活動(dòng)圖規(guī)范化和正確性的過程。

UML活動(dòng)圖形式化的定義一直以來是一個(gè)熱點(diǎn)問題，林添榮等[2]基于Hoare邏輯給出了UML活動(dòng)圖形式化定義，并根據(jù)此定義得出若干性質(zhì)。Trickvoic等[3]用Petri網(wǎng)作為UML活動(dòng)圖形式化語義并給出了UML活動(dòng)圖轉(zhuǎn)換為Petri網(wǎng)的規(guī)則。王聰?shù)萚4]給出的UML活動(dòng)圖操作語義是基于狀態(tài)變遷，處理起來相對(duì)復(fù)雜。朱雪陽等[5]根據(jù)UML活動(dòng)圖定義了一種稱為XYZ活動(dòng)圖的中間結(jié)構(gòu)，然后將XYZ映射為XYZ/E條件元。崔萌等[6]在UML活動(dòng)圖的基礎(chǔ)上加入了時(shí)間概念，然后定義了一種“實(shí)時(shí)”活動(dòng)圖。

由于UML活動(dòng)圖是半形式化的模型，我們不能直接推理和完成自動(dòng)分解。這就需要我們選擇合適的形式體系的活動(dòng)圖的語義模型。主流形式體系大致分為變遷系統(tǒng)[7，8]，進(jìn)程代數(shù)[9-12]和Petri網(wǎng)[13]等。變遷系統(tǒng)是一個(gè)基于自動(dòng)機(jī)的模型，包括狀態(tài)和轉(zhuǎn)換。這些變遷可以是活動(dòng)，動(dòng)作或事件。當(dāng)一個(gè)UML活動(dòng)圖被翻譯成一種變遷系統(tǒng)[14，15]，因?yàn)樵诨顒?dòng)圖中不存在狀態(tài)信息，我們需要增建狀態(tài)信息。同樣地，如果一個(gè)活動(dòng)圖被轉(zhuǎn)換成一個(gè)Petri網(wǎng)，在這樣的Petri網(wǎng)的地方也需要被附加地建立[16，17]。進(jìn)程代數(shù)是一個(gè)動(dòng)作/根據(jù)活動(dòng)積分。如果一個(gè)活動(dòng)圖映射到一個(gè)過程中，我們必須添加表達(dá)活動(dòng)圖[18，19]的同步控制同步事件名稱。此外，現(xiàn)有的一些努力，例如Daw[20]提出了活動(dòng)圖的操作語義。這樣的語義實(shí)際上是一種基于變遷系統(tǒng)的結(jié)構(gòu)操作語義。

我們采用依賴結(jié)構(gòu)作為形式化模型[21-23]，該模型是本文作者及團(tuán)隊(duì)成員耗費(fèi)近10年研究基于事件的形式化模型而開發(fā)出的新模型。該模型考慮到了簡(jiǎn)單、實(shí)用、輕量級(jí)，并參閱Petri網(wǎng)有的令牌機(jī)制，進(jìn)程代數(shù)的組合運(yùn)算操作。更重要的是活動(dòng)圖直接可以轉(zhuǎn)換成依賴結(jié)構(gòu)，無需增加或減少任何信息。

2 活動(dòng)圖形式化定義（Formal definition of activity diagram）

活動(dòng)圖是用來描述系統(tǒng)的動(dòng)作行為，我們能夠定義一個(gè)活動(dòng)圖的抽象語法。在這里，以表示A集合的基，定義為在A上的一個(gè)二元關(guān)系。下面我們給出活動(dòng)圖的定義

定義2.1：一個(gè)活動(dòng)圖是一個(gè)四元組，其中：

（1），這里，AN是活動(dòng)節(jié)點(diǎn)的集合，ON是對(duì)象節(jié)點(diǎn)的集合，，Ch是分支節(jié)點(diǎn)的集合，Me是合并節(jié)點(diǎn)的集合，F(xiàn)o是分叉節(jié)點(diǎn)的集合，Jo是匯合節(jié)點(diǎn)的集合；

（2）是節(jié)點(diǎn)間的關(guān)系；

（3）Ia是初始節(jié)點(diǎn)的集合；

（4）Fa是終止節(jié)點(diǎn)的集合。

為了正確使用活動(dòng)圖，必須對(duì)活動(dòng)圖進(jìn)行規(guī)范化處理。在UML活動(dòng)圖的規(guī)范[1]中，一個(gè)初始節(jié)點(diǎn)沒有輸入并只有一個(gè)輸出，活動(dòng)節(jié)點(diǎn)有一個(gè)輸入和一個(gè)輸出，分叉（Fork）有一個(gè)輸入和多個(gè)輸出，匯合（Join）有多個(gè)輸入和一個(gè)輸出，分支（Choice/Decision）有一個(gè)輸入和兩個(gè)或多個(gè)輸出，合并（Merge）有多個(gè)輸入和一個(gè)輸出，終止節(jié)點(diǎn)有一個(gè)輸入沒有輸出。表1提供UML活動(dòng)圖各類節(jié)點(diǎn)的入度和出度具體要求。

上面給出了活動(dòng)圖的形式化定義，基于定義2.1，我們可以定義節(jié)點(diǎn)的出度和入度。

定義2.2：設(shè)是一個(gè)活動(dòng)圖，設(shè)，，。和分別稱為的入度和出度。

有了一般活動(dòng)圖和它的節(jié)點(diǎn)的入、出度定義，我們就可以定義“規(guī)范的活動(dòng)圖”。

定義2.3：設(shè)是一個(gè)活動(dòng)圖，如果對(duì)任意滿足如下條件：

（1）若是活動(dòng)節(jié)點(diǎn)或?qū)ο蠊?jié)點(diǎn)，則并且；

（2）若是初始節(jié)點(diǎn)，則并且；

（3）若是終止節(jié)點(diǎn)，則并且；

（4）若是分叉節(jié)點(diǎn)，則并且，是有限正整數(shù)；

（5）若是匯合節(jié)點(diǎn)，則并且，是有限正整數(shù)；

（6）若是分支節(jié)點(diǎn)，則并且，是有限正整數(shù)；

（7）若是合并節(jié)點(diǎn)，則并且，是有限正整數(shù)。

我們稱G是一個(gè)規(guī)范的活動(dòng)圖。

命題2.1一個(gè)規(guī)范的活動(dòng)圖是一個(gè)活動(dòng)圖。

證明：根據(jù)定義2.1和定義2.2直接可得。

實(shí)際上，一個(gè)規(guī)范的活動(dòng)圖是一個(gè)特殊的活動(dòng)圖，它滿足一些規(guī)范化的條件。

從定義2.1可以看出，活動(dòng)圖實(shí)際上是一個(gè)有向圖，可以直接通過圖的遍歷算法，獲取每個(gè)節(jié)點(diǎn)的入度和出度，當(dāng)遍歷整個(gè)活動(dòng)圖時(shí)，可以判斷活動(dòng)圖節(jié)點(diǎn)的出度和入度是否滿足定義2.3。如果每個(gè)節(jié)點(diǎn)的入度和出度滿足定義2.3，則活動(dòng)圖是規(guī)范的；否則，該活動(dòng)圖是不規(guī)范的。

上述方法是從語法角度來判斷活動(dòng)圖的規(guī)范性，但更重要的是檢測(cè)活動(dòng)圖的正確性，即判斷是否死鎖，下面部分我們將討論將活動(dòng)圖轉(zhuǎn)換成形式化模型，并對(duì)活動(dòng)圖進(jìn)行正確性檢測(cè)。注意，我們可以將任何活動(dòng)圖（不一定是規(guī)范的活動(dòng)圖）轉(zhuǎn)換成形式化模型，并檢測(cè)它的正確性。

3 形式化模型（Formal models）

依賴結(jié)構(gòu)形式化模型包含四部分：轉(zhuǎn)換關(guān)系、同步關(guān)系、選擇（排斥或沖突）關(guān)系和優(yōu)先級(jí)關(guān)系。下面我們介紹該模型。

3.1 依賴結(jié)構(gòu)

為了方便敘述，本文首先給出一些輔助性的記法。假定E是事件的集合，表示集合E的冪集，而且令。一個(gè)“事件集”是指事件的集合，如果一個(gè)事件集中的所有事件都已經(jīng)出現(xiàn)，則稱該事件集是“可用的”，否則稱它是“不可用的”。

定義3.1：依賴結(jié)構(gòu)是一個(gè)七元組，其中：

（1）是非空的、有限的事件集合；

（2）是初始可用的事件節(jié)點(diǎn)的集合；

（3）是轉(zhuǎn)換關(guān)系；

（4）是同步關(guān)系，并且滿足：；

（5）是選擇關(guān)系，并且滿足：；

（6）是優(yōu)先級(jí)關(guān)系；

（7）是最后可用的事件集的集合。

一個(gè)轉(zhuǎn)換依賴（A，B）就是集合B中所有事件都依賴于集合A中所有的事件。一個(gè)集合時(shí)稱同步集；一個(gè)集合 時(shí)稱選擇集。任何一個(gè)同步集或者選擇集中至少有2個(gè)事件，同步關(guān)系不采用二元關(guān)系，目的是區(qū)分一個(gè)共享的同步的事件。例如，一個(gè)事件e分別和同步，但我們可以要求和這兩個(gè)事件不相互同步，也就是說同步關(guān)系不具傳遞性。因此，同步關(guān)系沒定義成在事件集上的對(duì)稱并傳遞的二元關(guān)系。選擇關(guān)系也需要去考慮類似情況。任意集合表示所有A集合中的事件都相互同步。只有當(dāng)A集合中所有的事件出現(xiàn)時(shí)，依賴于A中的所有事件才可能出現(xiàn)。任意集合表示B集合中的所有事件都相互排斥，也就是說，B集合中一個(gè)事件出現(xiàn)，則B集合中其他事件都不能出現(xiàn)。

優(yōu)先級(jí)依賴控制并發(fā)事件，也就是說這些事件相互獨(dú)立。初始可用的事件集即系統(tǒng)開始運(yùn)行之前可用的事件集。終止事件集是指在系統(tǒng)執(zhí)行過程中該事件集可用后，該系統(tǒng)或它的子系統(tǒng)就停止運(yùn)行的事件集。

這里，對(duì)于任意的集合，若則稱是一個(gè)轉(zhuǎn)換依賴，表示為，讀作“B依賴A”，并且A，B分為稱轉(zhuǎn)換依賴的前置事件集和后置事件集。對(duì)于任意的集合，若則稱是一個(gè)優(yōu)先級(jí)依賴，表示為。

一個(gè)依賴結(jié)構(gòu)能圖形化表示。如圖1所示，圖中一個(gè)事件集表示成一個(gè)集合，一個(gè)轉(zhuǎn)換依賴表示為從一個(gè)事件集指向另一個(gè)事件集的一個(gè)箭頭，優(yōu)先級(jí)依賴表示為終點(diǎn)帶圓圈的虛線。為了圖形化表示類似轉(zhuǎn)換依賴關(guān)系的同步關(guān)系，每一個(gè)同步的事件形成的集合和同步關(guān)系表示為一個(gè)事件集指向它的同步事件集的雙箭頭。選擇關(guān)系圖形化表示為一個(gè)選擇事件集指向可執(zhí)行的單個(gè)事件集的空心箭頭。

3.2 執(zhí)行語義

依賴結(jié)構(gòu)的執(zhí)行語義模擬了所建模系統(tǒng)的執(zhí)行過程。正如前文所述，在依賴結(jié)構(gòu)中的每一個(gè)轉(zhuǎn)換依賴（不包含優(yōu)先級(jí)依賴）對(duì)應(yīng)于一個(gè)活動(dòng)（操作或動(dòng)作），也就是一個(gè)執(zhí)行步驟。若一個(gè)轉(zhuǎn)換依賴的前置依賴集是可用的，則稱該轉(zhuǎn)換依賴是“已激活的”。只有已激活的轉(zhuǎn)換依賴才可能被執(zhí)行。為此，將計(jì)算過程中的當(dāng)前可用的事件集，以及當(dāng)前已激活的轉(zhuǎn)換依賴作為一個(gè)整體，稱為一個(gè)“狀態(tài)”。

定義3.2：設(shè)是一個(gè)依賴結(jié)構(gòu)，DS的一個(gè)狀態(tài)是一個(gè)二元組，其中，是可用事件集的集合，是已激活的轉(zhuǎn)換依賴的集合并滿足。DS的初始狀態(tài)為，這里，和。

這里定義了狀態(tài)，下面給出狀態(tài)演化規(guī)則。

定義3.3：設(shè)是一個(gè)依賴結(jié)構(gòu)，和是DS的兩個(gè)狀態(tài)。如果下列條件成立：

我們稱能夠通過執(zhí)行轉(zhuǎn)換依賴（A，B）演化成，表示為。

第一個(gè)條件要求當(dāng)前可執(zhí)行的轉(zhuǎn)換依賴（A，B）是當(dāng)前狀態(tài)下已激活的轉(zhuǎn)換依賴，第二個(gè)條件要求不存在一個(gè)事件比B中的事件優(yōu)先出現(xiàn)，第三個(gè)條件要求新狀態(tài)中已激活的轉(zhuǎn)換依賴包含后繼可激活的轉(zhuǎn)換依賴，最后一個(gè)條件要求是：如果存在一個(gè)已激活的轉(zhuǎn)換依賴它的前置依賴集是A，那么新狀態(tài)下仍然保留事件集A，否則移除事件集A，新的可用的事件必須添加到新的狀態(tài)中。

3.3 性質(zhì)

為了把依賴結(jié)構(gòu)用于分析系統(tǒng)的性質(zhì)和行為。本節(jié)先定義一些依賴結(jié)構(gòu)的性質(zhì)。

定義3.4：設(shè)是一個(gè)依賴結(jié)構(gòu)，并設(shè)是DS的初始狀態(tài)。

（1）如果在DS中存在一個(gè)狀態(tài)S，且存在一個(gè)狀態(tài)序列，使得，其中，則稱狀態(tài)S在DS中是可達(dá)的。如果在DS中存在兩個(gè)狀態(tài)S和并且存在狀態(tài)序列使得，其中，則稱狀態(tài)可達(dá)至狀態(tài)S，表示為。Sta（DS）表示DS中所有可達(dá)狀態(tài)的集合。

（2）設(shè)，如果并且，則稱S是終止的；如果S不是終止的并不存在一個(gè)狀態(tài)使得，則稱S是死的。如果任意狀態(tài)S是終止的或者存在一個(gè)終止?fàn)顟B(tài)，使得，則稱DS是弱終止的。如果使得S是死的，則稱DS是死鎖。如果不存在使得S是死的，則稱DS是無死鎖的。

作者所在研究小組已經(jīng)在文獻(xiàn)[21-23]中對(duì)系統(tǒng)中死鎖的存在與否進(jìn)行了研究，并提出了一個(gè)可達(dá)性算法用于檢測(cè)死鎖。

命題3.1設(shè)是一個(gè)依賴結(jié)構(gòu)。

（1）如果DS是弱終止，則稱DS是無死鎖的。

（2）如果并且，則稱S是死的。

證明：由定義4.4直接可得。

上述命題表明（1）一個(gè)無死鎖的系統(tǒng)比弱終止的系統(tǒng)是更一般的系統(tǒng)；（2）如果一個(gè)狀態(tài)已激活的轉(zhuǎn)換依賴集為空并且可用事件不都是終止事件，則該狀態(tài)是死的。

4 轉(zhuǎn)換規(guī)則（Transformation rules）

這里我們列出了活動(dòng)圖轉(zhuǎn)換為依賴結(jié)構(gòu)的具體規(guī)則，如圖1所示。一個(gè)活動(dòng)看成一個(gè)事件，一個(gè)活動(dòng)節(jié)點(diǎn)看成一個(gè)事件集，下面給出六個(gè)轉(zhuǎn)換規(guī)則。

（1） 一個(gè)活動(dòng)節(jié)點(diǎn)與另一個(gè)活動(dòng)節(jié)點(diǎn)通過一個(gè)帶箭頭的線（活動(dòng)邊）連在一起（如圖1（1）所示），該帶箭頭的線對(duì)應(yīng)著一個(gè)轉(zhuǎn)換依賴，如圖1（）所示。

（2）一個(gè)活動(dòng)節(jié)點(diǎn)通過一個(gè)菱形分支到兩個(gè)活動(dòng)節(jié)點(diǎn)，如圖1（2）所示，該菱形的分支結(jié)構(gòu)對(duì)應(yīng)著一個(gè)選擇依賴，如圖1（）所示。

（3）一個(gè)活動(dòng)節(jié)點(diǎn)通過一條粗橫線分叉成兩個(gè)活動(dòng)節(jié)點(diǎn)，如圖1（3）所示，該粗橫線的分叉結(jié)構(gòu)對(duì)應(yīng)著兩個(gè)轉(zhuǎn)換依賴，這兩個(gè)轉(zhuǎn)換依賴有相同的前置集，如圖1（）所示。

（4）兩個(gè)活動(dòng)節(jié)點(diǎn)通過一條粗線匯合到一個(gè)活動(dòng)節(jié)點(diǎn)，如圖1（4）所示，該粗線的匯合結(jié)構(gòu)對(duì)應(yīng)著一個(gè)同步依賴，如圖1（）所示。

（5）兩個(gè)活動(dòng)節(jié)點(diǎn)通過一個(gè)菱形合并成一個(gè)活動(dòng)節(jié)點(diǎn)，如圖1（5）所示，該菱形的合并結(jié)構(gòu)的對(duì)應(yīng)著兩個(gè)有相同后置集的轉(zhuǎn)換依賴，如圖1（）所示。

（6）初始節(jié)點(diǎn)和終止節(jié)點(diǎn)只是起一個(gè)控制作用，在這里當(dāng)作特殊點(diǎn)不用進(jìn)行轉(zhuǎn)換，但初始節(jié)點(diǎn)的后置節(jié)點(diǎn)轉(zhuǎn)換為依賴結(jié)構(gòu)圖中的初始節(jié)點(diǎn)，終止節(jié)點(diǎn)的前置節(jié)點(diǎn)轉(zhuǎn)換為依賴結(jié)構(gòu)圖中的終止節(jié)點(diǎn)。

命題 4.1設(shè)是一個(gè)規(guī)范的活動(dòng)圖，并假定通過上述轉(zhuǎn)換規(guī)則得到依賴結(jié)構(gòu)，則下面結(jié)論成立。

（1）若a在G中是活動(dòng)節(jié)點(diǎn)或?qū)ο蠊?jié)點(diǎn)，則；

（2）若a在G中是初始節(jié)點(diǎn)并且，則；

（3）若b在G中是終止節(jié)點(diǎn)并且，則；

（4）若a在G中是分叉節(jié)點(diǎn)，則；

（5）若a在G中是匯合節(jié)點(diǎn)，則存在一個(gè)同步集；

（6）若a在G中是分支節(jié)點(diǎn)，則存在一個(gè)同步集；

（7）若a在G中是合并節(jié)點(diǎn)，則。

證明：（1）因?yàn)橐粋€(gè)活動(dòng)看成一個(gè)事件，一個(gè)活動(dòng)節(jié)點(diǎn)看成一個(gè)事件集，所以（1）正確。（2）由轉(zhuǎn)換規(guī)則（6）可得，初始節(jié)點(diǎn)并沒有進(jìn)行轉(zhuǎn)換，但它的后繼節(jié)點(diǎn)對(duì)應(yīng)著依賴結(jié)構(gòu)圖中的初始節(jié)點(diǎn)，因此該結(jié)論正確。（3）由轉(zhuǎn)換規(guī)則（6）可得，終止節(jié)點(diǎn)并沒有進(jìn)行轉(zhuǎn)換，但它的前置節(jié)點(diǎn)對(duì)應(yīng)著依賴結(jié)構(gòu)圖中的終止節(jié)點(diǎn)，因此（3）正確。（4）通過轉(zhuǎn)換規(guī)則（3）可得，若a在G中是分叉節(jié)點(diǎn)，它只是起控制作用，并不屬于 ，因此（4）正確。（5）通過轉(zhuǎn)換規(guī)則（4）可得，若a在G中是匯合節(jié)點(diǎn)，正好對(duì)應(yīng)著一個(gè)同步依賴，因此（5）正確。（6）通過轉(zhuǎn)換規(guī)則（2）可得，若a在G中是分支節(jié)點(diǎn)，正好對(duì)應(yīng)著一個(gè)選擇依賴，因此該結(jié)論正確。（7）通過轉(zhuǎn)換規(guī)則（5）可得，若a在G中是合并節(jié)點(diǎn)，它起的是控制兩個(gè)或多個(gè)活動(dòng)合并，則它不是一個(gè)活動(dòng)。

5 工具及實(shí)例研究（Tool and case study）

我們的工具DS Tool是在開源圖形軟件JFDraw的基礎(chǔ)上建立起來的，JFDraw是基于Java開發(fā)的矢量圖形軟件，擁有標(biāo)準(zhǔn)的矢量圖形（矩形、直線、圓、弧、曲線），支持多種文件格式 （XML、JPG、PNG）。DS Tool將JFDraw的繪圖功能修改成可以直接畫UML活動(dòng)圖和依賴結(jié)構(gòu)圖，并以XML文件保存節(jié)點(diǎn)和圖形信息。通過第4節(jié)的轉(zhuǎn)換規(guī)則，可以將UML活動(dòng)圖轉(zhuǎn)換成依賴結(jié)構(gòu)模型，然后通過依賴結(jié)構(gòu)的可達(dá)性算法，判斷依賴結(jié)構(gòu)是否存在死鎖，從而確定活動(dòng)圖的正確性。

這里討論一個(gè)實(shí)際應(yīng)用的例子，通過該實(shí)例來演示如何使用我們的工具來判斷活動(dòng)圖的正確性。圖2是某公司的付款業(yè)務(wù)的活動(dòng)圖實(shí)例，從付款請(qǐng)求開始，可選擇美元或者澳元。若選擇美元，則需要財(cái)務(wù)總監(jiān)批準(zhǔn)，當(dāng)財(cái)務(wù)總監(jiān)批準(zhǔn)，則準(zhǔn)備支票并由財(cái)務(wù)總監(jiān)簽名，否則拒絕請(qǐng)求。若選擇澳元，就直接準(zhǔn)備支票，然后財(cái)務(wù)總監(jiān)簽名并更新賬戶數(shù)據(jù)庫，最后開支票。無論哪種付款方式都將生成付款文件。

為了簡(jiǎn)化問題，將圖2的活動(dòng)圖的活動(dòng)用字母代替，在表2中給出了所有活動(dòng)對(duì)應(yīng)的字母。通過表2轉(zhuǎn)換后得到圖3所示的依賴結(jié)構(gòu)圖。利用我們工具中對(duì)依賴結(jié)構(gòu)的可達(dá)性算法可以計(jì)算出在d和g同步過程出現(xiàn)死鎖，即財(cái)務(wù)總監(jiān)簽名后，并沒有更新賬戶數(shù)據(jù)庫，如圖4所示。

我們的工具對(duì)實(shí)例的活動(dòng)圖處理后生成13種狀態(tài)，發(fā)現(xiàn)在第9個(gè)狀態(tài)即 執(zhí)行完后出現(xiàn)死鎖。

6 結(jié)論（Conclusion）

本文首先給出了UML活動(dòng)圖形式化的定義，在此基礎(chǔ)上再用算法對(duì)UML活動(dòng)圖進(jìn)行正確性檢測(cè)，然后將UML活動(dòng)圖轉(zhuǎn)換為形式化模型依賴結(jié)構(gòu)，并給出了依賴結(jié)構(gòu)的執(zhí)行語義、相關(guān)性質(zhì)和活動(dòng)圖轉(zhuǎn)換為依賴結(jié)構(gòu)的規(guī)則，基于依賴結(jié)構(gòu)檢測(cè)UML活動(dòng)圖的正確性，最后通過我們的工具演示某公司的付款業(yè)務(wù)的活動(dòng)圖實(shí)例來判斷活動(dòng)圖的正確性。該工具有助于工程師和軟件開發(fā)初學(xué)者正確畫UML活動(dòng)圖，在將來的工作中我們將進(jìn)一步完善該工具，使其成為真正的CASE工具。

參考文獻(xiàn)（References）

[1] Object Management Group.Unified Modeling Language Specification v2.2[EB/OL].http：//www.omg.org/spec/UML/2.2，2009-02-01.

[2] 林添榮，蔣建民.活動(dòng)圖的一種邏輯語義[J].福建師范大學(xué)學(xué)報(bào)，2010，26（3）：26-30.

[3] Trickvoic I.Formalizing activity diagram of UML by Petri nets[J].Journal of Mathematics，2000：30.

[4] 朱雪陽，唐稚松.UML活動(dòng)圖的時(shí)序邏輯語義[J].計(jì)算機(jī)研究與發(fā)展，2005，42（9）：1478- 1484.

[5] 王聰，王智學(xué).UML活動(dòng)圖的操作語義[J].計(jì)算機(jī)研究與發(fā)展，2007，44（10）：1801-1807.

[6] 崔萌，李宣東.UML實(shí)時(shí)活動(dòng)圖的形式化分析[J].計(jì)算機(jī)學(xué)報(bào)，2004，27（3）：339-346.

[7] O.Marchal，P.Poizat， J.C.Royer.Checking Asynchronously Communicating Components Using Symbolic Transition Systems[J].CoopIS/DOA/ODBASE，2004（2）：1502-1519.

[8] M.Nielsen，G.Rozenberg，P.S.Thiagarajan，Elementary transition systems[J].Theoretical. Computer.Sci.，1992，96（1）：3-33.

[9] T. Bolognesi，E.Brinksma.Introduction to the ISO specification language LOTOS[J].Computer Networks and ISDN Systems，1987，14（1）：25-59.

[10] C.A.R.Hoare.Communicating Sequential Processes[J].Prentice-Hall，1978，21（8）：666-677.

[11] R.Milner，J.Parrow，D.Walker.A calculus of mobile processes[J].Information and Computation，1993，100：1-77.

[12] R.Milner.A Calculus of Communicating Systems[J].LNCS 92，Springer Verlag，1980，147：11-26.

[13] T.Murata.Petri Nets：properties，pnalysis，and applications[J].Proceedings of the IEEE，1989，77（4）：541-580.

[14] R.Eshuis，R.Wieringa.Tool support for verifying UML activity diagrams[J].IEEE Trans. Soft.Eng.，2004，30（7）：437-447.

[15] R.Eshuis.Symbolic model checking of UML activity diagrams[J].ACM Trans.on Soft.Eng. and Meth.，2006，15（1）：1-38.

[16] T.Staines.Intuitive mapping of uml 2 activity diagrams into fundamental modeling concept petri net diagrams and colored petri nets[J].ECBS，2008：191-200.

[17] H.St¨orrle.Structured nodes in uml 2.0 activities[J].Nordic Journal of Computing，2004，11（3）：279-302.

[18] I.Abdelhalim，S.Schneider，H.Treharne.An optimization approach for effective formalized UML model checking[J].SEFM，2012：248-262.

[19] J.K¨uster.A Classification of UML2 Activity Diagrams[J].Technical report，IBM ZRL Technical Report，2006：3673.

[20] Z.Daw，R.Cleavel.An extensible operational semantics for UML activity diagrams[J].SEFM，2015：360-368.

[21] Huifeng Chen，Jianmin Jiang，Zhong Hong，et al.Decomposition of UML activity diagrams[J].Software：Practice and Experience，2018，48（1）：105-122.

[22] Jian-Min Jiang，Huibiao Zhu，Qin Li，et al.Event-based mobility modeling and analysis[J].ACM Transactions on Cyber-Physical Systems，2017，1（2）：1-32.

[23] Jian-Min Jiang，Zhu，Huibiao，et al.Analyzing Event-Based Scheduling in Concurrent Reactive Systems[J].ACM Transactions on Embedded Computing Systems，2015，14（4）：1-27.

作者簡(jiǎn)介：

陳慧峰（1992-），男，碩士生.研究領(lǐng)域：形式化方法.

余曉菲（1993-），女，碩士生.研究領(lǐng)域：形式化方法.

蔣建民（1972-），男，博士，教授.研究領(lǐng)域：形式化方法.