具備時鐘變數的通訊與時間轉移系統之驗證方法

Abstract

目前大多數的即時系統驗證方法皆以Timed Automata作為即時系統描述模型。Timed Automata模型以有限狀態機結合時鐘變數與時鐘值限語法來描述即時系統之時間特性，再以Region Graph代表Timed Automata模型之執行行為，然後在此Region Graph上驗證時間性質。但Region的個數隨時鐘變數個數及時鐘值限常數值的增加而呈指數關係成長，因此驗證複雜的即時系統時，常因Region個數過於龐大而導致狀態爆炸問題的發生。 此外也有人採用Communication Timed Transition System(簡稱CTTS)模型以描述即時系統時間特性，該模型在有限狀態機之轉移上設定執行時間以表達系統時間特性。CTTS模型之時間性質驗證方法則是以路徑導向方法將系統模型切割為一組並行路徑，而後依次對每一並行路徑進行時間性質驗證，並行路徑之複雜度遠小於系統之複雜度，因此不會發生狀態爆炸問題。但CTTS模型最大的缺點為對即時系統時間特性之描述能力不如Timed Automata模型，因此造成某些時間性質無法驗證。 鑑於上述方法之缺點，本論文提出在CTTS模型加上時鐘變數與轉移執行時間上下限之Communication Timed Transition System with Clocks(簡稱CTTSC)模型，文中亦證明CTTSC模型具有與Timed Automata模型相同的即時系統時間行為描述能力。由於模型之變更，CTTS模型之時間性質驗證方法也必須加以修改及擴充，修改之重點包括︰ (1) 在路徑產生過程中增加對轉移上時鐘值限的檢查， (2) 在可達狀態分析過程中，將各模組之時鐘變數值記錄在可達狀態圖中的每個系統狀態，以便檢查系統狀態之時鐘變數值是否滿足轉移上所設定的時鐘值限， (3) 重新設計TCTL時間性質方程式之模型檢查演算法。 論文中也以兩個即時系統實例來說明驗證過程，由此二範例可發現本文所提出的CTTSC模型之時間性質驗證方法不僅驗證效率高、且無狀態爆炸問題之顧慮。

Most verification methods of timed systems are based on Timed Automata to model the system timing behavior. Timed Automata describe timing constraints in systems by annotating the state transition graphs with many clock variables and clock constraints. A Region Graph is constructed to represent the execution behavior of a timed automaton. Then, timing properties of a timed automaton can be analyzed on the region graph. However, the number of regions is exponential to that of clocks and the length of clock constraints. When a complicated timed system is verified, the large number of regions will lead to the state explosion problem. Another one timed system verification method is based on Communication Timed Transition System (CTTS) model. It defines the execution time of every transition in state transition graph to express the timing constraints of a system. The verification method of CTTS uses path-based approach to partition the whole system model into a set of concurrent paths, and then it verifies the timing properties on each concurrent path separately. The size of a concurrent path is much less than that of the whole system model, and thus the state explosion problem is alleviated. But the major problem of CTTS model is that its expressiveness for system timing constraints is weaker than timed automata model. And thus, there are some timing properties can’t be verified. Recognizing the difficulties of the above methods, we propose the verification method based on the new Communication Timed Transition System with Clocks (CTTSC) model. CTTSC model is revised from CTTS model by adding clock variable and defining the upper and lower bound of execution time on every transition. We also show that CTTSC and Timed Automata models have equal expressivenesses. Accordingly, the verification method for timing properties on CTTSC model is revised from that on CTTS model as follows: (1) Check timing constraints of clocks on transitions on generating paths for each module, (2) Record the value of each module clock in the global states of reachability graph to check whether the module clock satisfies the clock constraints on transitions, (3) Redesign the TCTL model checking algorithm. We also provide two examples to demonstrate the process of timing properties verification on CTTSC model. With the two examples, we show that the verification method of CTTSC model has high verification efficiency and no state explosion problem.