一種實時系統時間約束驗證方法研究

潘誠　王珊珊　王梓　司佳

摘要：目前，能夠對汽車電子領域中復雜嵌入式系統安全關鍵軟件功能模和時間約束分析的方法尚在研究中，而這些系統作為實時控制系統，應該確保其具有準確的、可分析的時間行為。時鐘約束規范語言CCSL是實時系統的標準描述語言中描述時鐘約束的規范語言。采用CCSL規范表達式描述實時系統時間約束；設計了CCSL基本元素到時間自動機基本元素的轉換規則；使用時間自用機驗證工具UPPAAL對轉換得到的自動機模型進行驗證分析，驗證實時系統是否滿足相應的時間約束。

關鍵字：實時系統；CCSL；時間自動機；時間約束；模型檢測

中圖分類號：TP311文獻標識碼：A

Abstract：Nowadays，functional modeling and time constraint analysis are separated for safetycritical software in complex embedded system，in the areas of automotive electronics.These systems as realtime systems should be ensured that they are accurate and can be analyzed by time constraint.Clock Constraint Specification Language （CCSL） is the standard language for describing clock constraints in a standard description language of a realtime system.Time constraint of realtime system described by CCSL regular expression；The transformation rules of CCSL basic elements to time automata basic elements are designed.Using UPPAAL，we validate that the realtime system satisfies the corresponding time constraints by verifying and analyzing the converted automata model.

Key words：realtime system；CCSL；time automata；time constraint；model checking

1引言

嵌入式實時系統中存在大量、復雜的組件交互行為，其中廣泛應用于航空航天、汽車電子、核電等對實時響應，時間約束具有較高要求的安全性工業控制中[1]。隨著軟件體系結構越來越復雜，軟硬件的交互行為越來越廣泛，這些行為如果不嚴格滿足特定的時間約束，則有可能帶來不可估量的生命財產損失。如何設計有著高質量、高可靠性的實時系統，并且可以進行時間約束的驗證工作，這是學術界和工業界亟待解決的一大熱點問題[2]。

目前為止，UML/MARTE[3]（ Unified Modeling Language /Modeling and Analysis of Real Time and Embedded systems）已成為工業界認可的針對實時系統的標準建模語言且已廣泛使用。CCSL[4]是MARTE規范中的一個附件，專門用來描述實時系統中各組件之間的時鐘規范，它在MARTE時鐘基礎上建立了時鐘間的因果關系和時間約束。本文提出一種基于時間自動機的時間約束驗證方法：首先，實時系統中的時間約束被描述為CCSL表達式；然后給出CCSL表達式到時間自動機之間的轉換方法；最后根據得到的時間自動機網絡，在UPPAAL[5]工具中進行驗證，分析時間約束是否被滿足。

本文后續章節安排如下：第2節，簡要介紹時鐘約束規范語言CCSL、時間自動機TA，給出基于時間自動機的實時系統時間約束驗證框架；第3節給出CCSL表達式到時間自動機的轉換規則；第4節，通過一個實例說明本文提出方法的可行性和有效性；第5節，結束語。

2相關理論

21CCSL

UML/MARTE引入了一個豐富的時間模型來支持離散和連續時間，物理和邏輯時間。在MARTE中，時鐘（Clock）是時間模型中的重要元素[6]。在使用MARTE時間模型時，某些獨立的時鐘又一般定義為單獨的模型，CCSL是描述這些時鐘模型的規范語言。

定義2.1CCSL時鐘：一個時鐘可以描述為一個五元組C = < T，<，D，λ，u >，其中T是瞬時的集合，<是Γ上關系的集合，D是標簽的集合，λ：T→D是標簽函數，u是一個符號化的單元。

時鐘可以分為邏輯時鐘（離散時鐘），物理時鐘（連續時鐘），CCSL描述的時鐘為邏輯時鐘[7]，u被稱為一跳（tick），表示對應瞬時的發生。有序集合< T，< >是時鐘上的時序化結構，<是T上的非自反，可傳遞的二元關系。由于邏輯時鐘也是離散時鐘，那么瞬時集合T中的瞬時可以采用自然數來表示排序關系：如果

CCSL的時鐘模型是MARTE對時間概念的進一步抽象，在MARTE的規范說明書中，時間建模是其重要部分之一，其中包括元模型的建立，與其他模型之間的關聯等，CCSL語法包括時鐘約束CC（clock constraint）、時鐘關系CR（clock relation）、時鐘表達式CE（clock expression）、時鐘規范CS（clock specification）和關系操作Rop（relation operators）。其中時鐘關系與時鐘表達式是本文關注的重點，使用巴克斯（Backus-Naur）范式對其進行描述[8]，如圖1所示。endprint

22時間自動機

在對實時系統的軟件安全性分析中，由于計算過程通常需要在滿足特定的時間約束條件下才能進行，為了解決這一問題，Alur R于1994年提出時間自動機（Timed Automata，TA），其本質是一種擴展了時間變量的有限狀態機，通過時鐘（主要包括用來描述絕對時間的物理時鐘和描述相對時間的邏輯時鐘）和時鐘通道等概念來描述系統時間約束性，有效實現了對實時系統行為的形式化描述及計算[9]。

在時間自動機中，系統的行為由時間變量約束，系統所處的狀態由位置節點表示，位置節點之間的有向邊表示系統狀態的遷移。在系統運行的開始階段，系統內置時鐘初始化為0，隨著時間的推移，系統的運行時間不斷增長，當內置時鐘變量的值滿足有向邊上的遷移條件（如有同步信號則還需同步信號到來）時便發生狀態的遷移。這種基于時間約束遷移條件的自動機保證了系統在時間軸上不會一直停留在一個狀態。

定義2.2時鐘約束：時鐘約束集合由時鐘變量集合C，約束關系集合

Φ組成，其中Φ（C）={φ|φ是一個時鐘約束}

表示時鐘約束集合[8]。時鐘約束φ具有如下定義：φ=x≤c|x≥c|xc|-φ|φ1^φ2，其中x∈C表示時鐘變量，x∈R+表示非負實數常量，φ1和φ2表示兩個不同的時鐘約束。

定義2.3時間自動機語法[10]：一個時間自動機可以由一個六元組表示，六元組的定義為：A=，其中：

P是時間自動機A中有窮狀態的集合，此集合非空；

P0是初始狀態的集合，且P0P；

Q是時間自動機A中有窮時鐘變量的集合；

S是時間自動機A中有窮事件的集合；

M是映射關系的集合，M可以表示為狀態之間的笛卡爾積，對于m∈M，記m=， 其中p表示起始狀態，p0表示目標狀態，且p、p0∈P；s是遷移動作，φ表示時鐘約束，x是時鐘變量；m表示在遷移動作s的觸發下，約束條件φ得到滿足，時間自動機A從起始狀態遷移到目標狀態，同時時鐘變量x被更新；

T是狀態集合P到時鐘集合的映射，記為P→Φ（0）。

定義2.4時間自動機語義[10]：對于時間自動機A=，它的語義可以通過轉換系統PA來描述。PA的狀態表示為一個二元組（p，f），其中p∈P，f是T（p）的時鐘解釋，滿足T（p）；若p∈P0且f（q）=0，那么狀態（p，f）是初始狀態。PA中主要有兩類轉換：

1）延遲遷移，即因時間的流逝導致狀態發生改變而引發的遷移：（p，f）q（p，f+q），其中q∈R+，f∈T（p）且f+q∈T（p）。

2）離散遷移，即因位置的變換而引發的遷移：（p，f）q（p′，f′），當且僅當sa，φ，qp′時，f∈T（p），f′=[q→0]f，f′∈T（p′）。

23驗證框架

本文基于時間自動機的實時系統時間約束驗證框架如圖2。

該方法首先系統行為和時間約束結合起來用CCSL規范表示；然后根據給出的CCSL到時間自動機的轉換規則，將CCSL表達式轉換為時間自動機；最后導入到UPPAAL中驗證。

3CCSL到時間自動機的轉換

31CCSL的狀態遷移語義

CCSL是描述UML/MARTE時間模型的時鐘規約語言，能夠采用時鐘模型對系統行為和時間需求進行規約，但是其規范說明書中并未明確給出與狀態遷移相關的語義[11]。在給出CCSL和時間自動機之間的映射關系之前，為CCSL引入基于狀態遷移系統的語義是必要的。

定義3.1時鐘狀態遷移系統（cLTS）：時鐘狀態遷移系統是一個四元組，A=，其中：

1）S是狀態的集合；

2）s0∈S是初始狀態；

3）C是有限時鐘集合；

4）TS×2c×S是轉換關系的集合，其中（s，Y，s′）∈T表示當系統從狀態s遷移到狀態時s′，在中YC所有的時鐘都會跳動一次。

CCSL規約可以采用cLTS表示。其中狀態表示當前系統經過時鐘跳動之后所處在的位置，狀態之間的有向邊表示相應的時鐘跳動一次。下面給出幾種簡單的CCSL時鐘關系的狀態遷移圖：

同步關系：時鐘a，b是兩個邏輯時鐘，對于任意調度σ∈N→2c滿足條件（σ=a=b）（n∈N，a∈σ（n）b∈σ（n）），則a與b滿足同步關系a=b。狀態遷移圖如圖3所示。

包含關系：時鐘a，b是兩個邏輯時鐘，對于任意調度σ∈N→2c滿足條件（σ=a=b）（n∈n，a∈σ（n）b∈σ（n）），則a與b滿足包含關系ab。狀態遷移圖如圖4所示。

互斥關系：時鐘a，b是兩個邏輯時鐘，對于任意調度σ∈N→2c滿足條件（σ=a=b）（n∈N，aσ（n）Vbσ（n）），則a與b滿足互斥關系a # b。狀態遷移圖如圖5所示。

32CCSL元素到時間自動機元素的映射

CCSL支持Integer、Boolean、String以及Real等數據類型，而在UPPAAL中僅支持整型Integer、布爾型Boolean以及字符型String三種基本數據類型（數組等其他類型都是從這三種演化而來的）。根據CCSL和UPPAAL時間自動機對于數據類型的定義，給出它們之間的映射關系，如表1所示。其中，Real類型在映射到整數型時直接向下取整。

CCSL規約將系統行為抽象為時鐘表達式，其中時鐘刻畫了系統在其運行時某一類事件發生的序列，時鐘關系描述了系統在其運行時多類事件之間的優先關系，時鐘表達式則描述了系統在其運行時事件之間更為復雜的約束關系。根據CCSL和時間自動機中各元素的定義建立它們之間的語義映射規則，其中CCSL規約代表了整個系統行為在語義上與UPPAAL時間自動機網絡一致；時鐘是瞬時的集合，定義了某一個事件循環往復地發生在語義上與循環結構的自動機狀態之間的循環遷移發送廣播通道（Broadcast channels）的語義相一致。如上節所述，CCSL并沒有明確系統具體所處的狀態語義，時鐘的瞬時跳動只能表達狀態的遷移，即UPPAAL位置之間的有向邊，而UPPAAL中的位置只能隱式地表達為時鐘瞬時跳動前后的某些狀態。CCSL和UPPAAL自動機元素的語義映射詳見表2。

CCSL具有多種時鐘關系和時鐘表達式，其中優先關系，周期表達式，延遲表達式與本文時間約束密切相關，下面給出它們的詳細映射規則：其中S狀態表示成功狀態，F狀態表示失效狀態。

1）優先關系：優先關系指定了兩個時鐘的邏輯關系，如果時鐘A優先于時鐘B，那么時鐘A的瞬時也優先于時鐘B對應的瞬時。圖6表示優先關系映射的時間自動機模板。

2）周期表達式：周期表達式一般用于離散時鐘的生成，即時鐘從連續物理時間中取周期運算，獲得具有某一周期的離散邏輯時鐘。圖7表示周期表達式的時間自動機模板。

3）延遲表達式：延遲表達式指定了一個參考時鐘，目標時鐘是由參考時鐘經過延遲后生成的，即對于參考時鐘的所有瞬時，目標時鐘的所有對應瞬時都要延遲一定的時間區間T[low，upper]。圖8表示延遲表達式的時間自動機模板。

4實例分析

下面給出一個電子剎車系統的案例分析。剎車系統由剎車踏板傳感器，主控制器，剎車執行器組成，它們的UML結構圖如圖9所示。所需滿足的CCSL表達式如表3所示。

5結束語

針對時間約束的驗證工作還未得到統一，且時間約束難以進行形式化的分析。本文給出一種將CCSL規范的一部分轉換為時間自動機來驗證時間約束滿足性的方法。通過CCSL基本元素與時間自動機基本元素之間語義的一致性，將CCSL元素映射為時間自動機元素，進而根據映射規則，給出時鐘關系的時間自動機模板。最后給出一個實例分析驗證方法的可行性和有效性。

在接下來的研究中，我們將進一步對完整的CCSL規范進行轉換，并嘗試給出語義一致性的證明，并給出一個簡單可用的自動化轉換工具來完善研究工作。

參考文獻

[1]CHEN Huowang，WANG Ji，DONG Wei.High confidence software engineering technologies[J].Acta Electronica Sinica，2003，31（12A）：1933-1938.

[2]黃志球，徐丙鳳，闞雙龍，等.嵌入式機載軟件安全性分析標準、方法及工具研究綜述[J].軟件學報，2014.25（2）：200-218.

[3]MARTE UML.UML profile for MARTE：modeling and analysis of realtime embedded systems[J].2015.

[4]ANDR C.Syntax and semantics of the clock constraint specification language （CCSL）[D].INRIA，2009.

[5]LARSEN K G，PETTERSSON P，YI W.UPPAAL in a nutshell[J].International Journal on Software Tools for Technology Transfer （STTT），1997，1（1）：134-152.

[6]GASCON R，MALLET F，DEANTONI J.Logical time and temporal logics：comparing UML MARTE/CCSL and PSL[C]//2011 Eighteenth International Symposium on Temporal Representation and Reasoning.IEEE，2011：141-148.

[7]MALLET F.Clock constraint specification language：specifying clock constraints with UML/MARTE[J].Innovations in Systems and Software Engineering，2008，4（3）：309-314.

[8]ANDR C.Syntax and Semantics of the Clock Constraint Specification Language （CCSL）[J].HALINRIA，2009.

[9]ALUR R DILL D L，A theory of timed automata[J].Theoretical Computer Science，1994.126（2）：183-235.

[10]ALUR R.Timed automata[C]//International Conference on Computer Aided Verification.Springer Berlin Heidelberg，1999：8-22.

[11]MALLET F，SIMONE R DCorrectness issues on MARTE/CCSL constraints[J].Science of Computer Programming，2015.106：78-92.endprint