馬 莉，鐘 勇，霍穎瑜

(佛山科學(xué)技術(shù)學(xué)院電子與信息工程學(xué)院，廣東 佛山 528000)

1 概述

隨著軟件系統(tǒng)的復(fù)雜度提高，其開發(fā)和可靠性維護(hù)也越來越困難，據(jù)統(tǒng)計，在項目開發(fā)過程中大約有80%的時間都用來修改那些在項目開發(fā)早期所沒有被發(fā)現(xiàn)的錯誤，其中有56%的錯誤原因可以追溯到較差的需求規(guī)格說明［1］。因此，采用嚴(yán)格數(shù)學(xué)方法來產(chǎn)生精確無歧義規(guī)格說明的形式化方法受到重視。形式化規(guī)格說明是形式化方法中一個重要的研究內(nèi)容，它是對系統(tǒng)做什么的數(shù)學(xué)描述，是用具有精確語義的形式化規(guī)格說明語言書寫的系統(tǒng)功能和性質(zhì)的描述。

實時系統(tǒng)是指計算的正確性不僅取決于結(jié)果邏輯的正確性，而且取決于結(jié)果產(chǎn)生的時間。實時系統(tǒng)包括嚴(yán)格實時系統(tǒng)(硬實時系統(tǒng))和非嚴(yán)格實時系統(tǒng)(軟實時系統(tǒng))2 類。嚴(yán)格實時系統(tǒng)指任務(wù)錯過截止期限會造成嚴(yán)重后果，甚至系統(tǒng)崩潰［2］，如工業(yè)控制系統(tǒng)是具有硬實時要求的系統(tǒng)。非嚴(yán)格實時系統(tǒng)指任務(wù)截止期限并非完全不能錯過，但可能會造成一定的后果，如系統(tǒng)性能的下降［3］，或需要系統(tǒng)有一定的彌補行為，如推遲截止期限、承擔(dān)某種責(zé)任等。

現(xiàn)有實時技術(shù)研究多集中在嚴(yán)格實時系統(tǒng)方面，如采用Object-Z 及其擴展語言來描述嚴(yán)格實時系統(tǒng)并形式化驗證系統(tǒng)對時間要求的可滿足性［4-5］，使用在UML 順序圖添加時間約束的方法進(jìn)行各種實時性質(zhì)的自動驗證［6-7］。文獻(xiàn)［8］基于時間自動機理論和模型檢測工具UPPAAL 實現(xiàn)了復(fù)雜信息系統(tǒng)實時性能的自動分析與驗證，來彌補事件順序分析方法難以模擬系統(tǒng)實時行為過程的不足。文獻(xiàn)［9］引入時間約束，提出使用TPN 網(wǎng)模型的沖撞檢測和消解方法。這使得在實時系統(tǒng)建模時可以檢查并消除模型中存在的沖撞錯誤。文獻(xiàn)［10］提出一種實時構(gòu)件的模型。通過引入動作的定義對構(gòu)件的交互行為建模，用時鐘約束表示構(gòu)件交互行為的時間約束信息來進(jìn)行實時系統(tǒng)形式化建模。文獻(xiàn)［11］使用UML 對實時系統(tǒng)進(jìn)行分析，上述對實時系統(tǒng)的形式化研究均假定時間限制是嚴(yán)格的，不能延緩和替代的。文獻(xiàn)［12］提出一種基于對象的分布式實時系統(tǒng)調(diào)度模型的形式化分析?，F(xiàn)有研究對非嚴(yán)格實時系統(tǒng)時間限制在一定條件下的可延緩性、可替代性以及實時行為的可補償性則缺乏研究，也缺乏對非嚴(yán)格實時系統(tǒng)的描述能力，如對實時行為的可補償性，Object-Z 及其擴展語言則難以描述。

DTL-real-time Object-Z (Distributed Temporal Logic Based Real-time Object-Z，DRTOZ)語言是針對現(xiàn)有形式化方法難以描述實時行為的可補償性以及執(zhí)行的周期性等時態(tài)因素提出的形式化規(guī)格說明語言。該語言使用分布式時態(tài)操作符和操作謂詞擴展了Object-Z 歷史不變式的語義。

本文采用該擴展的Object-Z 歷史不變式來表達(dá)非嚴(yán)格實時系統(tǒng)的責(zé)任策略，以會議系統(tǒng)為例，說明了非嚴(yán)格實時系統(tǒng)中缺省策略、補償策略以及其他非嚴(yán)格實時策略的形式化規(guī)格說明，最后給出了該會議系統(tǒng)的形式化規(guī)格，說明了該方法的可應(yīng)用性。

2 DTL-real-time Object-Z 語言

Object-Z 是形式化規(guī)格說明語言Z 的面向?qū)ο髷U展，能描述復(fù)雜的數(shù)據(jù)結(jié)構(gòu)，但不能描述時間約束和連續(xù)變量，因而現(xiàn)有研究多通過增加時態(tài)邏輯或集成其他符號和概念的方法來增加Object-Z 的時態(tài)描述能力。Real-time Object-Z［4］是Object -Z 的實時擴展語言，它將Object-Z 與實時精化演算結(jié)合，不僅可以描述系統(tǒng)復(fù)雜的數(shù)據(jù)結(jié)構(gòu)，還可以描述系統(tǒng)所需的時間約束。但針對復(fù)雜的非嚴(yán)格實時系統(tǒng)，Real-time Object-Z 表達(dá)力有限，如時態(tài)行為的周期性執(zhí)行、特定時間的觸發(fā)行為、實時行為違反后的補償行為等，實時精化演算算子缺乏該種表達(dá)能力，DTL-real-time Object-Z 語言通過下列方法，能完整地描述非嚴(yán)格實時行為的時態(tài)驅(qū)動、事件驅(qū)動和行為補償?shù)纫蛩?

(1)通過集成分布式時態(tài)邏輯，能完整地表達(dá)操作和狀態(tài)變化的時態(tài)因素，如在特定時間之后執(zhí)行、按某種周期執(zhí)行。

(2)通過引入操作的begin 和end 謂詞來表達(dá)事件驅(qū)動因素。

(3)通過引入二元操作符or else 描述操作補償概念。

Object-z 擴充語法的BNF 范式如下所示:

其中，一元操作符X(next)和G(always)，二元操作符∪(weak until)是分布式時態(tài)邏輯(DTL)的未來時態(tài)操作符;DTL 的過去時態(tài)操作符包括一元操作符Y(previous)，P(sometime in the past)和H(always in the past)，二元操作符S(since)。另外，Xn代表n 個重復(fù)的應(yīng)用X，定義作為上述范式的簡寫。

操作謂詞enabled，occurs，begin，end，or else 與時態(tài)操作符結(jié)合用來確定操作執(zhí)行的時態(tài)和狀態(tài)，Op enabled 描述操作Op 的預(yù)條件已具備，Op occurs|p描述系統(tǒng)執(zhí)行操作Op，Op begin|p 和Op end|p 分別描述時間持續(xù)性操作Op 的開始執(zhí)行和結(jié)束，二元操作符or else 表示在左邊事件未發(fā)生或狀態(tài)不成立時，執(zhí)行右邊事件或判斷右邊狀態(tài)的可成立性。

3 會議系統(tǒng)的責(zé)任策略

會議系統(tǒng)是實時系統(tǒng)，有時間限制，如作者需在投稿截止期前投稿、專家需在審稿截止期前審稿。但會議系統(tǒng)的實時又是非嚴(yán)格的，如當(dāng)投稿數(shù)量未達(dá)到會議預(yù)期投稿數(shù)，會議主席可能推遲投稿截止期限;又如專家在審稿截止期前發(fā)現(xiàn)不能完成審稿任務(wù)，也不會造成嚴(yán)重后果，但專家需承擔(dān)相應(yīng)的補償責(zé)任如推薦其他專家審稿等。

3.1 系統(tǒng)角色及其操作條件

會議系統(tǒng)的主體包括:投稿作者，審稿專家、會議主席和工作人員。會議系統(tǒng)包括截至日期等。

假定主客體及其屬性均已在會議系統(tǒng)注冊時確定，主體的主要動作如下:(1)D1:投稿截止日期;(2)D2:審稿截止日期;(3)D3:會議注冊截止日期;(4)D4:會議收費截止日期。

(1)投稿作者

投稿作者包括論文提交、修改論文、會議注冊、論文修改等操作:

1)Update——更新論文

更新論文操作的限制條件包括:首次上傳論文，或論文處于update 狀態(tài)且只能更新自己投遞的稿件。

更新論文操作的實時條件包括:截止日期D1前可更新論文，如果會議主席修改了截止日期，那么作者也可在新截止日期更新論文。

2)Delete——刪除論文

刪除論文的限制條包括:論文處于update 狀態(tài)且只能刪除自己投遞的稿件。

刪除論文操作的實時條件包括:截止日期D1前可刪除論文，如果會議主席修改了截止日期，那么作者也可在新截止日期刪除論文。

3)Submit——提交論文

提交論文操作的限制條件包括:論文處于update 狀態(tài)，提交人必須是該論文的作者之一且不能是程序委員會委員會。論文提交后狀態(tài)設(shè)置為submit。

提交論文操作的實時條件包括:截止日期D1前提交論文，如果會議主席修改了截止日期，那么作者也可在新截止日期前提交論文。

4)Revise——按照會議出版要求修改已接受論文格式

修改論文格式操作的限制條件包括:論文處于accept 狀態(tài)且只能修改自己投遞稿件。

修改論文格式操作的實時條件包括:會議注冊截止日期D3前可修改論文格式，如果在D3前征得會議工作人員的同意，也可在會議繳費截止日期之前修改論文格式并繳費。

5)Request——請求延長論文格式修改日期

該操作的限制條件包括:論文處于accept 狀態(tài)且只能請求自己投遞的稿件。

該操作的實時條件包括:會議注冊截止日期D3前。

(2)審稿專家

審稿專家包括接受或拒絕評審任務(wù)、評審論文和提交詳審結(jié)果操作:

1)Receive——接受評審任務(wù)

接受評審任務(wù)無限制條件。

接受評審任務(wù)的實時條件包括:接受到評審任務(wù)的一周內(nèi)應(yīng)做出接受或拒絕評審任務(wù)的答復(fù)，如果一周內(nèi)未答復(fù)，系統(tǒng)的政策是默認(rèn)該專家拒絕該評審任務(wù)。

2)Review——評審論文

評審論文無限制條件。

評審論文的實時條件包括:審稿截止日期前;如不能按期審稿，應(yīng)承擔(dān)如下責(zé)任:①在審稿截止日期前推薦一名符合要求并能參加審稿的審稿專家代替自己審稿;②或在審稿截止日期前兩周通知會議主席。③否則審稿專家會被大會列入不良記錄一次。

(3)會議主席

會議主席包括根據(jù)將論文分配給專家評審和根據(jù)專家的評審結(jié)果確定論文的錄用與否的操作。

1)Distribute——分配評審任務(wù)

分配評審任務(wù)限制條件包括:審稿專家不能是論文的作者;審稿專家的不良記錄不超過2 次;審稿專家評閱的論文不超過5 篇;每篇論文的審稿專家人數(shù)應(yīng)不少于3 人。

分配評審任務(wù)的實時條件包括:論文評審分配必須在投稿截止期后一周內(nèi)完成。

2)Decide——確定終審結(jié)果

確定終審結(jié)果限制條件包括:每篇論文返回的評閱結(jié)果不于3 份，如少于3 份，由會議主席另行組織二審專家組評審給出結(jié)論。

確定終審結(jié)果的實時條件包括:會議注冊截止日期的二周前。

3)Changedateline——延長截止日期

延長投稿截止日期的條件:過了投稿截止日期投稿數(shù)量未達(dá)到預(yù)期論文數(shù);截止日期只能延長一次。

延長投稿截止日期的實時條件包括:投稿截止日期之后3 天內(nèi)。

(4)工作人員

工作人員包括會議注冊、會議收費、作者回復(fù)等操作。

1)Register——會議注冊

會議注冊的限制條件包括:論文必須是accept狀態(tài)且論文格式符合會議出版要求，論文注冊后處于register 狀態(tài)。

會議注冊的實時條件包括:會議注冊截止日期D3前。

2)Checki——會議收費

會議繳費的限制條件包括:論文必須是register狀態(tài)且已收到作者注冊費，會議收費后論文處于checkin 狀態(tài)。

會議收費的實時條件包括:在會議收費的截止日期D4前。

3)RequestAnswer——答復(fù)延長注冊申請

答復(fù)延長注冊申請的限制條件包括:論文的delay 標(biāo)志必須是request 狀態(tài)，注冊申請延長答復(fù)后delay 標(biāo)志位處于true 或false 狀態(tài)。

答復(fù)延長注冊申請的實時條件包括:在會議收費的截止日期D4前。

3.2 主要責(zé)任策略

責(zé)任指主體執(zhí)行或不執(zhí)行某種行為時應(yīng)承擔(dān)的義務(wù)，本文探討的主要責(zé)任策略包括缺省(默認(rèn))策略、責(zé)任補償策略和非嚴(yán)格實時策略。

3.2.1 不變式策略的執(zhí)行域

不變式策略包含3 種時態(tài)操作G(always)，X(next)和∪(until)及其簡寫F 和組合GF 等。

時態(tài)操作符G 表示不變式在對象生命周期內(nèi)始終成立，如:

表示在每個時間步內(nèi)(H 表示每小時)系統(tǒng)均檢查上述不變式是否觸發(fā)，如觸發(fā)則產(chǎn)生相應(yīng)的責(zé)任，上式指每個時間步內(nèi)系統(tǒng)均檢查論文分配列表，并對列表中每篇論文均產(chǎn)生責(zé)任F≤7D(ReviewAnswer occurs|p?=p)(7 天內(nèi)應(yīng)做出評審答復(fù))。時態(tài)操作符加上S(秒)、M(分)、H(小時)、D(日)等表示具體的時間步單位。

式(1)中存在的問題是:對論文分配表中的論文，系統(tǒng)每小時就會觸發(fā)一次責(zé)任，將導(dǎo)致一篇論文承擔(dān)多次責(zé)任。

時態(tài)操作符F 表示不變式在對象生命周期內(nèi)最多觸發(fā)一次，如:

式(2)存在的問題是:對論文分配表中的任意論文觸發(fā)一次后，該不變式不再有效，這導(dǎo)致論文分配表只需一篇論文承擔(dān)責(zé)任。

組合操作符GF 表示相同觸發(fā)條件最多觸發(fā)不變式一次，如:

式(3)中對論文分配表中的每篇論文均可觸發(fā)不變式一次，即每篇論文都需承擔(dān)一次責(zé)任，顯然該策略是不變式的初衷。

時態(tài)操作符X 表示不變式只在對象實例化后的下一時間步成立，如:

式(4)說明在對象實例化后的下一時間步，如果用戶類型是長期用戶(usertype=long)，將需要承擔(dān)修改密碼的責(zé)任，其他時候該不變式不再成立。

二元操作符HIST ∪DTLPred 表示的DTLPred執(zhí)行前，不定式HIST 才成立，如:

式(5)說明當(dāng)用戶類型是長期用戶時，如未更改密碼，系統(tǒng)將每小時提醒一次。

3.2.2 缺省(默認(rèn))策略

缺省策略指主體不執(zhí)行某行為時，系統(tǒng)默認(rèn)其應(yīng)承擔(dān)的行為義務(wù)，如評審專家接受到評審任務(wù)的一周內(nèi)應(yīng)做出接受或拒絕評審任務(wù)的答復(fù)，如果一周內(nèi)未答復(fù)，系統(tǒng)默認(rèn)該專家執(zhí)行的是拒絕評審操作。DTL-real-time Object-Z 表達(dá)該缺省策略的方法如下:

不變式(6)使用二元操作符Or else 來表示缺省策略，當(dāng)操作符Or else 左邊的行為不執(zhí)行時，則執(zhí)行其右邊的默認(rèn)操作。

3.2.3 責(zé)任補償策略

責(zé)任補償策略指主體未完成應(yīng)承擔(dān)的責(zé)任操作時，主體也可完成補償責(zé)任操作。如審稿專家有評審論文的責(zé)任，審稿截止日期前，如若未完成責(zé)任，審稿專家可在審稿截止日期前推薦一名符合要求并能參加審稿的審稿專家代替自己審稿;若沒有推薦專家，審稿專家應(yīng)在審稿截止期的前兩周內(nèi)通知會議主席;否則審稿專家會被大會列入不良記錄一次。DTL-real-time Object-Z 表達(dá)該責(zé)任補償策略的方法如下:

式(7)通過多個二元操作符Or else 來表示責(zé)任補償?shù)倪B續(xù)性。

3.2.4 非嚴(yán)格實時策略

非嚴(yán)格實時策略指在滿足一定條件的情況下，系統(tǒng)的實時限制條件可以更改或延遲。如投稿截止期后，投稿數(shù)量不足時，會議主席可以推遲投稿截止期。

本文在會議系統(tǒng)中定義變量delay_days:N 代表延遲天數(shù)，用如下策略表達(dá)實時條件的更改。

其中，#sys.paperlist 表示系統(tǒng)的論文投稿數(shù)，如果小于會議預(yù)期將錄用的論文數(shù)(ENUM)，且已過論文投稿截止期(now ＞D1)，會議主席3 天內(nèi)可推遲論文投稿截止期，即執(zhí)行如下Changedateline 操作:

4 形式化規(guī)格說明

4.1 系統(tǒng)類和全局常量及變量

系統(tǒng)由主體類、客體類和會議系統(tǒng)類3 個部分組成。

主體指主體角色(User)，主體類包括:投稿作者類Author，審稿專家類Reviewer，會議主席類Chair，工作人員類Clerk 以及所有主體類的基類UserBase。

通用類型User 代表任意主體類型，用如下類聯(lián)合定義:

定義全局常量PC 代表程序委員會委員集合，全局常量ENUM 代表會議預(yù)期將錄用的論文數(shù)，全局變量sys 指向會議系統(tǒng)對象MeetingSystem，是會議系統(tǒng)類的全局指針。類型id 代表標(biāo)識符集。

Paper 類和MeetingSystem 類分別代表系統(tǒng)的客體類和會議系統(tǒng)類。

會議截止日期作為全局常量，包括:D1——投稿截止日期;D2——審稿截止日期;D3——會議注冊截止日期;D4——會議收費截止日期。

定義如下:

令A(yù)==N 代表絕對離散時間域，N 是自然數(shù)。DTL-real-time Object-Z 中也包含now 作為全局實時變量，隱含每個類中包含代表當(dāng)前絕對時刻的屬性now:A，該絕對時刻是系統(tǒng)中所有對象共享的全局系統(tǒng)不變式，類中任何操作均隱含:now'≥now［3］。

4.2 會議系統(tǒng)類MeetingSystem

MeetingSystem 類的屬性包括系統(tǒng)注冊用戶集(sysUserList)、會議注冊作者集(meetingUserList)和論文集(paperList)。

其中，register、check 和papersubmit 是環(huán)境輸入函數(shù)，采用時間精化(timed refinement)和ProCos 的方法來形式化輸入環(huán)境，將變量定義為時間到值的函數(shù)［3］，分別描述系統(tǒng)注冊、會議注冊以及論文提交操作。SysRegister，MeetingCheck 和Submit 方法分別將環(huán)境輸入的系統(tǒng)注冊用戶、會議注冊用戶以及提交的論文保存在系統(tǒng)注冊用戶集sysUserList、會議注冊作者集meetingUserList 和論文集paperList，變量delay_days 代表投稿截止日期的延遲天數(shù)。

IdleTick 代表系統(tǒng)空閑時的操作，因而整個系統(tǒng)可如下描述為操作的持續(xù)序列［3］:

4.3 主體類User

UserBase 是所有主體類(User)的基類，其屬性包括主體標(biāo)識ident(系統(tǒng)產(chǎn)生的唯一標(biāo)識)、用戶名username 和密碼password，其方法有修改用戶名和更改用戶密碼，UserBase 類的規(guī)格化說明如下:

Author 類繼承UserBase 類，包括論文更新操作Update、刪除操作Delete、提交操作Submit、修改操作Revise 以及請求操作request。

Update 操作增加或更新作者提交的論文，輸入p?是作者更新的論文，如果該論文在系統(tǒng)的論文列表中，則先刪掉原論文并添加更新論文，如果不在論文列表中，則將論文添加到論文列表中并將該論文的狀態(tài)設(shè)置成update，同時將該作者設(shè)置成通訊作者。Revise 操作按照會議論文的格式修改錄用后的論文。request 操作請求推遲論文提交，如作者提出論文在會議收費截止日期前提交論文。

審稿專家類Reviewer 類繼承Author 類，包括評審回復(fù)ReviewAnswer、論文評審結(jié)論Review 等操作。

其中，distributelist 是分配論文和論文分配的時間映射關(guān)系函數(shù);ReviewAnswer 操作是審稿專家接受或拒絕評審論文的回復(fù);Review 操作是審稿專家評審論文的成績;Recom 操作代表推薦一名審稿專家代替自己審稿;Notif 操作代表通知會議主席;SetBlackList 操作表示把未完成補償責(zé)任的審稿專家列入黑名單。

審稿專家有評審論文的責(zé)任，審稿截止日期前，如若未完成責(zé)任，則需承擔(dān)補償責(zé)任，Reviewer 類的歷史不變式如下:

會議主席Char 類繼承Reviewer 類，包括分發(fā)論文給專家操作Distribute、給出論文的最終總評定結(jié)論操作Conclude 等操作。

Changedateline 操作是更改審稿截止日期;ChangeReviewer 操作是更改審稿專家;Notify 操作是接收審稿專家拒絕審稿通知。

投稿截止期后，投稿數(shù)量不足時，會議主席將推遲投稿截止期，Char 類的歷史不變式如下:

工作人員Clerk 類繼承UserBase 類，包括注冊操作Register、會議繳費操作Checkin 和回復(fù)請求操作RequestAnswer。

format 函數(shù)用來判斷論文的格式是否符合會議格式要求;fee 函數(shù)用來判斷論文是否交了注冊費。

4.4 客體類

在本系統(tǒng)中客體類主要是論文類，其屬性包括作者集(author_list)、論文分配列表(distributelist)、同意審稿專家集(reviewr_list)、拒絕審稿專家集(refuselist)、通訊作者(contactor)、論文內(nèi)容(content)、論文已被評審的次數(shù)(reviewernum)、每位專家對論文評審的成績(scores)、論文評審總分(sum)、論文狀態(tài)(status)和論文延遲提交狀態(tài)(delay)等。

常量NUM 是論文的審稿專家數(shù);scores 是評審專家與其評審論文成績的映射函數(shù)。

5 結(jié)束語

目前，用于Z 和object-Z 語言的語法和類型檢驗工具很多，如Wizard，CZT(Community Z Tools)，TOZE，ZML 和Z/EVES 等。其中，ZML 工具支持TCOZ［13］;TCOZ 是在Object-Z 中加入了時態(tài)限制;DTL-real-time Object-Z 語言的語法和類型檢驗可在ZML 工具的基礎(chǔ)上增加分布式時態(tài)邏輯語法分析進(jìn)行改進(jìn)，具體方法篇幅所限，不再詳述。

本文針對非嚴(yán)格實時系統(tǒng)的實時要求具有延緩性、替代性以及可補償性的特征，采用DTL-real-time Object-Z 語言進(jìn)行規(guī)格說明。該語言通過擴展Object-Z 語言中的歷史不變式來描述責(zé)任策略，能較好地表達(dá)非嚴(yán)格實時系統(tǒng)中各類實時行為的非嚴(yán)格性。本文以會議系統(tǒng)為例，說明了該語言能較好地描述會議系統(tǒng)中的缺省策略、補償策略以及其他非嚴(yán)格實時策略。本文方法具有較好的可應(yīng)用性。

下一步工作將繼續(xù)研究DTL-real-time Object-Z規(guī)格語言在訪問控制、Web 語義集成等領(lǐng)域的具體應(yīng)用。

［1］朱 江，陳怡海，繆淮扣.Object-Z 規(guī)格說明的結(jié)構(gòu)模擬動畫技術(shù)［J］.上海大學(xué)學(xué)報:自然科學(xué)版，2005，11(6):589-195.

［2］龐麗萍.操作系統(tǒng)原理［M］.3 版.武漢:華中科技大學(xué)出版社，2000.

［3］Song Jin，Colton J，Zucconi L，et al.A Formal Object Approach to Real-time Specification［C］//Proc.of the 3rd Asia-Pacific Software Engineering Conference.［S.l.］:IEEE Press，1996.

［4］Smith G，Hayes I J.An Introduction to Real-time Object-Z［J］.Formal Aspects of Computing，2002，13(2):128-141.

［5］魏艷銘，張廣泉.基于Real-time Object -Z 語言的實時系統(tǒng)形式化描述［J］.重慶師范大學(xué)學(xué)報:自然科學(xué)版，2007，24(4):41-44.

［6］Firley T，Huhn M，Diethers K，et al.Timed Sequence Diagrams and Tool-based Analysis:A Case Study［C］//Proc.of the 2nd International Conference on the Unified Modeling Language:Beyond the Standard.New York，USA:Springer，1999:645-660.

［7］Yan Fei，Tang Tao.A Formal Modeling and Verification Approach for Real-time System［C］//Proc.of the 7th World Congress on Intelligent Control and Automation.［S.l.］:IEEEPress，2010:204-208.

［8］張 濤.復(fù)雜信息系統(tǒng)模型的形式化驗證方法研究［D］.哈爾濱:哈爾濱工程大學(xué)，2012.

［9］周 航，黃志球，祝 義，等.基于Time Petri Net 的實時系統(tǒng)沖撞檢測與消解［J］.計算機研究與發(fā)展，2012，49(2):413-420.

［10］席 林.形式化方法在構(gòu)件組裝實時系統(tǒng)中的應(yīng)用研究［D］.鄭州:鄭州大學(xué)，2012.

［11］周治平，夏 娟，紀(jì)志成，等.基于UML 實時系統(tǒng)設(shè)計方法的分析與比較［J］.計算機工程，2005，31(13):99-101.

［12］董榮勝，趙嶺忠，蔡國永，等.基于對象的分布式實時系統(tǒng)調(diào)度模型研究［J］.計算機研究與發(fā)展，2002，39(11):1464-1470.

［13］Mahony B，Dong Jinsong.Blending Object-Z and Timed CSP:An Introduction to TCOZ［C］//Proc.of the 20th International Conference on Software Engineering.［S.l.］:IEEE Press，1998:95-104.