UML活動圖的正確性檢測

陳慧峰　余曉菲　蔣建民

摘 要：UML（統一建模語言）活動圖廣泛用于軟件開發過程，然而它是半形式化的模型，不能進行推理，無法保證其正確性。為了保證它的正確性，必須先把它轉化為形式化模型再進行檢測?，F有工作已將活動圖轉換成變遷系統、進程代數、Petri網等模型，需要增加或丟失大量信息。本文提出一種新的方法，該方法直接將活動圖轉換成被稱為依賴結構的形式化模型，不會增加或減少活動圖的任何信息?；谝蕾嚱Y構模型我們首先討論了檢測活動圖的正確性方法，然后介紹相應的工具；最后用一個實例來詳細說明檢測過程。該工作有助于軟件工程師正確地使用UML活動圖對軟件系統進行分析和設計。

關鍵詞：活動圖；形式化模型；正確性

中圖分類號：TP311.5 文獻標識碼：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）

統一建模語言（UML）[1]是國際對象管理組織（OMG）認可的面向對象軟件的標準化建模語言。它具有簡單、統一的特點，而且能表達軟件設計中的動態和靜態信息，目前已成為軟件開發可視化領域建模語言的工業標準。在軟件系統的開發過程中，UML可以在軟件開發整個生命周期中使用。實踐證明，正確地使用UML可以幫助設計者縮短設計時間，減少開發成本。

UML活動圖作為統一建模語言最重要的組成部分之一，它廣泛用于軟件系統的開發過程，它貫穿于需求分析到系統建成后測試的各個階段。當前，在軟件開發過程中許多工程師不能規范使用活動圖，這導致無法正確地進行需求分析和設計，以致于整個軟件開發項目失敗，浪費了大量的時間和金錢。因此需要規范、正確地使用UML活動圖。

本文給出了UML活動圖形式化定義，由此可以確定給定的UML活動圖的規范性，并將活動圖轉換為稱為“依賴結構”的形式化模型，基于形式化模型可以檢測該活動圖的正確性。在本文中，我們開發了一個原型工具，并用一個實例詳細演示了檢測活動圖規范化和正確性的過程。

UML活動圖形式化的定義一直以來是一個熱點問題，林添榮等[2]基于Hoare邏輯給出了UML活動圖形式化定義，并根據此定義得出若干性質。Trickvoic等[3]用Petri網作為UML活動圖形式化語義并給出了UML活動圖轉換為Petri網的規則。王聰等[4]給出的UML活動圖操作語義是基于狀態變遷，處理起來相對復雜。朱雪陽等[5]根據UML活動圖定義了一種稱為XYZ活動圖的中間結構，然后將XYZ映射為XYZ/E條件元。崔萌等[6]在UML活動圖的基礎上加入了時間概念，然后定義了一種“實時”活動圖。

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

我們采用依賴結構作為形式化模型[21-23]，該模型是本文作者及團隊成員耗費近10年研究基于事件的形式化模型而開發出的新模型。該模型考慮到了簡單、實用、輕量級，并參閱Petri網有的令牌機制，進程代數的組合運算操作。更重要的是活動圖直接可以轉換成依賴結構，無需增加或減少任何信息。

2 活動圖形式化定義（Formal definition of activity diagram）

活動圖是用來描述系統的動作行為，我們能夠定義一個活動圖的抽象語法。在這里，以表示A集合的基，定義為在A上的一個二元關系。下面我們給出活動圖的定義

定義2.1：一個活動圖是一個四元組，其中：

（1），這里，AN是活動節點的集合，ON是對象節點的集合，，Ch是分支節點的集合，Me是合并節點的集合，Fo是分叉節點的集合，Jo是匯合節點的集合；

（2）是節點間的關系；

（3）Ia是初始節點的集合；

（4）Fa是終止節點的集合。

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

上面給出了活動圖的形式化定義，基于定義2.1，我們可以定義節點的出度和入度。

定義2.2：設是一個活動圖，設，，。和分別稱為的入度和出度。

有了一般活動圖和它的節點的入、出度定義，我們就可以定義“規范的活動圖”。

定義2.3：設是一個活動圖，如果對任意滿足如下條件：

（1）若是活動節點或對象節點，則并且；

（2）若是初始節點，則并且；

（3）若是終止節點，則并且；

（4）若是分叉節點，則并且，是有限正整數；

（5）若是匯合節點，則并且，是有限正整數；

（6）若是分支節點，則并且，是有限正整數；

（7）若是合并節點，則并且，是有限正整數。

我們稱G是一個規范的活動圖。

命題2.1一個規范的活動圖是一個活動圖。

證明：根據定義2.1和定義2.2直接可得。

實際上，一個規范的活動圖是一個特殊的活動圖，它滿足一些規范化的條件。

從定義2.1可以看出，活動圖實際上是一個有向圖，可以直接通過圖的遍歷算法，獲取每個節點的入度和出度，當遍歷整個活動圖時，可以判斷活動圖節點的出度和入度是否滿足定義2.3。如果每個節點的入度和出度滿足定義2.3，則活動圖是規范的；否則，該活動圖是不規范的。

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

3 形式化模型（Formal models）

依賴結構形式化模型包含四部分：轉換關系、同步關系、選擇（排斥或沖突）關系和優先級關系。下面我們介紹該模型。

3.1 依賴結構

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

定義3.1：依賴結構是一個七元組，其中：

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

（2）是初始可用的事件節點的集合；

（3）是轉換關系；

（4）是同步關系，并且滿足：；

（5）是選擇關系，并且滿足：；

（6）是優先級關系；

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

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

優先級依賴控制并發事件，也就是說這些事件相互獨立。初始可用的事件集即系統開始運行之前可用的事件集。終止事件集是指在系統執行過程中該事件集可用后，該系統或它的子系統就停止運行的事件集。

這里，對于任意的集合，若則稱是一個轉換依賴，表示為，讀作“B依賴A”，并且A，B分為稱轉換依賴的前置事件集和后置事件集。對于任意的集合，若則稱是一個優先級依賴，表示為。

一個依賴結構能圖形化表示。如圖1所示，圖中一個事件集表示成一個集合，一個轉換依賴表示為從一個事件集指向另一個事件集的一個箭頭，優先級依賴表示為終點帶圓圈的虛線。為了圖形化表示類似轉換依賴關系的同步關系，每一個同步的事件形成的集合和同步關系表示為一個事件集指向它的同步事件集的雙箭頭。選擇關系圖形化表示為一個選擇事件集指向可執行的單個事件集的空心箭頭。

3.2 執行語義

依賴結構的執行語義模擬了所建模系統的執行過程。正如前文所述，在依賴結構中的每一個轉換依賴（不包含優先級依賴）對應于一個活動（操作或動作），也就是一個執行步驟。若一個轉換依賴的前置依賴集是可用的，則稱該轉換依賴是“已激活的”。只有已激活的轉換依賴才可能被執行。為此，將計算過程中的當前可用的事件集，以及當前已激活的轉換依賴作為一個整體，稱為一個“狀態”。

定義3.2：設是一個依賴結構，DS的一個狀態是一個二元組，其中，是可用事件集的集合，是已激活的轉換依賴的集合并滿足。DS的初始狀態為，這里，和。

這里定義了狀態，下面給出狀態演化規則。

定義3.3：設是一個依賴結構，和是DS的兩個狀態。如果下列條件成立：

我們稱能夠通過執行轉換依賴（A，B）演化成，表示為。

第一個條件要求當前可執行的轉換依賴（A，B）是當前狀態下已激活的轉換依賴，第二個條件要求不存在一個事件比B中的事件優先出現，第三個條件要求新狀態中已激活的轉換依賴包含后繼可激活的轉換依賴，最后一個條件要求是：如果存在一個已激活的轉換依賴它的前置依賴集是A，那么新狀態下仍然保留事件集A，否則移除事件集A，新的可用的事件必須添加到新的狀態中。

3.3 性質

為了把依賴結構用于分析系統的性質和行為。本節先定義一些依賴結構的性質。

定義3.4：設是一個依賴結構，并設是DS的初始狀態。

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

（2）設，如果并且，則稱S是終止的；如果S不是終止的并不存在一個狀態使得，則稱S是死的。如果任意狀態S是終止的或者存在一個終止狀態，使得，則稱DS是弱終止的。如果使得S是死的，則稱DS是死鎖。如果不存在使得S是死的，則稱DS是無死鎖的。

作者所在研究小組已經在文獻[21-23]中對系統中死鎖的存在與否進行了研究，并提出了一個可達性算法用于檢測死鎖。

命題3.1設是一個依賴結構。

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

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

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

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

4 轉換規則（Transformation rules）

這里我們列出了活動圖轉換為依賴結構的具體規則，如圖1所示。一個活動看成一個事件，一個活動節點看成一個事件集，下面給出六個轉換規則。

（1） 一個活動節點與另一個活動節點通過一個帶箭頭的線（活動邊）連在一起（如圖1（1）所示），該帶箭頭的線對應著一個轉換依賴，如圖1（）所示。

（2）一個活動節點通過一個菱形分支到兩個活動節點，如圖1（2）所示，該菱形的分支結構對應著一個選擇依賴，如圖1（）所示。

（3）一個活動節點通過一條粗橫線分叉成兩個活動節點，如圖1（3）所示，該粗橫線的分叉結構對應著兩個轉換依賴，這兩個轉換依賴有相同的前置集，如圖1（）所示。

（4）兩個活動節點通過一條粗線匯合到一個活動節點，如圖1（4）所示，該粗線的匯合結構對應著一個同步依賴，如圖1（）所示。

（5）兩個活動節點通過一個菱形合并成一個活動節點，如圖1（5）所示，該菱形的合并結構的對應著兩個有相同后置集的轉換依賴，如圖1（）所示。

（6）初始節點和終止節點只是起一個控制作用，在這里當作特殊點不用進行轉換，但初始節點的后置節點轉換為依賴結構圖中的初始節點，終止節點的前置節點轉換為依賴結構圖中的終止節點。

命題 4.1設是一個規范的活動圖，并假定通過上述轉換規則得到依賴結構，則下面結論成立。

（1）若a在G中是活動節點或對象節點，則；

（2）若a在G中是初始節點并且，則；

（3）若b在G中是終止節點并且，則；

（4）若a在G中是分叉節點，則；

（5）若a在G中是匯合節點，則存在一個同步集；

（6）若a在G中是分支節點，則存在一個同步集；

（7）若a在G中是合并節點，則。

證明：（1）因為一個活動看成一個事件，一個活動節點看成一個事件集，所以（1）正確。（2）由轉換規則（6）可得，初始節點并沒有進行轉換，但它的后繼節點對應著依賴結構圖中的初始節點，因此該結論正確。（3）由轉換規則（6）可得，終止節點并沒有進行轉換，但它的前置節點對應著依賴結構圖中的終止節點，因此（3）正確。（4）通過轉換規則（3）可得，若a在G中是分叉節點，它只是起控制作用，并不屬于 ，因此（4）正確。（5）通過轉換規則（4）可得，若a在G中是匯合節點，正好對應著一個同步依賴，因此（5）正確。（6）通過轉換規則（2）可得，若a在G中是分支節點，正好對應著一個選擇依賴，因此該結論正確。（7）通過轉換規則（5）可得，若a在G中是合并節點，它起的是控制兩個或多個活動合并，則它不是一個活動。

5 工具及實例研究（Tool and case study）

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

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

為了簡化問題，將圖2的活動圖的活動用字母代替，在表2中給出了所有活動對應的字母。通過表2轉換后得到圖3所示的依賴結構圖。利用我們工具中對依賴結構的可達性算法可以計算出在d和g同步過程出現死鎖，即財務總監簽名后，并沒有更新賬戶數據庫，如圖4所示。

我們的工具對實例的活動圖處理后生成13種狀態，發現在第9個狀態即 執行完后出現死鎖。

6 結論（Conclusion）

本文首先給出了UML活動圖形式化的定義，在此基礎上再用算法對UML活動圖進行正確性檢測，然后將UML活動圖轉換為形式化模型依賴結構，并給出了依賴結構的執行語義、相關性質和活動圖轉換為依賴結構的規則，基于依賴結構檢測UML活動圖的正確性，最后通過我們的工具演示某公司的付款業務的活動圖實例來判斷活動圖的正確性。該工具有助于工程師和軟件開發初學者正確畫UML活動圖，在將來的工作中我們將進一步完善該工具，使其成為真正的CASE工具。

參考文獻（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] 林添榮，蔣建民.活動圖的一種邏輯語義[J].福建師范大學學報，2010，26（3）：26-30.

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

[4] 朱雪陽，唐稚松.UML活動圖的時序邏輯語義[J].計算機研究與發展，2005，42（9）：1478- 1484.

[5] 王聰，王智學.UML活動圖的操作語義[J].計算機研究與發展，2007，44（10）：1801-1807.

[6] 崔萌，李宣東.UML實時活動圖的形式化分析[J].計算機學報，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.

作者簡介：

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

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

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