一種實時系統(tǒng)時間約束驗證方法研究

潘誠　王珊珊　王梓　司佳

摘要：目前，能夠?qū)ζ囯娮宇I(lǐng)域中復(fù)雜嵌入式系統(tǒng)安全關(guān)鍵軟件功能模和時間約束分析的方法尚在研究中，而這些系統(tǒng)作為實時控制系統(tǒng)，應(yīng)該確保其具有準確的、可分析的時間行為。時鐘約束規(guī)范語言CCSL是實時系統(tǒng)的標準描述語言中描述時鐘約束的規(guī)范語言。采用CCSL規(guī)范表達式描述實時系統(tǒng)時間約束；設(shè)計了CCSL基本元素到時間自動機基本元素的轉(zhuǎn)換規(guī)則；使用時間自用機驗證工具UPPAAL對轉(zhuǎn)換得到的自動機模型進行驗證分析，驗證實時系統(tǒng)是否滿足相應(yīng)的時間約束。

關(guān)鍵字：實時系統(tǒng)；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引言

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

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

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

2相關(guān)理論

21CCSL

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

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

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

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

22時間自動機

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

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

定義2.2時鐘約束：時鐘約束集合由時鐘變量集合C，約束關(guān)系集合

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

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

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

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

P0是初始狀態(tài)的集合，且P0P；

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

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

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

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

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

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

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

23驗證框架

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

該方法首先系統(tǒng)行為和時間約束結(jié)合起來用CCSL規(guī)范表示；然后根據(jù)給出的CCSL到時間自動機的轉(zhuǎn)換規(guī)則，將CCSL表達式轉(zhuǎn)換為時間自動機；最后導(dǎo)入到UPPAAL中驗證。

3CCSL到時間自動機的轉(zhuǎn)換

31CCSL的狀態(tài)遷移語義

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

定義3.1時鐘狀態(tài)遷移系統(tǒng)（cLTS）：時鐘狀態(tài)遷移系統(tǒng)是一個四元組，A=，其中：

1）S是狀態(tài)的集合；

2）s0∈S是初始狀態(tài)；

3）C是有限時鐘集合；

4）TS×2c×S是轉(zhuǎn)換關(guān)系的集合，其中（s，Y，s′）∈T表示當系統(tǒng)從狀態(tài)s遷移到狀態(tài)時s′，在中YC所有的時鐘都會跳動一次。

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

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

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

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

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

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

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

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

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

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

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

4實例分析

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

5結(jié)束語

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

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

參考文獻

[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