安全關鍵的信息物理系統中時序行為的組合與精化

陳 博 李 曦,2 周學海,2

1 （中國科學技術大學軟件學院 江蘇蘇州 215123）

2 （中國科學技術大學計算機科學與技術學院 合肥 230051）（chenbo2008@ustc.edu.cn）

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

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

為了對安全攸關的CPS進行設計開發，本文基于時序約束描述語言（clock constraint specification language,CCSL）對系統進行實現.具體地，本文主要貢獻體現在3個方面：

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

2）給出基于L*學習的系統屬性驗證方法.通過分治策略對系統屬性進行驗證，有效解決模型組合后所帶來的狀態激增的問題.

3）提出針對時序約束行為的逐步求精方法.主要針對3種典型的時序約束規約進行精化實現，給出任務結構的生成規則，能夠將頂層的時序規約模型映射為操作系統中任務級的時序行為約束模型.

1 相關工作

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

1.1 時間行為的組合與驗證

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

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

1.2 CCSL時間約束建模

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

1.3 時間行為的精化

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

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

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

2.1 CCSL建模

CCSL是用于描述系統中時序規約的半形式化語言，該語言定義了豐富的時間約束語義來對系統規約進行表達.比如優先語義（precedence）：m＞n，定義了時鐘m的滴答次數要多于時鐘n的滴答次數，或者交替語義（alternative）：m～n，表達了時鐘m和時鐘n會交替滴答產生的約束關系.

CCSL規約語言的核心要素是邏輯時鐘，區別于能夠度量物理時間的物理時鐘，邏輯時鐘可以看作是能夠在設計階段對系統中任務的時序關系進行表達的模型元素.本節首先描述一個邏輯時鐘的概念，再擴展出系統中存在多個邏輯時鐘的時間結構定義.

定義1.邏輯時鐘.采用5個標簽〈I,?, D, τ, u〉結構來進行表達.標簽I為一系列事件的發生時刻，?為發生時刻序列I上的嚴格優先（strict precedence），D是時鐘上的記號，通過函數τ進行定義：τ∶I→D，u是時鐘遞增幅度.針對邏輯時鐘而言，遞增幅度u可以是系統滴答tick，也可以是總線的傳輸周期等.

定義2.時間結構.通過標簽〈C, ?〉進行表達，在時間結構中，C為包括邏輯時鐘或度量時鐘的時鐘集合，?為這組時鐘上的先后約束關系.

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

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

cisPeriodicOnclkperiod=4 offset=1,

disPeriodicOnclkperiod=4 offset=3.

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

Fig.2 Diagram of clocks relationship圖2 時鐘的關系圖

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

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

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

1）S為一組狀態節點，s0是初始節點；

2）λ∶Tran→A定義節點轉換過程中對應的事件；

3）α，β∶Tran→S是映射函數，節點轉換中的起點和終點的節點；

4）Tran?S×2λ×S是描述轉移集合是節點之間轉換關系的子集，當事件e?λ，則當節點s到s’的所有觸發事件e都發生，并將產生該轉換.

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

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

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

3）α（t）=α（e）=s，β（t）=β（e）=s，是2個轉換過程對應的起點節點和終點節點；

4）λ（t）=m，λ（e）=ε，引起轉換的相應事件.

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

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

同樣，通過遷移系統對圖2中的時鐘行為進行建模，可以得到圖4所示結果.執行的跡（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 基于狀態遷移的時序約束關系圖

在能夠表達一個時鐘的執行過程后，需要對系統中存在的多個時鐘的約束行為關系進行組合來描述整體，最直觀的方法是計算多個時鐘的笛卡兒積.

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

1）S=S1×S2×…×Sn，系統的全部狀態；

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

3）α（〈t1,t2,…,tn〉）=〈α（t1）,α（t2）,…,α（tn）〉，轉移過程的起始狀態節點；

4）β（〈t1,t2,…,tn〉）=〈β（t1）,β（t2）, …,β（tn）〉，一次轉移過程的目的狀態節點；

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

定義5.禁止狀態.2個系統M與N的乘積為AP×AQ，其禁止狀態節點Forbidden（M, N）?SM×SN應具有屬性：

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

定義6.時序行為可組合.如果M和N有一個外部系統E，可以保證M和N在組合后禁止狀態節點不可達，可得M和N是時序行為可組合的.

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

Fig.5 System behavior model圖5 系統行為模型

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

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

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

Fig.6 A legal external environment圖6 一個合法的外部環境

3 組件的時序行為可組合驗證

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

3.1 組合驗證框架

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

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

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

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

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

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

在具體工作中，本文基于L*方法來對外部環境應具有的正確行為進行學習，不斷嘗試去找出能夠讓模型M滿足屬性P的所有行為，以此利用得到的所有正確行為序列構建出外部環境Ai.

3.2 基于L＊學習的時序行為可組合驗證

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

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

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

算法1.對時間進行學習的L*算法.

輸入：事件集合Σ；

輸出：通過學習得到滿足時間行為的遷移系統.

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

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

③ while true do

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

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

⑥ end while

⑦ 通過前面判定表中學習得到的行生成相應的遷移系統M；

⑧ ifψc（M）==1 then

⑨ returnM；

⑩ else

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

? end if

? end while

?σ←（σ,true）；s←（s,true）；e←（e,true） ； / * 通過對無時間語義的行為進行學習得到判定表（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，將其提交至教師進行候選人查詢（Mt） ；

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

? end while

? returnMt.

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

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

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

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

本節給出針對前述示例1行為的學習過程，初始階段判定表為空，逐步添加事件行為的前、后字符串序列來對判定表進行創建， 得到判定表T-1（表1）和判定表T-2（表2）.在計算M的判定表時，需要先確定M的事件集，具體地，前序字符串為S={ε}，后序字符串為E={ε}，事件集為Σ={c,d}，向“教師”提交整合后的字符串并查詢，判斷該字符串序列是否屬于所要學習的模型行為，如果屬于，就將判定表中對應的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中行④所給出規則來檢測判定表是否封閉，發現不存在s'滿足公式T（s·c·e）=T（ε·c·ε）.則判定表T-1不封閉，并將c添加至字符串集S中，更新T值，如表2所示.

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

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

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

Fig.8 Learning results without timing semantics圖8 無時間語義的學習結果

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

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

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

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

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

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

如下對2.1節中例1進行時間屬性學習的過程描述.首先對第1階段（無時間語義的行為推理過程）得到的判定表進行時間屬性的賦值，如表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轉換為假設條件，并再把交給函數ψc（M）進行檢查，如其值為false，則會提供一個破壞屬性的行為：σ={（c=1,clk＞1）（d=1,clk＞1）}；然而當判定表中S={（c,true）（d,true）}，則判斷時間屬性的有效值：|(clk＞1)(clk＞1)|∩|(true)(true)|≠?，并把前后字符串序列的時間約束進行分解，事件c和d的時間約束分別分解為（c,clk＜1）和（c,clk＞1），同時（d,clk＜1）和（d,clk≥1），再次利用判定表得出事件序列，并提交給函數（Mt），獲得T值，可得表5中的判定表T-5.

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

不斷對模型進行學習，能夠形成封閉的判定表T-5，通過判定表T-5可以得到圖9中的假設條件Ai（轉換為模型M）.

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

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

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

精化實現了對系統規約逐步具體化的操作過程[31].為了建立具體時序行為模型，本文通過CCSL時序約束語言建立上層時序模型，并對3種典型的時序規約實現精化.本文給出精化關系定義7.

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

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

精化過程實現了從較高層級模型到低層級模型的過渡與轉換.高層模型表達了系統需求層的時序關系，低層模型可以表達更為具體的系統任務級的時序關系[32].為了構建上層時序規約，本文以3種基本的時序約束需求作為基礎來建立規約模型并進行精化.3種約束關系分別為：

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

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

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

刻畫任務在執行過程中的前后順序依賴關系是精化過程的基礎，為了刻畫依賴約束，本文將通過任務圖來建立時序行為需求規約與任務模型之間的關系.

4.1 任務圖結構

利用任務圖G（U，V，N）結構可以刻畫任務之間的優先順序，其包括基本元素：

1）U表示圖中節點，V表示圖中的邊，N={τ1,τ2,…,τn}描述任務；

2）更為重要的是，每個任務具有相應的特征，Ti為任務的執行周期，任務的初始相位Pi應大于0，任務執行的時限Di應大于Pi，同樣，任務應具有最差執行時間ei的屬性，在各屬性中，[Pi, Di]時間段刻畫了任務可調度運行的區間Wi（Wi=Di-Pi）.

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

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

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

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

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

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

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

輸出：精化后的時序約束任務模型，周期Ti，任務實現Di，相位Pi.

① 給出系統任務圖結構G，描述系統中任務τ1,τ2,…,τn之間的依賴關系；

② 根據任務圖以及需求中的時序約束關系，通過任務之間的步調協同約束關系、延遲約束關系、間隔約束關系等，推導出任務參數Ti，Di，Pi的整體解空間S；

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

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

⑤ fork=0 →n-1 do

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

⑦ forj=k+1 →n-1 do

⑧ ifτj?τkthen

⑨Pj=Dk,Dj≤Pj； / *具有優先關系的任務，其相位值等于（或大于）前序任務的截止時間，進一步得到二者之間的關系 * /

⑩ end if

? end for

? end for

? 目標力爭最小化任務的相位值，最大化任務的截止時間，以此最大化任務利用率，得到Pi與Di的解空間，求得最優值；

? returnTi,Pi,Di.

針對時序行為進行逐步求精，本質是將上層的時序規約轉換為底層具體實現的過程，為了滿足行為的一致性，轉換過程應保證3方面的特性要求：

1）正確性.將精化后任務層的時序關系描述為TC，其次假定δ是系統的上層時序約束規約，在此定義下轉換出的 TC需要能夠滿足δ的要求.

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

3）可組合性.通過精化過程能夠推導出任務模型（周期、相位等），同時該任務模型能夠滿足系統時序規約的要求，可以得到多個子系統（組件）之間的時序行為是可以進行組合的.

4.2 約束關系的處理

任務之間的傳輸數據要盡量能夠保持數據傳輸步調的協同性.發送端和接收端的速率過于雜亂不利于數據的處理.如圖10中的示例，發送端和接收端具有一定的協同性，任務τ2可以容易地處理接收任務τ1的數據，因為任務τ1的發送周期P1=10 ms，而任務τ2的接收周期P2=30 ms，則任務τ2每隔3個時間間隔對數據進行接收（忽略掉2個），可參見圖10示例.

Fig.10 Task behavior with harmonious relationship圖10 具有協同關系的任務行為

定義8.任務周期的協同性.考慮2個或多個任務之間具有先后順序的依賴關系，在這種情景下，如果周期之間存在倍數關系，則稱任務之間是具有周期協同性的.假設任務為τ1和τ2，相應的周期值為T1和T2，2個周期值具有關系：T2=KT1（K∈ ?+），則2個任務的執行周期是具有協同關系的（T2|T1）.在圖11的任務圖結構可給出約束關系：

Fig.11 Timing relationship of task chain圖11 任務鏈的時序關系

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

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

定義9.延遲約束的處理.F（O|I）=tf定義了這樣的約束關系：為了保證任務在時間t內把寫入外部環境的事件O執行完成，參與這個輸出值計算的全部輸入數據事件I應該早于t - tf的時間到達.

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

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

其次，從整體任務或部分任務的輸入輸出行為上考量，可以得出的關系式為：

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

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

如圖12所示，在任務的執行過程中涉及多個與時間約束相關的時間屬性值，其中包括任務執行的初始時間點位置（相位Pi）和描述任務執行結束的時間點位置（時限Di）.

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

在此基礎上可以結合任務的時間行為屬性給出具體的約束關系式，即當第i個輸出事件盡量早發生，第i+1個輸出事件盡量晚發生時，該情景下產生輸出事件的最大的間隔輸出時間；當第i個輸出事件盡量晚發生時，第i+1個輸出事件盡量早發生時，該情景下將產生輸出事件最小的間隔輸出時間.相應約束關系為：

在描述任務的時間行為約束關系時，除去基本的任務執行周期、相位等時間元素，任務在執行中的計算時間上界e同樣是比較關鍵的建模內容.可以建立任務的執行時間ei、相位Pi以及截止時間Di之間的關聯.

同理，將上述關系擴展到多個任務的情景，能夠推導出如式（6）的約束表達（其中，E=e1+e2+…+en）.

4.3 約束關系的推導

針對某系統，能夠通過式（1）～（5）得出任務的時序約束關系表達式集合，在此基礎上對式（1）～（6）進行推導得出具體的變量值.相關流程為：

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

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

4.3.1 變量消除方法

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

為了通過消元來計算每個元素的值，需要進一步推導出元素之間的關系，具體給出的關系式為：

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

假設某個例子，相位和截止時間之間的關系為P4≥D4+18，P4≤31-D4，通過式子轉移將P4進行消除，得到的關系式為：

限定取值范圍為正整數，則D4相應的取值范圍為{1,2,…,7}.

在計算任務的周期Ti時，依據前面給出的優先順序約束，以及任務執行周期Ti的協同性等基本限定，同時，任務執行應保證資源利用率的限制，得：

基于此，建立系統的任務結構圖能夠確定時序規約和底層時序行為之間的推演關系，通過式（1）～（11）能夠確定基本的任務模型解空間.進一步對周期值進行限定，能夠細化取值范圍并最終確定最優的任務執行周期Ti.

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

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

5 實驗分析

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

5.1 精化方法性能分析

為了對精化方法的性能進行評估，本文對比了多種將需求規約轉化為實現模型的精化方法，主要從2個角度分析性能：1）精化的擴展性通過具體分析精化過程所用時間得到；2）生成任務集的效能通過相同約束場景下生成的任務數量進行評估.表6給出了相關的實驗設置.

Table 6 Scenario of Experiment表6 實驗場景

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

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

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

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

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

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

5.2 組合驗證方法的實驗及性能評估

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

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

從時序約束行為的角度出發，通過構件化的方法對系統進行設計和開發.首先建立任務之間的優先順序結構圖，同時給出具體的需求規約模型（部分如圖15所示）用于后續組件時間行為的可組合驗證.

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

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

Fig.16 Task structure diagram of automotive system圖16 智能小車系統的任務結構圖

得到系統的任務結構圖后，依據式（5）（6）可以得到表8中的任務-時間屬性關系式.

Table 8 Timing Behavior Relationship deduced from Task Link表8 任務鏈路推導的時間行為關系

將變量（周期、相位、截止時間等）和常量（任務的執行時間）代入任務-時間屬性的關系式，依據傅里葉-莫茨金消元法，由式（8）～（10）消除特定變量元素并推導出時間屬性的最優值，如表9所示.

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

如表9所示，對任務進行精化后可以得到具體的任務結構（包括任務執行周期、截止時間等）.得到任務的基本時間屬性后可以利用傳統的調度方法（單調速率RM、最早截止時間優先EDF等）進行調度實現.圖17給出了采用RM單調速率調度方法的調度過程.

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

Table 10 Experimental Statistical Results of CAR-1表10 CAR-1的實驗統計結果

Table 11 Experimental Statistical Results of CAR-2表11 CAR-2的實驗統計結果

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

Fig.18 Verification rules for automotive system圖18 智能小車系統的驗證規則

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

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

6 結 論

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

在未來的工作中，將基于CCSL語言進一步開展系統時序行為分析及驗證等相關工作，包括將任務模型轉化為具體底層代碼、擴展建模工具來對CCSL進行支持等相關研究與探索.

作者貢獻聲明：陳博提出實現方案、分析實驗數據，以及撰寫論文；李曦提出了研究思路，并審閱文章內容；周學海提出論文寫作思路并修改論文.