安全關(guān)鍵的信息物理系統(tǒng)中時序行為的組合與精化

陳 博 李 曦,2 周學(xué)海,2

1 （中國科學(xué)技術(shù)大學(xué)軟件學(xué)院 江蘇蘇州 215123）

2 （中國科學(xué)技術(shù)大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院 合肥 230051）（chenbo2008@ustc.edu.cn）

信息物理系統(tǒng)（cyber physical systems, CPS）通常是由多個組件（物理組件、計(jì)算組件等）組成的復(fù)雜信息系統(tǒng)[1].其發(fā)展迅速，尤其在近年計(jì)算機(jī)系統(tǒng)中軟硬件架構(gòu)處理能力不斷強(qiáng)化的加持下，使得CPS迭代速度不斷加快.比如某款汽車系統(tǒng)中包含由200個供應(yīng)商中提供的70多個 ECU 單元，且數(shù)量不斷增加，同時預(yù)計(jì)內(nèi)部軟件系統(tǒng)代碼量也將從2005年的幾百行增長至2025年的100億行，面對如此復(fù)雜龐大的系統(tǒng)，如何保證系統(tǒng)的正確性、安全性是類似CPS開發(fā)過程所面臨的主要問題.現(xiàn)今，基于構(gòu)件的開發(fā)（component-based development, CBD）方法成為該類系統(tǒng)主要的開發(fā)方式[2].其具體過程如圖1所描述，首先給出頂層規(guī)約（specification），再通過精化方法細(xì)化規(guī)約，最終得到具體實(shí)現(xiàn)（implementation）.因此，構(gòu)建系統(tǒng)關(guān)鍵屬性的行為模型，再利用精化與組合方法生成具體模型，最終對關(guān)鍵屬性進(jìn)行驗(yàn)證是CBD方法的核心內(nèi)容.

Fig.1 Component software development method based on V model圖1 基于 V 模型的組件化軟件開發(fā)方法

為了對安全攸關(guān)的CPS進(jìn)行設(shè)計(jì)開發(fā)，本文基于時序約束描述語言（clock constraint specification language,CCSL）對系統(tǒng)進(jìn)行實(shí)現(xiàn).具體地，本文主要貢獻(xiàn)體現(xiàn)在3個方面：

1）給出時序行為可組合的形式化定義.為了闡述時序行為的組合過程，通過遷移系統(tǒng)（transition system,TS）描述時序約束語義，并在此基礎(chǔ)上給出時序行為可組合的形式化定義.

2）給出基于L*學(xué)習(xí)的系統(tǒng)屬性驗(yàn)證方法.通過分治策略對系統(tǒng)屬性進(jìn)行驗(yàn)證，有效解決模型組合后所帶來的狀態(tài)激增的問題.

3）提出針對時序約束行為的逐步求精方法.主要針對3種典型的時序約束規(guī)約進(jìn)行精化實(shí)現(xiàn)，給出任務(wù)結(jié)構(gòu)的生成規(guī)則，能夠?qū)㈨攲拥臅r序規(guī)約模型映射為操作系統(tǒng)中任務(wù)級的時序行為約束模型.

1 相關(guān)工作

目前，在時序規(guī)約建模與精化等方面已有若干相關(guān)工作的開展[3-4]，本節(jié)將對其進(jìn)行歸納和比較.

1.1 時間行為的組合與驗(yàn)證

時序行為模型是安全攸關(guān)的CPS在設(shè)計(jì)與開發(fā)過程中需要構(gòu)建的主要內(nèi)容[5].為了對系統(tǒng)的時序行為進(jìn)行描述，國內(nèi)外研究小組從系統(tǒng)的不同層次、不同角度對系統(tǒng)行為進(jìn)行刻畫.較為著名的研究如加州大學(xué)伯克利分校的Eker等人[6]從系統(tǒng)的異構(gòu)計(jì)算模型（model of computation, MOC）角度刻畫組件行為，生成組件的異構(gòu)行為模型，并在文獻(xiàn)[7]中通過狀態(tài)機(jī)方法來檢查組件之間異構(gòu)行為的可組合性.其次，Kopetz[8]從通信行為角度對組件時序關(guān)系進(jìn)行刻畫，設(shè)計(jì)時間觸發(fā)架構(gòu)用于保證節(jié)點(diǎn)與節(jié)點(diǎn)之間傳輸過程的正確性，并給出時序防火墻（temporal firewall）概念[9]來刻畫組件的時序行為并判定其可組合性.其次，賓夕法尼亞大學(xué)Insik等人[10]的研究工作專注于建立層次化的系統(tǒng)行為模型，描述CPS具有分層的系統(tǒng)架構(gòu)，建立分層模型逐層刻畫行為和驗(yàn)證行為的可組合性.文獻(xiàn)[11]中給出了更為傳統(tǒng)的系統(tǒng)模型，并描述系統(tǒng)由若干任務(wù)、調(diào)度器以及時鐘等元素組成，以及通過UPPAAL驗(yàn)證工具對任務(wù)的可調(diào)度性進(jìn)行驗(yàn)證.

針對CPS進(jìn)行設(shè)計(jì)開發(fā)仍然需要形式化工具的支持.在已有的方法中，基于狀態(tài)語義的自動機(jī)模型，如接口自動機(jī)[12]、I/O自動機(jī)[13]等均被用于描述組件的接口行為，并分別依據(jù)典型的樂觀與悲觀2種組合方式對組件的可組合性進(jìn)行判定.同時，相關(guān)工作增加了時間屬性并給出時間自動機(jī)[14]、時間I/O自動機(jī)[15]等方法用于對系統(tǒng)的時間行為進(jìn)行刻畫.Henginzer[16]提出的混成自動機(jī)也是一種典型的基于狀態(tài)建模思想，是能夠?qū)PS中離散行為和連續(xù)行為進(jìn)行建模與驗(yàn)證的形式化方法.2021年，Lin等人[17]也通過混成自動機(jī)建模了復(fù)雜系統(tǒng)的行為，并以此判定系統(tǒng)的可控性.又如基于事件語義的Event-B形式化方法，相關(guān)工作給出了基于Event-B語言的以事件精化、事件組合[18-19]為核心的系統(tǒng)實(shí)現(xiàn)方法.其次，遷移系統(tǒng)也是一種能夠?qū)M件行為進(jìn)行建模的有效方法，基于此語義開發(fā)的LTSA（label transition systems analyzer）分析軟件是一種有效的建模工具，能夠?qū)ο到y(tǒng)進(jìn)行建模、分析，同時可以判定模型所具有的屬性，并當(dāng)存在違反屬性的反例時，能夠?qū)Ψ蠢龜?shù)據(jù)進(jìn)行輸出.因此從易用性、可行性等角度出發(fā)，本文最終選擇遷移系統(tǒng)作為時序行為的形式化描述方法.

1.2 CCSL時間約束建模

CCSL語言由Zhang等人[20]提出，其作為UML/MARTE語言中的時間模型被廣泛關(guān)注.CCSL是一種半形式化的語言，對于CCSL的形式化表達(dá)及屬性驗(yàn)證仍然是一個具有挑戰(zhàn)性的工作.為了驗(yàn)證時序約束關(guān)系，相關(guān)工作已經(jīng)基于不同的方法對模型進(jìn)行驗(yàn)證，如自動機(jī)、動態(tài)邏輯[20]、SMT可滿足理論等方法對CCSL進(jìn)行語義轉(zhuǎn)換并驗(yàn)證.在國內(nèi)的研究中，華東師范大學(xué)Zhang等人[21]的若干工作對CCSL的發(fā)展也起到推動作用.

1.3 時間行為的精化

傳統(tǒng)的逐步求精方法[22]主要針對UML中的時序圖、狀態(tài)圖進(jìn)行求精的實(shí)現(xiàn)，將時序圖、狀態(tài)圖模型映射為底層具體模型.然而在對CPS行為進(jìn)行求精時，如何將頂層的規(guī)約精化為底層的具體實(shí)現(xiàn)是CBD方法的核心內(nèi)容.而針對時間行為的精化等同于對任務(wù)的時間屬性的分解.文獻(xiàn)[23]將數(shù)據(jù)流分成2種類型并進(jìn)行調(diào)度，給出了保證時間約束的數(shù)據(jù)流調(diào)度算法，以使數(shù)據(jù)延遲變得確定.文獻(xiàn)[24]也設(shè)計(jì)一種能夠保證數(shù)據(jù)流延遲時間約束的調(diào)度實(shí)現(xiàn)方法，將系統(tǒng)整體的時間約束轉(zhuǎn)化為子系統(tǒng)的時間約束關(guān)系，保證傳輸過程時間行為的正確性.同樣，文獻(xiàn)[25]提出一種將上層時序規(guī)約映射為下層任務(wù)執(zhí)行模型的求精策略，在求精流程中將時間延遲規(guī)約分解為子系統(tǒng)級的時間規(guī)約，最后生成相應(yīng)的任務(wù)集.在文獻(xiàn)[26]中實(shí)現(xiàn)了對組件執(zhí)行時間進(jìn)行預(yù)分配（time-budget）的方法，主要通過2個過程來具體實(shí)現(xiàn)：過程1會把時間延遲進(jìn)行子系統(tǒng)級別的分配；過程2將基于迭代的策略對子系統(tǒng)中的任務(wù)進(jìn)行組合來創(chuàng)建任務(wù)子集.

通過對國內(nèi)外關(guān)于CPS建模與精化的研究發(fā)現(xiàn)，現(xiàn)有工作中解決CPS的建模問題普遍從計(jì)算行為、層次化調(diào)度行為等角度入手建立模型并驗(yàn)證屬性.而針對安全關(guān)鍵CPS的實(shí)際具體開發(fā)而言，仍然需要依據(jù)已有的上層建模語言，從時間行為角度建立系統(tǒng)的時序行為需求模型，繼而通過組合、精化等方法對系統(tǒng)進(jìn)行設(shè)計(jì)與驗(yàn)證.通過調(diào)研，現(xiàn)有研究中仍然缺少類似工作.為了解決該問題，本文較為系統(tǒng)化地對基于時序行為的建模與驗(yàn)證進(jìn)行研究，繼而從時間行為角度出發(fā)，基于CCSL時序約束語言建立系統(tǒng)的時序行為需求模型，借鑒接口自動機(jī)的組合機(jī)理，通過樂觀方法定義時序行為的可組合性.給出時序行為的精化方法，同時通過L*方法來迭代學(xué)習(xí)模型的行為，并基于此實(shí)現(xiàn)針對時序行為的組合驗(yàn)證，以此形成自上而下、統(tǒng)一的開發(fā)框架.

2 時序行為建模及可組合性定義

2.1 CCSL建模

CCSL是用于描述系統(tǒng)中時序規(guī)約的半形式化語言，該語言定義了豐富的時間約束語義來對系統(tǒng)規(guī)約進(jìn)行表達(dá).比如優(yōu)先語義（precedence）：m＞n，定義了時鐘m的滴答次數(shù)要多于時鐘n的滴答次數(shù)，或者交替語義（alternative）：m～n，表達(dá)了時鐘m和時鐘n會交替滴答產(chǎn)生的約束關(guān)系.

CCSL規(guī)約語言的核心要素是邏輯時鐘，區(qū)別于能夠度量物理時間的物理時鐘，邏輯時鐘可以看作是能夠在設(shè)計(jì)階段對系統(tǒng)中任務(wù)的時序關(guān)系進(jìn)行表達(dá)的模型元素.本節(jié)首先描述一個邏輯時鐘的概念，再擴(kuò)展出系統(tǒng)中存在多個邏輯時鐘的時間結(jié)構(gòu)定義.

定義1.邏輯時鐘.采用5個標(biāo)簽〈I,?, D, τ, u〉結(jié)構(gòu)來進(jìn)行表達(dá).標(biāo)簽I為一系列事件的發(fā)生時刻，?為發(fā)生時刻序列I上的嚴(yán)格優(yōu)先（strict precedence），D是時鐘上的記號，通過函數(shù)τ進(jìn)行定義：τ∶I→D，u是時鐘遞增幅度.針對邏輯時鐘而言，遞增幅度u可以是系統(tǒng)滴答tick，也可以是總線的傳輸周期等.

定義2.時間結(jié)構(gòu).通過標(biāo)簽〈C, ?〉進(jìn)行表達(dá)，在時間結(jié)構(gòu)中，C為包括邏輯時鐘或度量時鐘的時鐘集合，?為這組時鐘上的先后約束關(guān)系.

可以看出，邏輯時鐘是一系列具有嚴(yán)格先后關(guān)系的時間點(diǎn)集合.通常用來描述某個事件在時間線上的一系列動作.2個時鐘之間最純粹、最本質(zhì)的關(guān)系是優(yōu)先（precedence）.從最基本關(guān)系出發(fā)，可以推出其他時序關(guān)系，如同時發(fā)生（coincidence）、嚴(yán)格優(yōu)先（strict precedence）、互相排斥（exclusive）等.

例1.假設(shè)存在2個時鐘c與d，2個時鐘的關(guān)系為：時鐘c與基準(zhǔn)時鐘延遲1個時間單位，并在之后以4為周期值進(jìn)行執(zhí)行（屬于subclock子時鐘約束的一種），而時鐘d與基準(zhǔn)時鐘延遲3個時間單位，之后同樣以4為周期值進(jìn)行執(zhí)行.通過CCSL語言進(jìn)行描述可以得到的關(guān)系為：

cisPeriodicOnclkperiod=4 offset=1,

disPeriodicOnclkperiod=4 offset=3.

在CCSL仿真工具Timesquare中對時序行為進(jìn)行模擬得出的執(zhí)行過程如圖2所示.執(zhí)行過程描述的3個邏輯時鐘的時序約束關(guān)系為：首先邏輯時鐘clk滴答，在其后產(chǎn)生的是邏輯時鐘c的滴答（offset=1），繼而，邏輯時鐘c以4為周期值進(jìn)行滴答.邏輯時鐘d以邏輯時鐘clk為基準(zhǔn)，同樣以4為周期值產(chǎn)生滴答，并且其偏移值為3（offset=3）.

Fig.2 Diagram of clocks relationship圖2 時鐘的關(guān)系圖

2.2 時序約束行為的組合與可組合性定義

在系統(tǒng)開發(fā)過程中需要對時序行為進(jìn)行建模及分析，本文依據(jù)文獻(xiàn)[27]所給方法通過遷移系統(tǒng)來刻畫CCSL，并采用組合推理方式對屬性進(jìn)行檢查.

定義3.時鐘遷移系統(tǒng)[27].可以通過一個在事件集A上的五元組A=（S，λ，α，β，Tran） 進(jìn)行表達(dá)，其中：

1）S為一組狀態(tài)節(jié)點(diǎn)，s0是初始節(jié)點(diǎn)；

2）λ∶Tran→A定義節(jié)點(diǎn)轉(zhuǎn)換過程中對應(yīng)的事件；

3）α，β∶Tran→S是映射函數(shù)，節(jié)點(diǎn)轉(zhuǎn)換中的起點(diǎn)和終點(diǎn)的節(jié)點(diǎn)；

4）Tran?S×2λ×S是描述轉(zhuǎn)移集合是節(jié)點(diǎn)之間轉(zhuǎn)換關(guān)系的子集，當(dāng)事件e?λ，則當(dāng)節(jié)點(diǎn)s到s’的所有觸發(fā)事件e都發(fā)生，并將產(chǎn)生該轉(zhuǎn)換.

描述時鐘m的行為Clockm=（S，λ，α，β，Tran），時鐘滴答集合為Am={m,ε}，則：

1）S={s} 邏輯時鐘m僅存在一個狀態(tài)；

2）Tran={t,e}是2個轉(zhuǎn)換過程，分別由時鐘m滴答和ε產(chǎn)生；

3）α（t）=α（e）=s，β（t）=β（e）=s，是2個轉(zhuǎn)換過程對應(yīng)的起點(diǎn)節(jié)點(diǎn)和終點(diǎn)節(jié)點(diǎn)；

4）λ（t）=m，λ（e）=ε，引起轉(zhuǎn)換的相應(yīng)事件.

圖3（a）是時鐘m的滴答轉(zhuǎn)換過程，圖3（b）是同步關(guān)系（mcoincidencen），以及圖3（c）是子時鐘關(guān)系（nis subclockofm）.

Fig.3 Clock ticking behaviors圖3 時鐘的滴答行為

同樣，通過遷移系統(tǒng)對圖2中的時鐘行為進(jìn)行建模，可以得到圖4所示結(jié)果.執(zhí)行的跡（trace）為{（c=0,d=0,clk=0），（c=1,d=0,clk=1），（c=0,d=0,clk=2），（c=0,d=0,clk=2），（c=0,d=1,clk=3），（c=0,d=0,clk=0），（c=1,d=0, clk=1）,…}.

Fig.4 Relationship diagram of timing constraint based on state transition圖4 基于狀態(tài)遷移的時序約束關(guān)系圖

在能夠表達(dá)一個時鐘的執(zhí)行過程后，需要對系統(tǒng)中存在的多個時鐘的約束行為關(guān)系進(jìn)行組合來描述整體，最直觀的方法是計(jì)算多個時鐘的笛卡兒積.

定義4.時鐘約束行為的組合.對于n個邏輯時鐘A1, A2,…,An，其同步行為是A1×A2×…×An的一個子集合I，則多個時鐘的約束行為組合可以描述為在動作子集I?A1×A2×… ×An上的時鐘遷移系統(tǒng)A=（S, λ,α, β, Tran），其中：

1）S=S1×S2×…×Sn，系統(tǒng)的全部狀態(tài)；

2）λ（〈t1,t2,…,tn〉）=〈λ（t1）,λ（t2）,…,λ（tn）〉，轉(zhuǎn)移過程的事件行為；

3）α（〈t1,t2,…,tn〉）=〈α（t1）,α（t2）,…,α（tn）〉，轉(zhuǎn)移過程的起始狀態(tài)節(jié)點(diǎn)；

4）β（〈t1,t2,…,tn〉）=〈β（t1）,β（t2）, …,β（tn）〉，一次轉(zhuǎn)移過程的目的狀態(tài)節(jié)點(diǎn)；

5）Tran= {〈t1, t2, …, tn〉∈T1×T2× …Tn|〈λ1（t1）,λ2（t2）,…,λn（tn）〉 ∈I}，是所有的轉(zhuǎn)移行為.

定義5.禁止?fàn)顟B(tài).2個系統(tǒng)M與N的乘積為AP×AQ，其禁止?fàn)顟B(tài)節(jié)點(diǎn)Forbidden（M, N）?SM×SN應(yīng)具有屬性：

其中AM（v）與AN（v）是系統(tǒng)M與系統(tǒng)N在組合后所得到的狀態(tài)v下所接受的事件集合.shared（M, N）表示M與N之間的共有動作.基于定義5，組件組合后，當(dāng)處于禁止?fàn)顟B(tài)下，M對事件e有轉(zhuǎn)移發(fā)生，而N對事件e沒有轉(zhuǎn)移發(fā)生，或兩者情況彼此相反，即，在禁止?fàn)顟B(tài)下，不能在同一時刻使得M與N一起產(chǎn)生轉(zhuǎn)移，稱為禁止?fàn)顟B(tài)節(jié)點(diǎn).

定義6.時序行為可組合.如果M和N有一個外部系統(tǒng)E，可以保證M和N在組合后禁止?fàn)顟B(tài)節(jié)點(diǎn)不可達(dá)，可得M和N是時序行為可組合的.

行為可組合的定義描述了系統(tǒng)在組合后的執(zhí)行行為并沒有改變原系統(tǒng)的執(zhí)行行為，確保了系統(tǒng)在集成前與集成后行為的一致性.基于這個基本檢查形式，可以對系統(tǒng)的行為進(jìn)行笛卡兒積的計(jì)算，并在此基礎(chǔ)上進(jìn)行模型檢查.本文給出圖5的示例進(jìn)行更具體的說明.

Fig.5 System behavior model圖5 系統(tǒng)行為模型

圖5（a）描述3個時鐘（observe,write,replace）的時序行為，首先時鐘observe滴答，之后是時鐘write滴答，該模型與圖5（b）模型組合后，形成了圖5（c）的模型.其中，圖5（a）模型中時鐘write滴答后期待響應(yīng)的是時鐘replace，而圖5（b）模型在產(chǎn)生時鐘write滴答后時鐘exec滴答，可能產(chǎn)生ok或nok，而在nok發(fā)生后將導(dǎo)致時鐘incorrect滴答，而該時鐘行為是圖5（a）模型不能接受的.因此，組件進(jìn)行組合后有可能進(jìn)入非法狀態(tài)Err，導(dǎo)致系統(tǒng)錯誤.因此組件是不可組合的.簡單而言，在組件組合后的狀態(tài)集合中，某狀態(tài)并不是所有組件都希望到達(dá)的，則該狀態(tài)稱為禁止?fàn)顟B(tài).

“死鬼，接招！看我無敵旋風(fēng)腳！”我一邊喊一邊把腳踢了出去。只見那些可憐的鬼還沒有反應(yīng)過來，就被我打倒在地了。哈哈！鬼被我打趴下了！我得意地大笑起來，準(zhǔn)備對付下一個目標(biāo)了。

本文將組件時序行為的可組合性描述為各個組件的時序行為在合并之后，如果能夠滿足組件原有的時序行為約束要求，則可以定義為時序行為可組合的.如圖6所示，系統(tǒng)給出了外部環(huán)境的執(zhí)行過程，外部環(huán)境讀入exec后，執(zhí)行內(nèi)部動作check，最后輸出ok告知系統(tǒng)結(jié)果.上述過程沒有時鐘incorrect滴答.可以看出，能夠存在一個子系統(tǒng)使得整體系統(tǒng)在組合后沒有進(jìn)入Err節(jié)點(diǎn)，則表明系統(tǒng)整體行為約束是具有可組合性的.

Fig.6 A legal external environment圖6 一個合法的外部環(huán)境

3 組件的時序行為可組合驗(yàn)證

在計(jì)算若干個組件行為的笛卡兒積后可以得到整體模型.為了驗(yàn)證屬性需要，對計(jì)算后的模型進(jìn)行檢查以驗(yàn)證其是否滿足時序行為可組合的要求.

3.1 組合驗(yàn)證框架

為了緩解模型組合后產(chǎn)生的狀態(tài)爆炸問題[28]，本文通過組合驗(yàn)證的方法對時序行為進(jìn)行檢查.組合驗(yàn)證基于分治的思想對個體模型的屬性進(jìn)行檢查來減少對整體狀態(tài)空間的搜索，以此緩解狀態(tài)爆炸問題.首先介紹最基本的推理規(guī)則.

假設(shè)-保證推理（assumption-guarantee reasoning,AGR）[29]：該范式包含元素〈A〉M〈P〉，其中，M是一個組件，P是一個屬性（可以用遷移系統(tǒng)表示），A是組件M的外部環(huán)境的假設(shè)條件.該推理規(guī)則描述組件M屬于某類系統(tǒng)，該類系統(tǒng)在滿足假設(shè)條件A的前提下，系統(tǒng)可以保證具有屬性P.如果系統(tǒng)是由組件M1和M2構(gòu)成，則描述推理形式為

該規(guī)則描述為：如果需要驗(yàn)證組件M1和M2在組合之后的整體行為能夠提供的保證為P，則首先得到組件M1在提供保證P時，外部環(huán)境需要滿足的假設(shè)行為A（上述規(guī)則中的步驟1），基于此，在推導(dǎo)出假設(shè)行為A后，則再檢查組件M2在默認(rèn)外部行為為true時，是否滿足假設(shè)條件A（上述規(guī)則中的步驟2），通過此方法對M1||M2是否滿足屬性P進(jìn)行驗(yàn)證.以此通過檢查局部狀態(tài)空間的方法，實(shí)現(xiàn)對整體狀態(tài)空間的搜索.通過組合驗(yàn)證的方法對得到外部環(huán)境應(yīng)具備的假設(shè)條件A，在本文中，我們通過L*方法對模型進(jìn)行推理學(xué)習(xí)，得到條件A.

為了獲得假設(shè)條件A，如圖7所示，驗(yàn)證框架采用迭代的方式進(jìn)行組合驗(yàn)證的推理.在每一次迭代過程中，基于上一輪得到的正確行為以及本輪的推導(dǎo)行為，給出假設(shè)條件Ai.首先通過步驟1判斷M1在外部系統(tǒng)為Ai時，是否能保證提供行為P，如果結(jié)果是false，其含義為假設(shè)行為Ai偏弱（Ai尚未對外部系統(tǒng)進(jìn)行足夠的限制，存在錯誤的行為導(dǎo)致屬性P不被滿足），因此，需要通過返回的反例對假設(shè)條件Ai進(jìn)行強(qiáng)化（對環(huán)境Ai的行為太過“寬容”，需要移除一些行為）.因此，在下一輪迭代過程Ai+1中，所學(xué)習(xí)得到的外部環(huán)境至少將上一輪迭代過程中破壞屬性P的反例行為給剔除掉.

Fig.7 Iterative based compositional verification framework圖7 基于迭代的組合驗(yàn)證框架

當(dāng)步驟1的返回值為true，則表明Ai的行為已經(jīng)足夠強(qiáng)化，能夠滿足屬性P.為了完成證明，步驟2需要判定在外部環(huán)境行為條件為true的情況下，M2是否能滿足屬性Ai，如果步驟2返回值為true，則表明組合驗(yàn)證成立，M1和M2的組合可以滿足保證具有行為P；如果返回值為false，則應(yīng)該分析M1||M2是否破壞了屬性P，或者Ai過于強(qiáng)化.如果Ai過于強(qiáng)化，則需要在第i+1次迭代時通過反例對其弱化，因此，至少在下一輪迭代的時候，這個反例中的行為將在假設(shè)條件Ai中被允許.

在具體工作中，本文基于L*方法來對外部環(huán)境應(yīng)具有的正確行為進(jìn)行學(xué)習(xí)，不斷嘗試去找出能夠讓模型M滿足屬性P的所有行為，以此利用得到的所有正確行為序列構(gòu)建出外部環(huán)境Ai.

3.2 基于L＊學(xué)習(xí)的時序行為可組合驗(yàn)證

L*學(xué)習(xí)早期被用于對正則表達(dá)式進(jìn)行規(guī)則推理[30]以得到符合行為要求的狀態(tài)機(jī).該推理給出一個虛構(gòu)身份——最小勝任教師（minimally adequate teacher），在具體過程中，方法通過迭代的方式向教師提出2個問題，分別為成員資格詢問（membership query）和候選者資格詢問（candidate query）.考慮到有些行為沒有時間語義，本文將具體的學(xué)習(xí)過程劃分為無時間語義推理與有時間語義推理2個階段.2個推理過程在整體流程上是類似的，都需要經(jīng)過“成員資格詢問”和“候選人資格詢問”2個查詢操作.而2個學(xué)習(xí)過程不同的是，無時間語義推理過程是一種對行為的不斷學(xué)習(xí)（查詢）的過程，而在有時間語義的行為推理中，需要不斷將全局時間進(jìn)行分解，不斷找出滿足屬性P的時間行為的過程.

1）無時間語義的推理過程

在對假設(shè)條件A進(jìn)行推理時，該方法先定義一個判定表（S,E,T），在這個表格中S列和E列表示所判定行為的前字符串序列和后字符串序列，最初，S列和E列都是空事件集{ε}.T列是經(jīng)過“教師”查詢后從字符串S∪S·Σ·E到{true, false}（或{1,0}）的計(jì)算值.判斷該字符串是否屬于正確行為，“·”的計(jì)算定義為：對于2個字符串m和n，M·N= {mn|m∈M , n∈N}，計(jì)算出字符串m和n序列動作.向“教師”查詢獲得結(jié)果后，將判定表中的T值進(jìn)行更新.（在算法1偽代碼中對應(yīng)的處理過程是行①～?）.

算法1.對時間進(jìn)行學(xué)習(xí)的L*算法.

輸入：事件集合Σ；

輸出：通過學(xué)習(xí)得到滿足時間行為的遷移系統(tǒng).

①S=E={ε}； / *初始化判定表中的集合 * /

②查詢ψm（ε），判斷是否屬于合法的行為，同時查詢ψm（ε·σ），更新判定表中的T值，其中σ∈Σ；

③ while true do

④ whileTF（s·σ·e）≠TF（s'·e） do

⑤S←S∪s·σ； / *將s·σ加入前綴集合S中 * /

⑥ end while

⑦ 通過前面判定表中學(xué)習(xí)得到的行生成相應(yīng)的遷移系統(tǒng)M；

⑧ ifψc（M）==1 then

⑨ returnM；

⑩ else

? updateT； / * 教師返回反例并對其進(jìn)行分析，得到后綴加入到集合E中，再次對判定表中的行為進(jìn)行查詢，更新T值 * /

? end if

? end while

?σ←（σ,true）；s←（s,true）；e←（e,true） ； / * 通過對無時間語義的行為進(jìn)行學(xué)習(xí)得到判定表（S,E,T），在該判定表中加入時間語義，其中，σ∈Σ, s∈S, e∈E* /

? 不滿足條件的情況下，給出反例（a1,g1） （a2,g2）…（an,gn） ；

? for （i= 1;i≤n;i++）

? …

? if （ai,g） 是p或e的子串，其中p∈S∪（S·Σt），e∈Ethen [gi]∩[g]≠?

? 將p分割為，其中（ai,gi）是pi的子串，（aj,gj）是pj的子串，j∈1,2,…,n;

? 將e分割為，其中（ai,gi）是ei的子串，（aj,gj）是ej的子串，j∈1,2,…,n；

? end if

? end for

? whileTF（s·σ·e）≠TF（s'·e） do

?S←S∪s·σ； / * 將s·σ加入到前綴集合S中，（s·σ·ε），更新T，其中ε∈Σt* /

? end while

? 得到封閉的判定表，生成Mt，將其提交至教師進(jìn)行候選人查詢（Mt） ；

? 如果返回false，則同時返回反例，對反例進(jìn)行分析并得到后綴加入到集合E中，不斷迭代學(xué)習(xí)得到假設(shè)條件Ai的模型Mt；

? end while

? returnMt.

上述偽代碼給出了對行為進(jìn)行學(xué)習(xí)的整體過程，最終得到了具有時間屬性的、滿足行為規(guī)則要求的模型Mt，接下來將結(jié)合偽代碼講解算法中的成員查詢過程和候選人查詢過程.

成員查詢.該階段將判斷字符組成的事件序列是否屬于正確的系統(tǒng)該接受的行為.計(jì)算可得，事件序列為σ=〈a1,a2, …,an〉，σ∈Σ，Σ是事件集合.“教師”驗(yàn)證模型〈Aσ〉M1〈P〉.當(dāng)其值是true時，則成員查詢函數(shù)ψm（ε·σ）=1，判定表中T值也為1，表明該事件序列沒有在M1中影響行為P，應(yīng)屬于正確的事件行為序列.如果ψm（ε·σ）=0，則返回值為false，同時判定表中T值為0，并給出一個負(fù)反例，該反例屬于當(dāng)前Ai中的事件行為序列，卻破壞了屬性P，因此對反例分析后再將該行為剔除掉，得出前字符串并加入判定表的集合S中.向教師提交事件序列進(jìn)行查詢，并同步更新對應(yīng)的T值（算法1中行②）.最后，通過公式來查看判定表是否為封閉的（行④）：

?s∈S, ?a∈Σ, ?s'∈S, ?e∈E:TF（sa·e）=TF（s'e）.

候選人查詢.通過成員查詢過程判斷判定表是否是封閉的（算法1中行④～⑥）.如果是封閉的，則依據(jù)判定表生成遷移系統(tǒng)M.其中，遷移系統(tǒng)的狀態(tài)是前序字符串集S中的元素，s0=ε，動作λ=Σ為事件集合（算法1中行⑦）.通過候選人查詢函數(shù)ψc（M）進(jìn)行查詢，如果返回值為true，則證明M1||M2能夠保證屬性P（算法1中行⑧⑨）；否則如果模型檢查返回false，則同時返回一個正反例（counter- example），該正反例描述了其所表示的事件序列能夠滿足屬性P，卻不在Ai中，表明所得到的條件Ai對事件行為進(jìn)行了過度的約束，應(yīng)將正反例行為加入到Ai中，再分析正反例得出后綴并加入到判定集合E中，并向教師提交字符序列進(jìn)行查詢，并更新T（算法1中行?）.

本節(jié)給出針對前述示例1行為的學(xué)習(xí)過程，初始階段判定表為空，逐步添加事件行為的前、后字符串序列來對判定表進(jìn)行創(chuàng)建， 得到判定表T-1（表1）和判定表T-2（表2）.在計(jì)算M的判定表時，需要先確定M的事件集，具體地，前序字符串為S={ε}，后序字符串為E={ε}，事件集為Σ={c,d}，向“教師”提交整合后的字符串并查詢，判斷該字符串序列是否屬于所要學(xué)習(xí)的模型行為，如果屬于，就將判定表中對應(yīng)的T賦值為1，如表1所示.

Table 1 The Observation Table T-1 of Model M表1 模型M的判定表T-1

Table 2 The Observation Table T-2 of Model M表2 模型M的判定表T-2

再次按照算法1中行④所給出規(guī)則來檢測判定表是否封閉，發(fā)現(xiàn)不存在s'滿足公式T（s·c·e）=T（ε·c·ε）.則判定表T-1不封閉，并將c添加至字符串集S中，更新T值，如表2所示.

再次檢查判定表的封閉情況，如封閉，則將其轉(zhuǎn)換為遷移系統(tǒng)，并發(fā)送給“教師”判斷該模型是不是正確的假設(shè)條件，“教師”返回false，并提供反例序列σ=cdd.此行為是被Ai認(rèn)可的事件序列，但不是正確的學(xué)習(xí)結(jié)果.因此需要在判定表中更新、計(jì)算后序字符串為d.修改判定表，依此過程進(jìn)行推導(dǎo)，最終得到滿足條件的判定表T-3.

計(jì)算得到判定表T-3是封閉的，由表3可得出，所學(xué)習(xí)到的模型包括4個狀態(tài)s0，s1，s2，s3，狀態(tài)s0接收到時鐘c滴答后遷移至狀態(tài)s2，圖8展示了所有遷移的路徑關(guān)系，建模了時鐘c與d的約束行為.

Table 3 The Observation Table T-3 of Model M表3 模型M的判定表T-3

Fig.8 Learning results without timing semantics圖8 無時間語義的學(xué)習(xí)結(jié)果

2）有時間語義的推理過程

對時間屬性進(jìn)行推理的過程也可以理解為是對無時間語義行為進(jìn)行精化的過程.首先要做的是將無時間語義事件集Σ轉(zhuǎn)換為描述時間語義的事件集ΣT=Σ×GΣ.基于類似的操作，判定表也會變?yōu)橛袝r間語義的判定表（算法1中行?）.具體地，對于時間語義行為的推理過程為：

①通過算法1中行①～?可以生成一個缺少時間語義的假設(shè)條件Ai，再把Ai交給函數(shù)ψc（M）進(jìn)行判定（算法1中行?～?）.

②當(dāng)函數(shù)ψc（M）的判定結(jié)果為false，會一同給出一個錯誤的行為（反例），如 （a1,g1），（a2,g2），…，（an,gn）（第2個元素g1，g2，…，gn是事件a1，a2，…，an產(chǎn)生的時序約束），需要對這個錯誤行為進(jìn)行分析并進(jìn)一步地分割事件流，檢查判定表中前字符串S和后字符串E在時間屬性上是否包含（ai,g），并滿足[gi]∩[g]≠?，則時序?qū)傩訹g]被gi分割成[g]=[gi]∪G.在這樣的方式下，前字符串序列S將被分割為，具體地，元素（ai,g0）刻畫了，元素（ai,gj）刻畫了S?j.同樣，判定表中后字符串序列E也被分割為，元素（ai,gi） 刻畫了， 元素（ai,gj） 刻畫了， 其中j∈{1,2,…,m}.在這個階段，基于對時間屬性的分割把無時間語義的事件分解為多個具有時間語義的事件結(jié)構(gòu)，再將事件流提交給函數(shù)進(jìn)行檢查，其形式為，其中j∈{1,2,…,m}，再對判定表中的T值進(jìn)行更新（算法1中行?～?）.

③依據(jù)行?～?將得到更為具體的判定表，并再檢查其封閉性.對于前字符串序列s·a，如果沒有發(fā)現(xiàn)某個s'∈ Σt，滿足s·a≡s′，則定義這個判定表不封閉.這樣就要把s·a添加進(jìn)集合S，再利用函數(shù)（s·a·ε）重新對判定表中T賦值（算法1中行??）.

④當(dāng)判定表是封閉的，再把判定表轉(zhuǎn)換為遷移系統(tǒng)Mt，并通過函數(shù)（Mt）檢查其是否滿足屬性要求，如果Mt不是正確的學(xué)習(xí)結(jié)果，則將給出反例修訂判定表，再次迭代學(xué)習(xí)，直至得到所學(xué)習(xí)到的正確的模型Mt（算法1中行?）.

如下對2.1節(jié)中例1進(jìn)行時間屬性學(xué)習(xí)的過程描述.首先對第1階段（無時間語義的行為推理過程）得到的判定表進(jìn)行時間屬性的賦值，如表4所示.

Table 4 The Observation Table T-4 of Model M表4 模型M的判定表T-4

在判定表T-4中，Σt= {（c,true）,（d,true）}，St={（ε,true）,（c,true）,（c,true）,（d,true）,（d,true）,（d,true）}，同時后序字符串序列Et={（ε,true）,（d,true）}.可以把判定表 T-4轉(zhuǎn)換為假設(shè)條件，并再把交給函數(shù)ψc（M）進(jìn)行檢查，如其值為false，則會提供一個破壞屬性的行為：σ={（c=1,clk＞1）（d=1,clk＞1）}；然而當(dāng)判定表中S={（c,true）（d,true）}，則判斷時間屬性的有效值：|(clk＞1)(clk＞1)|∩|(true)(true)|≠?，并把前后字符串序列的時間約束進(jìn)行分解，事件c和d的時間約束分別分解為（c,clk＜1）和（c,clk＞1），同時（d,clk＜1）和（d,clk≥1），再次利用判定表得出事件序列，并提交給函數(shù)（Mt），獲得T值，可得表5中的判定表T-5.

Table 5 The Observation Table T-5 of Model M表5 模型M的判定表T-5

不斷對模型進(jìn)行學(xué)習(xí)，能夠形成封閉的判定表T-5，通過判定表T-5可以得到圖9中的假設(shè)條件Ai（轉(zhuǎn)換為模型M）.

Fig.9 Assumption Ai derived from reasoning圖9 推理得到的假設(shè)條件Ai

L*算法的正確性.L*算法通過對模型M的行為進(jìn)行學(xué)習(xí)推算得到一個擁有最少狀態(tài)集的系統(tǒng)TS.首先，L*算法在推導(dǎo)階段的每個迭代過程中得到的模型在狀態(tài)數(shù)量上是增長的，每輪迭代過程所得到的模型中狀態(tài)數(shù)量都比上一輪迭代過程中的狀態(tài)數(shù)量多.究其原因，判定表中所給出的前序字符串S就是所推導(dǎo)出模型的狀態(tài)集合，所得到的模型應(yīng)該有數(shù)量為|S|的狀態(tài)節(jié)點(diǎn)，而在學(xué)習(xí)過程中，在得到正確的模型之前，每輪迭代所得到的模型都是錯誤的，因此，每輪迭代所得到的狀態(tài)數(shù)量都是最少的，直到學(xué)習(xí)到了正確的行為，這樣，在學(xué)習(xí)到一個行為正確的模型時，這個模型包含最少數(shù)量狀態(tài)的狀態(tài)集合.而在猜測次數(shù)上，假設(shè)模型有n個正確的狀態(tài)，算法將作出n-1次候選人查詢.

4 組件的時序行為精化方法

精化實(shí)現(xiàn)了對系統(tǒng)規(guī)約逐步具體化的操作過程[31].為了建立具體時序行為模型，本文通過CCSL時序約束語言建立上層時序模型，并對3種典型的時序規(guī)約實(shí)現(xiàn)精化.本文給出精化關(guān)系定義7.

定義7.時序約束關(guān)系的精化.如果模型K=(SK,s0K,ΣK,→K)與模型L=(SL,sL0,ΣL,→L)存在精化關(guān)系，描述成K?L，表示為具有關(guān)系R?SK×SL，（sK0,s0L）是初始狀態(tài)節(jié)點(diǎn)，對于所有節(jié)點(diǎn)(s,t)∈R，屬性成立：如果其中(k′,l′)∈R,k′∈SK；

定義7定義了2個模型（K和L）滿足精化條件(K?L)，模型K和L具有關(guān)系(R?SK×SL)，其中，在某個狀態(tài)節(jié)點(diǎn)（K,L）下所有事件c1,c2,…,cn發(fā)生，在L中產(chǎn)生轉(zhuǎn)移同樣動作〈c1,c2,…,cn〉下模型K中產(chǎn)生轉(zhuǎn)換則稱模型K和L滿足精化條件.

精化過程實(shí)現(xiàn)了從較高層級模型到低層級模型的過渡與轉(zhuǎn)換.高層模型表達(dá)了系統(tǒng)需求層的時序關(guān)系，低層模型可以表達(dá)更為具體的系統(tǒng)任務(wù)級的時序關(guān)系[32].為了構(gòu)建上層時序規(guī)約，本文以3種基本的時序約束需求作為基礎(chǔ)來建立規(guī)約模型并進(jìn)行精化.3種約束關(guān)系分別為：

1）延遲約束.考慮系統(tǒng)讀入某個數(shù)據(jù)，然后內(nèi)部任務(wù)計(jì)算反饋數(shù)據(jù)，并再把反饋數(shù)據(jù)進(jìn)行輸出的時間區(qū)間.假設(shè)某組件在時刻m讀取外部控制命令，經(jīng)過本地控制任務(wù)處理得到反饋信息，并在時刻n寫入外部緩存，同時限定整體處理時限為t，類似這樣的約束關(guān)系可以采用CCSL中的n-m＜t進(jìn)行描述.

2）關(guān)聯(lián)約束.考慮組件中的某個輸出動作，追溯到所有與其相關(guān)的輸入動作，則關(guān)聯(lián)約束刻畫所有輸入事件的同步關(guān)系，可以利用時序約束語言CCSL中最小上界inf（）和最小下界sup（）進(jìn)行刻畫.

3）間隔約束.在某系統(tǒng)中，限定輸出事件的產(chǎn)生在某個時間范圍內(nèi)稱為間隔約束.如某示例，“汽車制動指令將在20～50 ms之間產(chǎn)生”，類似約束可以在CCSL中使用min＜n-m＜max關(guān)系進(jìn)行刻畫.

刻畫任務(wù)在執(zhí)行過程中的前后順序依賴關(guān)系是精化過程的基礎(chǔ)，為了刻畫依賴約束，本文將通過任務(wù)圖來建立時序行為需求規(guī)約與任務(wù)模型之間的關(guān)系.

4.1 任務(wù)圖結(jié)構(gòu)

利用任務(wù)圖G（U，V，N）結(jié)構(gòu)可以刻畫任務(wù)之間的優(yōu)先順序，其包括基本元素：

1）U表示圖中節(jié)點(diǎn)，V表示圖中的邊，N={τ1,τ2,…,τn}描述任務(wù)；

2）更為重要的是，每個任務(wù)具有相應(yīng)的特征，Ti為任務(wù)的執(zhí)行周期，任務(wù)的初始相位Pi應(yīng)大于0，任務(wù)執(zhí)行的時限D(zhuǎn)i應(yīng)大于Pi，同樣，任務(wù)應(yīng)具有最差執(zhí)行時間ei的屬性，在各屬性中，[Pi, Di]時間段刻畫了任務(wù)可調(diào)度運(yùn)行的區(qū)間Wi（Wi=Di-Pi）.

3個屬性Ti，Pi，Di描述了任務(wù)τi的時間行為，本文將對其進(jìn)行逐步求精推算.

對時序行為進(jìn)行精化的過程如算法2所示，針對時序行為進(jìn)行精化的方法包含3個步驟：

1）算法初始化過程.羅列需求（如給出系統(tǒng)的幾種時序行為需求、建立任務(wù)圖等）（算法2的行①）、給出任務(wù)圖、描述時間約束（timing constriant, TC）、定義若干變量（主要為任務(wù)周期、任務(wù)的截止時間，以及任務(wù)的初始相位等）.

2）時間屬性細(xì)化過程.通過約束關(guān)系將任務(wù)的時間屬性進(jìn)行細(xì)化，得到任務(wù)時間屬性的解空間，再通過變量消除方法消除相位Pi以及截止時間Di，得到僅有任務(wù)周期Ti的約束關(guān)系，同時使用利用率進(jìn)行周期值的計(jì)算，得到任務(wù)的屬性值（算法2的行②③）.

3）推導(dǎo)出任務(wù)若干時間屬性的過程.得到任務(wù)周期值后，通過啟發(fā)式方法對相位Pi以及截止時間Di（算法2的行⑤～⑩）.

算法2.時序行為的精化方法.

輸入：時序約束需求模型；

輸出：精化后的時序約束任務(wù)模型，周期Ti，任務(wù)實(shí)現(xiàn)Di，相位Pi.

① 給出系統(tǒng)任務(wù)圖結(jié)構(gòu)G，描述系統(tǒng)中任務(wù)τ1,τ2,…,τn之間的依賴關(guān)系；

② 根據(jù)任務(wù)圖以及需求中的時序約束關(guān)系，通過任務(wù)之間的步調(diào)協(xié)同約束關(guān)系、延遲約束關(guān)系、間隔約束關(guān)系等，推導(dǎo)出任務(wù)參數(shù)Ti，Di，Pi的整體解空間S；

③ 消除解空間中的變量Di，Pi，將S映射到只有周期變量的子解空間；

④ 在得到周期值后，通過啟發(fā)式方法求得相位值與截止時間；

⑤ fork=0 →n-1 do

⑥Pk=0； / * 設(shè)置Dk為所有任務(wù)中最大的周期值，初始化任務(wù)的相位、截止時間 * /

⑦ forj=k+1 →n-1 do

⑧ ifτj?τkthen

⑨Pj=Dk,Dj≤Pj； / *具有優(yōu)先關(guān)系的任務(wù)，其相位值等于（或大于）前序任務(wù)的截止時間，進(jìn)一步得到二者之間的關(guān)系 * /

⑩ end if

? end for

? end for

? 目標(biāo)力爭最小化任務(wù)的相位值，最大化任務(wù)的截止時間，以此最大化任務(wù)利用率，得到Pi與Di的解空間，求得最優(yōu)值；

? returnTi,Pi,Di.

針對時序行為進(jìn)行逐步求精，本質(zhì)是將上層的時序規(guī)約轉(zhuǎn)換為底層具體實(shí)現(xiàn)的過程，為了滿足行為的一致性，轉(zhuǎn)換過程應(yīng)保證3方面的特性要求：

1）正確性.將精化后任務(wù)層的時序關(guān)系描述為TC，其次假定δ是系統(tǒng)的上層時序約束規(guī)約，在此定義下轉(zhuǎn)換出的 TC需要能夠滿足δ的要求.

2）可行性.通過精化方法可以得到任務(wù)的若干時間屬性，如周期、相位等，而在此時間屬性下，需要保證所有任務(wù)調(diào)度執(zhí)行的可行性，同時在所有任務(wù)運(yùn)行的情況下，資源利用率應(yīng)小于1.

3）可組合性.通過精化過程能夠推導(dǎo)出任務(wù)模型（周期、相位等），同時該任務(wù)模型能夠滿足系統(tǒng)時序規(guī)約的要求，可以得到多個子系統(tǒng)（組件）之間的時序行為是可以進(jìn)行組合的.

4.2 約束關(guān)系的處理

任務(wù)之間的傳輸數(shù)據(jù)要盡量能夠保持?jǐn)?shù)據(jù)傳輸步調(diào)的協(xié)同性.發(fā)送端和接收端的速率過于雜亂不利于數(shù)據(jù)的處理.如圖10中的示例，發(fā)送端和接收端具有一定的協(xié)同性，任務(wù)τ2可以容易地處理接收任務(wù)τ1的數(shù)據(jù)，因?yàn)槿蝿?wù)τ1的發(fā)送周期P1=10 ms，而任務(wù)τ2的接收周期P2=30 ms，則任務(wù)τ2每隔3個時間間隔對數(shù)據(jù)進(jìn)行接收（忽略掉2個），可參見圖10示例.

Fig.10 Task behavior with harmonious relationship圖10 具有協(xié)同關(guān)系的任務(wù)行為

定義8.任務(wù)周期的協(xié)同性.考慮2個或多個任務(wù)之間具有先后順序的依賴關(guān)系，在這種情景下，如果周期之間存在倍數(shù)關(guān)系，則稱任務(wù)之間是具有周期協(xié)同性的.假設(shè)任務(wù)為τ1和τ2，相應(yīng)的周期值為T1和T2，2個周期值具有關(guān)系：T2=KT1（K∈ ?+），則2個任務(wù)的執(zhí)行周期是具有協(xié)同關(guān)系的（T2|T1）.在圖11的任務(wù)圖結(jié)構(gòu)可給出約束關(guān)系：

Fig.11 Timing relationship of task chain圖11 任務(wù)鏈的時序關(guān)系

針對具有共同輸入事件的2個或多個任務(wù)而言，其輸入行為將影響2個或多個任務(wù)，假設(shè)存在任務(wù)τ1和τ2，任務(wù)具有共同的輸入行為I2，而2個鏈路的寫入外部環(huán)境事件分別為O1和O2，為了簡便起見，可以把2個數(shù)據(jù)輸入行為進(jìn)行合并.在圖11中，存在2個任務(wù)鏈路都包含輸出到外部環(huán)境的事件Y2，在這種情況下，可以把相應(yīng)的同步輸入行為{I1,I2,I3}統(tǒng)一合并為任務(wù)τs.并結(jié)合任務(wù)的時間屬性給出式（2）的定義：

其中，Jcorrd表示多個任務(wù)鏈路中輸入行為的最大抖動時間.

定義9.延遲約束的處理.F（O|I）=tf定義了這樣的約束關(guān)系：為了保證任務(wù)在時間t內(nèi)把寫入外部環(huán)境的事件O執(zhí)行完成，參與這個輸出值計(jì)算的全部輸入數(shù)據(jù)事件I應(yīng)該早于t - tf的時間到達(dá).

這個過程涉及到從輸入到輸出的整條任務(wù)鏈，而整條任務(wù)鏈中的時間行為將具體涵蓋每個任務(wù)的任務(wù)計(jì)算處理時間以及數(shù)據(jù)傳輸過程所用時間.其中，任務(wù)的計(jì)算處理時間描述任務(wù)具體代碼段在特定平臺上的運(yùn)行時間；而任務(wù)的數(shù)據(jù)傳輸過程所用時間涉及到任務(wù)在整條鏈路的執(zhí)行過程中由于等待數(shù)據(jù)輸入產(chǎn)生的延遲時間.在本質(zhì)上，應(yīng)該讓等待任務(wù)輸入數(shù)據(jù)的時間盡量減小，而對于前面所給出的任務(wù)同步輸入行為的處理，恰恰能夠解決該問題，使多個輸入任務(wù)的處理時間達(dá)到最優(yōu).

系統(tǒng)中任務(wù)的處理流程通常呈現(xiàn)鏈路路徑的形式，比如τ1,τ2,…,τn，在該路徑中τn是最終寫入外部環(huán)境的任務(wù)，τ1是最初從外部環(huán)境讀入數(shù)據(jù)的任務(wù)，相應(yīng)的周期是T1,T2,…,Tn，從任務(wù)的協(xié)同性考慮，得到關(guān)系式Ti+1|Ti（1≤i＜n）.比如考慮圖11中有3個任務(wù)τ1,τ2,τ3，如果從協(xié)同性上考量可以得到T3|T2以及T2|T1.

其次，從整體任務(wù)或部分任務(wù)的輸入輸出行為上考量，可以得出的關(guān)系式為：

基于任務(wù)的時間行為屬性，同樣可以得到一些基本的時間約束關(guān)系，比如基于任務(wù)的優(yōu)先順序可以得到關(guān)系式Di≤Pi+1（1≤i＜n），描述了第i個任務(wù)結(jié)束后，第i+1個任務(wù)可以開始執(zhí)行.

定義10.間隔約束關(guān)系的處理.該時間約束描述了2個連續(xù)輸出的相同事件在時間屬性上的關(guān)系，類似例子所描述的“控制指令的輸出需要在3～13 ms之內(nèi)完成”，描述了控制指令最短在3 ms時輸出完成，最長在13 ms時輸出完成，則可以分別表達(dá)為：l（O）=3和u（O）=13.

如圖12所示，在任務(wù)的執(zhí)行過程中涉及多個與時間約束相關(guān)的時間屬性值，其中包括任務(wù)執(zhí)行的初始時間點(diǎn)位置（相位Pi）和描述任務(wù)執(zhí)行結(jié)束的時間點(diǎn)位置（時限D(zhuǎn)i）.

Fig.12 The timing behavior of separation constraint圖12 具有間隔約束的時序行為

在此基礎(chǔ)上可以結(jié)合任務(wù)的時間行為屬性給出具體的約束關(guān)系式，即當(dāng)?shù)趇個輸出事件盡量早發(fā)生，第i+1個輸出事件盡量晚發(fā)生時，該情景下產(chǎn)生輸出事件的最大的間隔輸出時間；當(dāng)?shù)趇個輸出事件盡量晚發(fā)生時，第i+1個輸出事件盡量早發(fā)生時，該情景下將產(chǎn)生輸出事件最小的間隔輸出時間.相應(yīng)約束關(guān)系為：

在描述任務(wù)的時間行為約束關(guān)系時，除去基本的任務(wù)執(zhí)行周期、相位等時間元素，任務(wù)在執(zhí)行中的計(jì)算時間上界e同樣是比較關(guān)鍵的建模內(nèi)容.可以建立任務(wù)的執(zhí)行時間ei、相位Pi以及截止時間Di之間的關(guān)聯(lián).

同理，將上述關(guān)系擴(kuò)展到多個任務(wù)的情景，能夠推導(dǎo)出如式（6）的約束表達(dá)（其中，E=e1+e2+…+en）.

4.3 約束關(guān)系的推導(dǎo)

針對某系統(tǒng)，能夠通過式（1）～（5）得出任務(wù)的時序約束關(guān)系表達(dá)式集合，在此基礎(chǔ)上對式（1）～（6）進(jìn)行推導(dǎo)得出具體的變量值.相關(guān)流程為：

1）通過式（1）～（6）能夠得到系統(tǒng)整體的時序約束關(guān)系集合S，剔除其中的相位與截止時間，得到僅涉及任務(wù)周期值Ti的時序約束集合；

3）將步驟2）中計(jì)算得到的Ti代入最初的時序約束S，在此情況下將生成僅關(guān)于相位和截止時間的關(guān)系集合，進(jìn)一步利用線性關(guān)系對相位和截止時間屬性值進(jìn)行最終推導(dǎo).

4.3.1 變量消除方法

在對時間屬性值進(jìn)行推導(dǎo)的過程中需要不斷地對變量進(jìn)行消除.本文利用傅里葉-莫茨金消元法[33]來對變量進(jìn)行消元，將關(guān)系式中的若干元素（周期、相位等）有限次地變換，消去其中的某些元素.當(dāng)存在若干元素x=（x1,x2,…,xn），且多個元素之間滿足的關(guān)系為：

為了通過消元來計(jì)算每個元素的值，需要進(jìn)一步推導(dǎo)出元素之間的關(guān)系，具體給出的關(guān)系式為：

再對xˉ進(jìn)行處理，能夠給出如式（10）所示的取值范圍空間.

假設(shè)某個例子，相位和截止時間之間的關(guān)系為P4≥D4+18，P4≤31-D4，通過式子轉(zhuǎn)移將P4進(jìn)行消除，得到的關(guān)系式為：

限定取值范圍為正整數(shù)，則D4相應(yīng)的取值范圍為{1,2,…,7}.

在計(jì)算任務(wù)的周期Ti時，依據(jù)前面給出的優(yōu)先順序約束，以及任務(wù)執(zhí)行周期Ti的協(xié)同性等基本限定，同時，任務(wù)執(zhí)行應(yīng)保證資源利用率的限制，得：

基于此，建立系統(tǒng)的任務(wù)結(jié)構(gòu)圖能夠確定時序規(guī)約和底層時序行為之間的推演關(guān)系，通過式（1）～（11）能夠確定基本的任務(wù)模型解空間.進(jìn)一步對周期值進(jìn)行限定，能夠細(xì)化取值范圍并最終確定最優(yōu)的任務(wù)執(zhí)行周期Ti.

4.3.2 相位和截止時間推算方法

通過前面的計(jì)算過程能夠推導(dǎo)出周期的取值范圍，并最終求得最優(yōu)解.將所得到的周期值代入式（1）～（11）中能夠得到關(guān)于相位Pi和截止時間Di的關(guān)系式.對相位和截止時間的推導(dǎo)可以基于貪心算法完成，其原則為，在任務(wù)可調(diào)度的前提下，使得運(yùn)行窗口盡可能大，則要求Di值盡可能大，而使得相位的取值盡可能小.依據(jù)此規(guī)則來對這2個值進(jìn)行推導(dǎo).

5 實(shí)驗(yàn)分析

為了對方法進(jìn)行性能評估，本文開展了2個實(shí)驗(yàn).第1個仿真實(shí)驗(yàn)評估了精化方法的性能，第2個實(shí)驗(yàn)通過智能小車示例評估模型的組合，驗(yàn)證方法的性能.

5.1 精化方法性能分析

為了對精化方法的性能進(jìn)行評估，本文對比了多種將需求規(guī)約轉(zhuǎn)化為實(shí)現(xiàn)模型的精化方法，主要從2個角度分析性能：1）精化的擴(kuò)展性通過具體分析精化過程所用時間得到；2）生成任務(wù)集的效能通過相同約束場景下生成的任務(wù)數(shù)量進(jìn)行評估.表6給出了相關(guān)的實(shí)驗(yàn)設(shè)置.

Table 6 Scenario of Experiment表6 實(shí)驗(yàn)場景

與當(dāng)前多數(shù)針對CPS的建模與精化的工作類似，為了全面評估精化方法的性能，本文與2種具有代表性的關(guān)鍵方法進(jìn)行對比：1）UML-RT方法.該方法通過擴(kuò)展UML語義和通過封裝體（capsule）、端口（port）與連接器（connector）等元素建立系統(tǒng)的靜態(tài)與動態(tài)模型，最終轉(zhuǎn)化為任務(wù).2）Shige方法.通過建立時間需求模型，并對時間行為進(jìn)行分解與合成等操作，生成系統(tǒng)任務(wù).

精化過程的性能評估涉及到支持模型數(shù)量多少的問題，可將其定義為模型精化方法的可擴(kuò)展性.在進(jìn)行評估時通過整體精化過程中相同模型轉(zhuǎn)化為底層具體實(shí)現(xiàn)模型時所調(diào)用的代碼行數(shù)來進(jìn)行評判.代碼行數(shù)體現(xiàn)不同方法對于解空間集合進(jìn)行搜索求解時的性能及效率，是擴(kuò)展性的體現(xiàn).相關(guān)統(tǒng)計(jì)數(shù)據(jù)可見圖13，在對相同模型進(jìn)行精化的前提下，本文方法和UML-RT方法相比較，平均可降低0.11次迭代次數(shù)；與Shige方法相比，平均可降低3.16次迭代次數(shù)（迭代次數(shù)取自然對數(shù)）.

Fig.13 Computation on of iterations of different refinement algorithms圖13 不同精化算法的迭代次數(shù)對比

另一個重要的性能分析指標(biāo)是精化方法的有效性，本文依據(jù)精化方法所生成任務(wù)模型的任務(wù)數(shù)量來對其進(jìn)行評估.在相同的需求場景下，生成任務(wù)數(shù)量越少，任務(wù)切換及調(diào)度代價越小則精化方法表現(xiàn)越好.在操作過程中，分別給出不同的場景需求，將利用率劃分為0.75 /0.85/ 0.95（低/中/高），同時對系統(tǒng)的時序需求規(guī)約進(jìn)行隨機(jī)生成（端到端延遲、任務(wù)執(zhí)行時間等）.

圖14給出不同精化方法在限定組件數(shù)量的前提下，隨機(jī)生成系統(tǒng)的時序需求規(guī)約，并通過不同精化方法得到任務(wù)模型中任務(wù)數(shù)量的對比.由于對資源利用率的限定，不同精化方法生成的任務(wù)數(shù)量也存在差異，統(tǒng)計(jì)數(shù)據(jù)可見，本文所給方法在滿足利用率要求的前提下，所構(gòu)建任務(wù)數(shù)量相對較少.同時在系統(tǒng)組件個數(shù)分別為12和16的場景下，組件為16時精化后任務(wù)集的利用率相對更低.本文方法可以在保證時序約束的前提下，系統(tǒng)資源利用率可提升約15.22%.

Fig.14 Comparison of the number of tasks generated by refinement圖14 精化生成的任務(wù)數(shù)量對比

5.2 組合驗(yàn)證方法的實(shí)驗(yàn)及性能評估

本文通過實(shí)現(xiàn)智能主從小車系統(tǒng)來對組合驗(yàn)證方法進(jìn)行性能評估.該系統(tǒng)由手柄端、主車端以及從車端組成，其執(zhí)行過程為：首先，手柄端發(fā)送操作命令至主車端，主車端收到命令后，對數(shù)據(jù)進(jìn)行解析并執(zhí)行具體操作.主車端也將自身信息發(fā)送至從車端，使得從車端執(zhí)行跟車等動作.對時間行為約束關(guān)系進(jìn)行分析，最為關(guān)鍵的時間屬性是端到端的時間約束關(guān)系.如表7所示的具體規(guī)約主要定義3種時間約束行為：1）主車端內(nèi)部任務(wù)流延遲.從接收到手柄端控制命令開始到發(fā)送至控制單元的控制流時間延遲.2）主從車端傳輸延遲.主車端需要將自身的速度、姿態(tài)等信息數(shù)據(jù)發(fā)送給從車端，并將操作指令輸出到從車端執(zhí)行單元的時間延遲.3）從車端內(nèi)部任務(wù)流延遲時間.由從車端采集自身的速度、姿態(tài)等信息，經(jīng)過計(jì)算后發(fā)送到從車端執(zhí)行控制單元所用的時間.

Table 7 Requirement Description of End-to-End Delay表7 端到端延遲的需求描述ms

從時序約束行為的角度出發(fā)，通過構(gòu)件化的方法對系統(tǒng)進(jìn)行設(shè)計(jì)和開發(fā).首先建立任務(wù)之間的優(yōu)先順序結(jié)構(gòu)圖，同時給出具體的需求規(guī)約模型（部分如圖15所示）用于后續(xù)組件時間行為的可組合驗(yàn)證.

Fig.15 Behavior requirement model of delay constraint relationship in automotive system圖15 智能車系統(tǒng)中延遲約束關(guān)系的行為需求模型

在圖16中，任務(wù)τ1建模手柄的操作命令發(fā)送到主車，主車讀取數(shù)據(jù)的行為；任務(wù)τ2建模了主車采集自身速度、位置等數(shù)據(jù)的行為；任務(wù)τ4建模了主車自身的內(nèi)部任務(wù)，對速度、方向等數(shù)據(jù)進(jìn)行計(jì)算，并發(fā)送到控制單元的行為；任務(wù)τ5建模了讀取姿態(tài)、速度等信息，并發(fā)送給從智能車的行為；任務(wù)τ3建模了從智能小車獲取傳感器姿態(tài)、位置等信息的過程；任務(wù)τ6建模了對控制命令計(jì)算后，發(fā)送到組件O2的過程.

Fig.16 Task structure diagram of automotive system圖16 智能小車系統(tǒng)的任務(wù)結(jié)構(gòu)圖

得到系統(tǒng)的任務(wù)結(jié)構(gòu)圖后，依據(jù)式（5）（6）可以得到表8中的任務(wù)-時間屬性關(guān)系式.

Table 8 Timing Behavior Relationship deduced from Task Link表8 任務(wù)鏈路推導(dǎo)的時間行為關(guān)系

將變量（周期、相位、截止時間等）和常量（任務(wù)的執(zhí)行時間）代入任務(wù)-時間屬性的關(guān)系式，依據(jù)傅里葉-莫茨金消元法，由式（8）～（10）消除特定變量元素并推導(dǎo)出時間屬性的最優(yōu)值，如表9所示.

Table 9 Determination of Task Time Properties表9 任務(wù)時間屬性的確定

如表9所示，對任務(wù)進(jìn)行精化后可以得到具體的任務(wù)結(jié)構(gòu)（包括任務(wù)執(zhí)行周期、截止時間等）.得到任務(wù)的基本時間屬性后可以利用傳統(tǒng)的調(diào)度方法（單調(diào)速率RM、最早截止時間優(yōu)先EDF等）進(jìn)行調(diào)度實(shí)現(xiàn).圖17給出了采用RM單調(diào)速率調(diào)度方法的調(diào)度過程.

為了評估組合驗(yàn)證方法的性能，本文針對智能主從小車系統(tǒng)給出2個版本的實(shí)現(xiàn)，在第1個版本（CAR-1）中實(shí)現(xiàn)了手柄數(shù)據(jù)收發(fā)、從車讀取主車信息并跟隨等功能，在第2個版本（CAR-2）中實(shí)現(xiàn)了主從小車距離檢測、從車的姿態(tài)回傳等功能.基于對需求的分析，給出規(guī)約模型并逐步精化，得出具體模型.本文分別對3種驗(yàn)證方法進(jìn)行性能評估及對比，具體是：1）組合驗(yàn)證方法.通過本文所給的方法對時序模型逐步求精并驗(yàn)證.2）分組驗(yàn)證方法.基于本文所給組合驗(yàn)證方法，利用啟發(fā)式方法進(jìn)行組件分組的驗(yàn)證.3）時間I/O自動機(jī)的驗(yàn)證方法.得到系統(tǒng)的任務(wù)模型后，通過時間I/O自動機(jī)建立模型并基于UPPAAL工具[35]對模型進(jìn)行驗(yàn)證，具體的統(tǒng)計(jì)數(shù)據(jù)見表10和表11.

Table 10 Experimental Statistical Results of CAR-1表10 CAR-1的實(shí)驗(yàn)統(tǒng)計(jì)結(jié)果

Table 11 Experimental Statistical Results of CAR-2表11 CAR-2的實(shí)驗(yàn)統(tǒng)計(jì)結(jié)果

CAR-1中存在3個時序約束規(guī)約，結(jié)合前面推導(dǎo)出的任務(wù)結(jié)構(gòu)給出了32個邏輯時鐘定義，包括初始執(zhí)行相位、截止時間等，本文借鑒華文獻(xiàn)[36]給出的任務(wù)結(jié)構(gòu)來建立具體模型.同時利用本文所給的組合驗(yàn)證方法與圖15所示的系統(tǒng)需求模型（specification model）所精化后的模型進(jìn)行可組合驗(yàn)證.需要驗(yàn)證由表10所生成的任務(wù)模型是否滿足系統(tǒng)時間屬性的要求，如圖18所示.相關(guān)的驗(yàn)證結(jié)果統(tǒng)計(jì)如表10所示，在CAR-1場景下采用的組合驗(yàn)證方法用時12.27 s，采用的分組驗(yàn)證方法用時9.98 s.通過自動機(jī)模型進(jìn)行驗(yàn)證（UPPAAL工具）用時較長，約為38 s.

Fig.18 Verification rules for automotive system圖18 智能小車系統(tǒng)的驗(yàn)證規(guī)則

如表11中的統(tǒng)計(jì)數(shù)據(jù)，本文所給方法在模型檢查所用時間以及消耗內(nèi)存方面，尤其在分組驗(yàn)證的模式下，驗(yàn)證用時降低約63.24%，內(nèi)存的使用約減少44.01%.同時，模型過于復(fù)雜導(dǎo)致內(nèi)存消耗較大，使得表11中的規(guī)格5和規(guī)格8在組合驗(yàn)證方法中沒有完成.而在這2種規(guī)格分組驗(yàn)證的方式下，驗(yàn)證過程用時約為38 s，內(nèi)存消耗峰值約為73 MB.

為了對方法進(jìn)行綜合考量，本文也利用基于狀態(tài)語義的建模方法對智能車系統(tǒng)進(jìn)行行為建模，并采用UPPAAL驗(yàn)證工具對模型進(jìn)行檢查.其中，針對CAR-1系統(tǒng)的所有屬性，檢查都能夠完成并得到相關(guān)結(jié)果.而在CAR-2系統(tǒng)的行為驗(yàn)證中，由于系統(tǒng)的復(fù)雜性導(dǎo)致在驗(yàn)證過程中出現(xiàn)狀態(tài)數(shù)量急劇增長的情況，幾個屬性驗(yàn)證沒有得到結(jié)果.相關(guān)驗(yàn)證時間和內(nèi)存使用的數(shù)據(jù)統(tǒng)計(jì)如表10和表11所示.

6 結(jié) 論

對安全關(guān)鍵的信息物理系統(tǒng)進(jìn)行建模、分析和驗(yàn)證是該類系統(tǒng)開發(fā)過程的關(guān)鍵步驟.本文給出了一種基于時序行為的系統(tǒng)建模及驗(yàn)證方法，首先通過CCSL時序約束語言構(gòu)建上層的時序行為需求模型，并對時序行為進(jìn)行精化，最終通過組合驗(yàn)證的方法對系統(tǒng)的實(shí)現(xiàn)模型進(jìn)行驗(yàn)證.本文通過仿真實(shí)驗(yàn)與小車示例對方法進(jìn)行了評估，相關(guān)統(tǒng)計(jì)數(shù)據(jù)表明本文所給方法在一定程度上提高了精化和驗(yàn)證過程的性能.

在未來的工作中，將基于CCSL語言進(jìn)一步開展系統(tǒng)時序行為分析及驗(yàn)證等相關(guān)工作，包括將任務(wù)模型轉(zhuǎn)化為具體底層代碼、擴(kuò)展建模工具來對CCSL進(jìn)行支持等相關(guān)研究與探索.

作者貢獻(xiàn)聲明：陳博提出實(shí)現(xiàn)方案、分析實(shí)驗(yàn)數(shù)據(jù)，以及撰寫論文；李曦提出了研究思路，并審閱文章內(nèi)容；周學(xué)海提出論文寫作思路并修改論文.