用帶時鐘變量的線性時態邏輯擴充Ｏｂｊｅｃｔ－Ｚ
2009-01-01 00:00:00文志誠李長云滿君豐
計算機應用研究 2009年5期
(湖南工業大學 計算機與通信學院 湖南 株洲 412008)
摘 要：ObjectZ是形式規格說明語言Z的面向對象擴充，適合描述大型面向對象軟件規格說明，但它不能很好地描述連續性實時變量和時間限制。線性時態邏輯能夠描述實時系統，但不能很好地處理連續時間關系，也不能很好地模塊化描述形式規格說明。首先用時鐘變量擴充線性時態邏輯，接著提出了一個方法——用帶時鐘變量的時態邏輯(LTLC)來擴充ObjectZ。用LTLC擴充的ObjectZ是一個模塊化規格說明語言，是ObjectZ語法和語義的最小擴充，其最大優點在于它能方便地描述和驗證復雜的實時軟件規格說明。
關鍵詞：ObjectZ； 用帶時鐘變量的時態邏輯； 實時系統； 形式規格說明； 形式驗證
中圖分類號：TP311文獻標志碼：A
文章編號：1001-3695(2009)05-1764-06
Adding linear temporal logic with clocks to ObjectZ
WEN Zhicheng LI Changyun MAN Junfeng
(School of Computer Communication Hunan University of Technology Zhuzhou Hunan 412008 China )
Abstract:ObjectZ an extension to formal specification language Z is good for describing large scale objectoriented software specification. While ObjectZ has found application in a number of areas its utility is limited by its inability to specify continuous variables and realtime constraints. Linear temporal logic can describe realtime system but it can not deal with time variables well and also can not describe formal specification modularly. This paper extended linear temporal logic with clocks(LTLC) and presented an approach to adding linear temporal logic with clocks to ObjectZ. Extended ObjectZ with LTLC a modular formal specification language is a minimum extension of the syntax and semantics of ObjectZ. The main advantage of this extension lies in that it is convenient to describe and verify the complex realtime software specification.
Key words：ObjectZ; LTLC; realtime system; formal specification; formal verification
0 引言
ObjectZ是形式規格說明語言Z的面向對象擴充，通過面向對象技術易于模塊化設計復雜的數據與算法，但它是單線程語義，操作是原子的且沒有持續動作、抽象的終止。因此，用ObjectZ描述實時系統是比較困難的。
時態邏輯公式可以簡短、精確地描述系統和組件，為了更好地描述實時系統行為與性質，許多時態邏輯已經被提出了，如計算樹邏輯(TCTL)[1]、metric interval temporal logic[2]和線性時態邏輯(LTL)[3]等。線性時態邏輯由Manna等人提出，將行為模型看成是一個線性序列狀態，對于每一個行為，有一個確切的后繼行為。傳統地，實時系統的軟件模型集中研究系統進程與它們的特性，或者數據處理或時間依靠性質。然而，用時態邏輯描述的形式規格說明一般不具有模塊化[4~6]，此外，用時態邏輯描述的規格說明不能很好地處理持續的時間關系和性質。因此，用時態邏輯描述實時系統存在固有的局限性。
本文首先引進了帶時鐘變量的線性時態邏輯(linear temporal logic with clocks，LTLC)，它是用時鐘變量對線性時態邏輯的擴充，易于描述規格說明中的持續時間關系與性質，文獻[7]已做了類似的工作，但不具有面向對象的特性。接下來，將LTLC與ObjectZ結合以彌補它們固有的缺點，更好地描述實時形式規格說明。擴充的ObjectZ是ObjectZ語法和語義最少的擴充，可以精致地描述面向對象實時系統。此外，它還可以描述多線程規格說明，驗證也變得容易。
1 帶時鐘變量的線性時態邏輯
1.1 LTLC語法
LTLC語法由兩部分構成，即線性時態邏輯(LTL)語法和時鐘變量語法。定義如下：
1.1.1 LTL語法
a)變量：x1，x2，x3，…
b)布爾變量：p1，p2，p3，…
c)布爾常量：true 或1
d)常量：c1，c2，c3，…
e)函數：f1，f2，f3，…
f)原子命題：P1，P2，P3，…
g)命題連接詞：，∨，∧，→，
h)等號：=
i)量詞：，
j)時態算子：□(always)，◇(sometimes)，○(next)，(until)
LTL的項e遞歸定義如下：
e::= xi｜pi｜true｜1｜ci｜fi(e)
LTL的命題合式公式B遞歸定義如下：
B::=Pi｜e1=e2｜B｜B1∨B2｜B1∧B2｜B1→B2｜
B1B2｜□B｜◇B｜B1B2｜○B｜xiB｜xiB
1.1.2 時鐘變量語法
a)時鐘變量：tnow，t1，t2，t3，…
b)時鐘常量：mt1，mt2，mt3，…
c)函數操作符：+，-，*
d)關系符：=，≤，＞
時鐘變量tnow(表示現在時間)的類型為realtime，時鐘變量ti和時鐘常量mti類型是Time。
γ::=tnow｜ti｜mti｜(γi-γj)｜(γi+γj)｜(γi*γj)
相似地，時鐘公式C遞歸定義如下：
C::= (γ1=γ2)｜(γ1≤γ2)｜(γ1＞γ2)｜tiC｜tiC
1.1.3 LTLC的語法
帶時鐘變量線性時態邏輯公式A遞歸定義如下：
A::=B｜C｜A｜A1∨A2｜A1∧A2｜A1→A2｜A1A2
｜□A｜◇A｜A1A2｜○A｜uA｜uA(u=xi or ti)
1.2 LTLC語義
LTLC公式的語義可以在Kripke結構上解釋。Kripke結構K=〈U I S R〉：
a)U=D∪T∪{0，1}：非空集合D(個體域)、時間T和布爾集合{0，1}。
b)I：解釋。
c)S：狀態集合。
d)RS×S：轉換關系。
狀態si是到狀態sj的遷移(記做si→sj)，當且僅當(si，sj)∈R。一條路徑是狀態的無限序列，如π=(s0 s1，s2，…)∈S∝，可以記做(s0→s1→s2→s3→…)。解釋I可以對常量、函數和公式進行解釋或賦值。其實，狀態si也可以看做對時鐘變量與非時鐘變量在這個狀態的指派或賦值。其中，在D或布爾集合可以對非時鐘變量指派取值，在時間集合T可以對時鐘變量指派或賦值。事實上，時鐘變量可以按照普通變量(非時鐘變量)來處理，只是取值不同。
設Γ（π，i)表示項Γ在路徑π的位置i的值，(π i)A表示公式A在路徑π的位置i為真。
定義1 一個時態邏輯公式可以解釋在無限的狀態序列π=(s0，s1，s2，…)上，相對于路徑π的位置i，對項Γ和公式A，遞歸定義Γ(π i)和(π i)A如下：
當Γ是一個變量x時，x(π i)=si(x)
當Γ是一個常量c時，c(π i)=cI
這里，a)b)中的變量和常量包括時鐘變量與時鐘常量，只是它們的指派與解釋取值在時間集合T上。
當Γ是一個布爾變量p時，p(π i)=si(p)
對于n元函數f(n)和它相應的項Γ1，Γ2，…，Γn，函數f(n)值為f(n)(Γ1，…，Γn)(π i)=f(n)I(Γ1(π i)，…，Γn(π i))
當公式A是一個n元原子公式P(n) (Γ1，…，Γn)時，存在一個關系：(π，i)P(n)(Γ1，…，Γn) 當且僅當 〈Γ1(π，i)，…，Γn(π i)〉∈P(n)I
對于任何公式A1和A2，定義(π i)A1，(π i)(A1∧A2)，(π i)(A1∨A2)，(π i)(A1→A2)，(π i)(A1A2)類似，例如(π i)(A1→A2)當且僅當 (π i)A1蘊涵(π i)A2。
對任何公式A，(π i)□A當且僅當對任意 j≥i，(π j)A
對任何A，(π i)◇A當且僅當存在j和j≥i，(π j)A
對于任何公式A，(π i)○A 當且僅當(π i+1)A
對于任何公式A1和A2，(π i)A1A2 當且僅當對某個j且j≥i，如果(π j)A2，則對任意k，i≤k 對于任何公式A，(π i)uA 當且僅當對任意的d∈D∪T，(π i)A[d｜u] 對于任何公式A，(π i)uA 當且僅當存在d∈D∪T，(π i)A[d｜u] 如果(π 0)A，則序列π滿足時態邏輯公式A，表示為πA。如果公式A是有效的，即所有的序列滿足公式A，表示為A。 定理1 從LTLC的語義可以得出下面的定理： s)如果A是一個重言式，則A是一個公理 t)如果A是一個公理，則□A也是一個公理 這些定理的證明不難。下面解釋幾個定理： 定理1 f)的意思為：如果A總是為真，則A在下一狀態也為真。i)的意思為：當A真蘊涵在下一個狀態A真，且如果A現在為真，則A永遠為真。 j)的意思為：A1為真直到A2為真等價于A2為真，或者A1為真且在下一個狀態A1為真直到A2為真。因此，可以方便地用LTLC的語法來描述具有持續時間關系和性質的實時規格說明，這些定理能被用來推理實時規格說明的行為與性質。 2 增加LTLC到ObjectZ中 2.1 擴充的 ObjectZ的語法 本節將給出用LTLC擴充的ObjectZ的語法。通常，ObjectZ類的不變式和操作中的謂詞是用謂詞邏輯公式描述的，但在擴充的ObjectZ中，類的不變式與操作謂詞可以用LTLC公式描述。 2.1.1 類結構 對于擴充的ObjectZ類，引進可選的操作MAIN，決定類對象缺省的行為，它是由定義在本類中的一些非確定性操作組成的。在一個類中，當對象初始化后，進程MAIN指出此對象的一個活動行為。在通常情況下，初始化工作在初始化模式中完成。活動對象擁有它們自己控制的線程，它們的狀態變量與操作定義是封裝的(更新事件是隱藏的)。即使相同的類，不同的對象不共享數據。其他的對象不能引用一個活動對象的狀態變量，也不能引起任何其他局部的操作。如果一個類中沒有MAIN進程，它稱為非活動類。非活動對象被系統中其他的對象控制，其狀態與操作對控制對象是充分有效的，除非明確的隱藏。因此，擴充的ObjectZ是一個多線程規格說明語言，它的類結構如圖1所示。 全局時鐘變量tnow，在任何類的外面定義，可以在任何類的狀態模式與初始化模式中使用。其他時鐘變量，在相應的操作中定義，只能被此操作使用。時鐘常量，定義在常量定義部分，與非時鐘常量一樣，能夠被類中任何部分使用。時鐘常量與時鐘變量相結合，對相應的狀態或輸入/輸出變量能起著一個限時作用。 2.1.2 操作結構 標準ObjectZ與擴充的ObjectZ主要區別在于操作模式。在擴充的ObjectZ操作的謂詞部分由幾個可選的謂詞合取連接[8]。操作模式的結構如圖2所示。 在變量定義部分(variable definitions)，狀態變量有形式Δ(x y)，表示狀態變量x和y在這部分將被修改。此外，輸入/輸出變量也定義在這部分中。接收一個輸入，期望一個輸出和通過復雜的函數更新一個狀態變量(形成后狀態)可能會持續一段時間。因此，這些狀態變量與輸入/輸出變量各自有兩個相應的時鐘變量，即前后狀態時鐘變量，它們都定義在此部分中，不定義在狀態模式中。注意，任何時鐘變量不是類中的狀態變量。當然，如果一個操作與時間不相關，在操作中使用的變量沒有相應的時鐘變量。本文將不考慮這種情況，因為它與標準的ObjectZ規格說明相同。 定義2 對于一個狀態變量與輸入/輸出變量v，它的兩個相應時鐘變量為tv和t′v。前狀態時鐘變量tv對于相應的狀態變量或輸入/輸出變量v，起初始化時間和給定期望完成的時間作用，后狀態的時鐘變量t′v起復位或賦值作用。當一個狀態變量或輸入/輸出變量被涉及時(被賦值等)，其相應的時鐘變量初始化且從0開始逐步增加。因此，將狀態變量、輸入/輸出變量對應的時鐘變量直接結合其相應的期望完成的時間，可以方便地描述連續時間關系。 通常地，在一個操作中，時間模塊有兩種轉換，即跳躍轉換(jump transformation)和延時(delay transformation)。跳躍轉換是一個瞬時動作，可表示為state∧guard→new_state。其中，state表示在轉換之前的狀態；new_state表示不超過限制時間內轉換后的狀態；guard表示在跳躍轉換前的能動條件，也就是轉換的前置條件。因此，在擴充的ObjectZ的規格說明中，跳躍轉換可以描述為□(state_v∧tv＞mti∧new_state_v′∧f(t′v))。這里mti(一個時鐘常量)表示在一個操作中的變量v(對應于它的時鐘變量tv)期望完成的時間，通過函數f(t′v)可以對時鐘變量復位或賦予新時間或什么事都不做，即對時鐘變量可以不復位或置新值。 延時轉換(delay transformation)可以被描述為state→invariant。其中invariant表示在限定的時間內狀態沒有被改變。當時鐘變量值不少于限定的時間時，狀態一定得到修改。因此，在擴充的ObjectZ中，可以描述為□((state_v∧tv≤mti)(new_state_v′∧tv＞mti∧f(t′v)))，表示從現在開始，state_v∧tv≤mti為真直到下一個狀態下new_state_v′∧tv＞mti∧f(t′v)為真。由此可知，延時轉換與跳躍轉換是兩個不相同的概念。 設var(jump)和var(delay)分別表示在一個操作中各自出現在跳躍轉換與延時轉換中的所有狀態變量構成的集合，要求[var(jump)]∩[var(delay)]=。一個狀態變量可能出現在延時轉換部分或在跳躍轉換部分，但不能同時出現在這兩個部分之中。也就是說，一個狀態變量或是跳躍變量，或是延時變量，不能同時是兩種變量，輸入/輸出一般是跳躍變量。時鐘變量只能與它相應的狀態變量或輸入/輸出變量一起使用，不能單獨使用。 非轉換部分(nontransformation part)與時間無關，即在這部分出現的狀態變量、輸入/輸出變量與時間無關，因此，條件判斷與前狀態時鐘變量的初始化可以在這個部分執行。條件判斷及前狀態時鐘變量的初始化是瞬時的，使用的時間可以被忽略。時間限制部分(time constraint)，給出時鐘變量與時鐘常量的關系，能夠限制相關的使用時間。 另外，每個操作隱含地關聯著狀態復位操作restore，因為一個對象狀態當超時時必須恢復 (復合操作符{t})。表達式A{t}restore表示如果操作A在最后的時間還沒有完成，則控制轉向操作restore，這由操作中使用的時鐘變量決定。如果一個對象做了很多動作，但最后使用操作restore來廢棄它們，對任何其他的對象來說，這些廢棄的狀態是可視的。如果一個操作只包含延時轉換，則不會超時，因此不必與恢復操作restore結合。同時，可以給定恢復操作restore一致的期望完成的時間。 注意，時態邏輯操作符、□與超時合成符{t}、非確定性選擇符各不相同。用上述方法表示的繼承、多態和復合操作與標準的ObjectZ相同。 2.1.3 簡單例子 下面以十字路口交通管理系統為例，有三個指示燈(綠、黃、紅)和四個狀態(綠、綠和黃、紅、紅和黃)，其實就是紅綠燈之間的變換，中間有一個過渡黃燈。開始時，綠燈亮，持續60 s(綠狀態)。接著，綠燈將向紅燈轉換，但中間有一個過渡狀態(綠和黃狀態)，它將持續3 s。接下來，紅燈持續50 s(紅狀態)。再接下來，紅燈向綠燈轉換，但中間也有一個過渡狀態(紅和黃狀態)，將持續4 s。這四個狀態輪流交替，變換圖如圖3所示。 設狀態變量為p，它可以表示狀態之間的改變，定義在類的狀態模式中，相應的時鐘變量為tp和t′p。明顯地，狀態變量p是一個延時變量，因此可以按照延時轉換來設計。在擴充的ObjectZ風格中，操作lightswitch描述如圖4所示。 謂詞部分表示時鐘變量初始化，從現在的狀態到下一個狀態將持續一段時間。這里，整數1、2、3和4簡單地表示相應的四個狀態。例如，□(p=2∧tp≤3)(p′=3∧tp＞3∧t′p=0)表示總是從現在的狀態2(綠和黃狀態)到下一個狀態3(紅狀態)遷移，這將持續3 s且最后時鐘變量復位(t′p=0)。 2.2 擴充的ObjectZ的語義 ObjectZ采用歷史語義，擴充的ObjectZ的語義與時間有關，本文將它稱為實時歷史語義，將對象的歷史事件與狀態映射到實時上。 2.2.1 擴充的ObjectZ實時歷史語義 Smith[9~11]對ObjectZ類給出了歷史語義模型，它同語法結構相對應，對其進行補充。擴充的ObjectZ歷史模型以實時歷史為基礎，是對標準ObjectZ歷史擴充，它表示實時序列的非單調增加。因此，其實時歷史realtimehistory結構如圖5所示，包括歷史history結構和在進化過程中的對象狀態與實時關系。可以將一個對象的狀態映射到全局時間上，即投映在那些對象狀態已經改變的時間點上，沒有改變的時間點將不考慮。因為擴充的ObjectZ有一個特性，即超時。如果超時，操作會調用恢復操作restore，狀態必須得到復位。因此，在對象的歷史中，可能存在兩個狀態(相應于兩個時間點)，在這兩個狀態，對象值是一樣的。 這里，history是ObjectZ的歷史語義模型；函數state(τ)返回對象在時間τ的狀態； i，j:dom states#8226;states(i)=states(j)表示可能(析取“∨”)存在兩個整數i和j，對象在j的狀態與在i的狀態相同。 對于擴充的ObjectZ實時歷史狀態遷移描繪如圖6所示，可以表達實時歷史。在兩個狀態ss(i)和ss(j)之間，對象狀態可能被修改的時間點為k，k+1，…，m，…和n，如狀態ss(i)在時間點k上，狀態ss(j)在時間點n上。在一個操作開始與結束(形成一個事件，這里是es(i))，狀態可能存在一些局部改變，也就是說，在操作開始與結束之間可能存在一些狀態變量已經被修改而另一些還沒有被修改，一些狀態變量可能被修改的時間點用黑點表示，如圖6所示。 從圖6可知，實時τ比時間historytimes(k) (在時間點k)大，比時間historytimes(k+1) (在時間點k+1)要小，因此，有關系STATE(k)=STATE(τ)。在時間點m，操作restore將被調用，狀態遷移將轉向時間點n(狀態ss(j))，因此，在i的狀態等于在j的狀態，有關系states(i)=states(j) 。其中：ss(i)=STATE(k)和ss(j)= state(n)。注意，k、m、n是時間點，i、j是狀態點，τ是實時變量。 在擴充的ObjectZ中，定義在狀態模式中的狀態變量與時間相關，它們的值隨著時間而改變。因此，如果知道了對象的歷史，則可以獲得在不同時間點狀態變量的值。 2.2.2 操作與操作符的語義 在本節中，定義復合操作符{t}和操作restore/MAIN的語義如下： a)對于復合操作符{t} b)對于操作restore 當一個對象使用操作restore來廢棄先前的動作時，O.restore可以語義上描述為一個模式，表示對象O經歷了一個事件，假設對象O經歷的事件是有限的，事件的操作為restore。 由此可以得出，如果O.restore發生，則對象O先前調用的操作已經超時，它的后狀態與現在狀態的前狀態相同。操作restore的參數為空。函數front和last只對序列有效。 c)進程MAIN 進程MAIN決定一個對象的缺省行為，它是由一些定義在此類中的操作非確定性構成的。其語義定義如下： 這里，函數op返回構成進程MAIN的操作。 3 完成的時間 現在考慮完成一個操作所需要的時間。在ObjectZ中，操作有原子操作(不由兩個或兩個以上操作復合而成的操作)和復合操作，在擴充的ObjectZ規格說明中，也有類似的這兩種操作，將分別討論之。 3.1 操作完成的時間 為了考慮一個操作的完成時間，有幾個符號需定義。在擴充的ObjectZ操作中，δ(OP)表示操作OP期望完成的時間，δ(x)表示變量x從開始被涉及到結束被涉及期望完成的時間。當一個變量被涉及，相應的時鐘變量初始化并從0開始逐步增加。 對變量存在兩種情況：a)在跳躍轉換中，對于狀態變量或輸入/輸出變量，期望完成的時間小于或等于限制的時間，即有δ(v)≤mti，這里，mti是一個時間常量，與變量v相對應。因為在OP在中，有一個謂詞tv＞mti，意思是當它大于時間mti，相應的狀態變量，輸入/輸出變量v一定不會被涉及，但小于mti時也可以不被涉及，提前完成涉及。如果在最后的時間內，對變量v的涉及還沒完成，就會產生超時。按照這樣，δ(OP)等于δ(v)=mti加上此變量v在被涉及前已使用過的時間。b)對于延時轉換，延時狀態變量期望完成的時間等于它所需要的延時，意思是在所需要的延時時間內延時變量的值不會被修改。但如果超過所需要的延時，則必須得到修改，因此δ(v)=mtj。延時變量永遠不會導致超時。 如果在一個操作中不存在超時，則有表達式δ(OP)=∑(δJ(v))+∑(δD(v))和δ(OP)≤∑mtk。這里，δJ(v)表示在跳躍轉換中變量v所使用的時間，δD(v)表示在延時轉換中變量v所使用的時間，mtk (k=1 2 …)表示在操作OP中所使用的時間常量。對于操作restore，期望完成的時間是在規格說明中統一給定的；對于進程MAIN，它的終止隨著對象終止而終止。 3.2 復合操作期望完成的時間 在擴充的ObjectZ中，對一些操作OP1，…，OPn，使用一個或多個操作符如合取(∧)、平行(‖)、序列復合(;)、選擇([])、環境操作符(#8226;)，可以形成一個新的操作OP。除了超時復合操作符{t}外，其他的操作符與標準的ObjectZ相同。復合操作OP期望完成的時間考慮如下： a)OP=OP1∧OP2表示操作OP1和OP2并發執行，以后面那個操作完成而結束。因此，有關系：δ(OP)=max(δ(OP1)，δ(OP2))。 b)OP=OP1;OP2表示操作OP1先執行，OP2在OP1完成后才執行。因此，期望完成的時間等于兩個操作期望完成的時間之和。 c)OP=OP1OP2表示兩個操作中的一個被非確定性執行。因此，期望完成的時間就是非確定被執行那個操作完成的時間。 d)OP=OP1‖OP2表示操作OP1與操作OP2通信。在標準的ObjectZ中，通信方向不明確。有兩種情況，即雙向通信和單向通信。當兩個操作OP1和OP2中有一個終止，則操作OP完成。 e)OP=OP1#8226;OP2表示操作OP1聲明的范圍擴展到操作OP2。操作OP1先執行，完成后，操作OP2被執行。操作OP期望完成的時間等于兩個操作期望完成的時間之和。 f)OP=OP1{t}OP2表示當操作OP1超時后操作OP2被執行。因此，操作OP期望完成的時間是兩個操作期望完成的時間之和。 4 實例研究 考察如下一個擴充的ObjectZ規格說明，它描述了一個系統(圖 7和8)，有兩個類，即console和button。類button描述了按鈕對象特征，它包含一個狀態變量on，記錄按鈕是否在0或1位置(開/關)。開始時，按鈕對象在0狀態。一個按鈕能夠在位置“0/1”上交替轉換，并延時mt1，這個行為可以用操作toggle來說明。因此，在操作toggle中on是延時變量，它按照延時轉換方法來處理，定義了其相應的時鐘變量：ton和t′on。類button第一行指出了此類與外界環境交換的界面限制為初始化模式init和操作toggle。操作toggle僅包括延時狀態變量on，因此不會導致超時，不必與恢復操作restore相結合。對現在的時間tnow有兩個限制：a)要求當現在時間tnow小于將來某個時間sometime (□(tnow＞sometime)時，此對象才能夠被初始化，它是一個時間不變式)；b)所需延時mt1小于最大的延時updelay。時鐘變量tnow在任何類的外面定義，可以被所有的類使用。 類console描述了控制臺對象的特征，它包含兩個按鈕，即busy和lazy。前者比后者使用頻繁。但由于硬件容忍度，按鈕使用次數均不會多于最大次數max。類console對象包括一個常數max，記錄按鈕容忍度。 現在考慮類console的狀態模式。ObjectZ語義保證對象屬性如busy是一個對象標志符，可以引用不同的對象值，雖然對象引用的值可能有時相等，但□(busy≠lazy)表示標志符引用兩個不同的對象。在第二部分，如果本系統能夠初始化，要求現在的時間比0大(□(tnow＞0))。 在狀態模式中定義了兩個狀態變量，即busy_ctr和lazy_ctr，以記錄每個按鈕應用次數。最初，按鈕初始化，記數器為0。操作模式selectAndIncrement0從需要一個來自外界環境的輸入，可以標志所使用的按鈕，但要求busy_ctr＜max。 如果標志的是lazy按鈕，則要求lazy計數器嚴格地小于busy計數器，接著計數器增加。這里，變量busy_ctr和lazy_ctr是跳躍變量，按照跳躍轉換方式。此外，在此類中對狀態變量和輸入/輸出變量還定義了其相應的時鐘變量。在類console中，操作模式selectAndIncrement0與恢復操作restore隱含地結合，構成操作selectAndIncrement。操作selectAndIncrement由操作toggleOneButton來定義，有一個內部輸入參數b?，再調用輸入參數b?對象的操作toggle，這里使用了環境操作符，將聲明范圍擴展到后面部分。當計數器busy_ctr達到最大max，則執行操作shutDown，不能再執行類console對象中的任何操作。除此以外，此類還定義了進程MAIN來決定缺省行為，由操作toggleOneButton或shutDown來非確定性決定的。 5 形式驗證 在擴充的ObjectZ中，不變式和操作的前置條件計算方法與標準的ObjectZ相同。當推理用本方法開發的形式規格說明時，首先可以充分地使用推理標準ObjectZ規格說明的方法[12~15]，接著可以使用在1.2節中描述的帶時鐘變量線性時態邏輯推理方法進行推理。推理用擴充的ObjectZ開發的規格說明比用其他擴充ObjectZ方法開發的規格說明要容易得多，因為可以重用推理標準ObjectZ規格說明的規則與方法。 例如，對于類button，有一個明顯的性質，即按鈕(變量on表示)能夠在位置“0/1”上交替轉換，并延時mt1，可以寫成如下形式： 式(1)表示當按鈕在位置0時，延時mt1到達位置1，或當按鈕在位置1時，延時mt1到達位置0。根據擴展的W邏輯[12，13]，可以按1.2節的方法證明之。 其中[toggle]表示toggle的謂詞形式，在式(3)已經給出了。因此證明了式(1)，驗證了所需性質。 6 結束語 實時系統與其他非實時系統之間的最大不同之處就是實時系統要滿足需求功能與時間之間的關系，對于許多系統來說，實時系統的精確需求是必要的，特別對于安全關鍵系統來說，經常需要功能和時間要求。本文給出了一個方法來用帶時鐘變量的時態邏輯擴充形式規格說明語言ObjectZ，使得可以方便地開發與驗證面向對象實時規格說明。這樣，用時態邏輯可以方便地描繪時間關系，驗證規格說明可以分兩步，首先使用推理ObjectZ規格說明的擴展的W邏輯[12，13]，再使用1.2節所描述的推理時態邏輯公式的定理進行推理，可以重用已有的推理方法及規則。因此，用帶時鐘變量的線性時態邏輯擴充ObjectZ最大的優點在于它能方便地描述和驗證復雜的實時軟件規格說明。 參考文獻： ［1］TORRE S L NAPOLI M. A decidable dense branchingtime temporal logic[C]//Proc of the 20th Conference on Foundations of Software Technology and Theoretical Computer Science Table of Contents. London:[s.n.] 2000:139-150. [2]BOWMAN H，CAMERON H KING P，et al. Mexitl: multimedia in executable interval temporal logic[J]. Formal Methods in System Design 2003，22(1): 5-38. [3]MANNA Z PNUELI A. The temporal logic of reactive and concurrent systems: specification[M].New York:SpringerVerlag，1992. [4]BELLINI P MATTOLINI R NESI P. Temporal logics for realtime system specification[J]. ACM Computing Surveys 2000，32(1):12-42. [5]HENZINGER T A MANNA Z PNUELI A. Temporal proof methodologies for timed transition systems[J]. Information and Computation 1994，112(2):273-337. [6]MATTOLINI R NESI P. An interval logic for realtime system specification[J]. IEEE Trans on Software Engineering 2001，27(3):208-227. [7]LI Guangyuan TANG Zhisong. A linear temporal logic with clocks for verification of realtime systems[J].Journal of Software，2002，13(1):33-41. [8]MIAO Huaikou WEN Zhicheng. An approach to extending ObjectZ with realtime[C]//Proc of the 3rd IEEE International Workshop on Electronic Design Test and Applications. Kuala Lumpur Malaysia:IEEE Computer Society press 2006:345-349. [9]SMITH G. An objectoriented approach to formal specification[D]. Australia: University of Queensland 1992. [10]SMITH G. The ObjectZ specification language[C]//Advances in Formal Methods.[S.l.]: Kluwer Academic Publishers 2000. [11]SMITH G. Statebased approaches: from Z to ObjectZ formal methods for distributed processing: a survey of objectoriented approaches[M]. New York:Cambridge University Press 2001:105-125. [12]SMITH G. Extending W for ObjectZ[C]//Proc of the 9th International Conference of Z Users (ZUM’95). 1995:276-295. [13]SMITH G. Reasoning about ObjectZ specifications[C]//Proc of Asia Pacific Software Engineering Conference. Brisbane Queensland Australia:[s.n.] 1995: 489-497. [14]WINTER K SMITH G. Compositional verification for ObjectZ[C]//Proc of International Conference of Z and B Users (ZB 2003). Turku Finland:[s.n.] 2003:280-299. [15]WEN Zhicheng MIAO Huaikou ZHANG Xinlin. Formal verification based on ObjectZ specification[J]. Computer Science，2007，34(5): 247-251.
