摘要:車站聯鎖軟件一直有著嚴格的測試要求,仿真模塊是測試的重要組成部分,Petri網作為形式化語言的一種,有著準確與完備的特點,對于安全苛求軟件的測試尤為適合,該文提出了一種使用Petri網對聯鎖軟件測試中仿真模塊建模的方式,并分別給出了針對鐵路道岔的基于基本Petri網和有色Petri網2個建模實例。該模型有助于提高測試系統的安全性與精確性。
關鍵詞:聯鎖;軟件測試;建模;Petri網
中圖分類號:U284文獻標識碼:A 文章編號:1009-3044(2008)30-0606-03
Research on Simulation Modeling at Railway Interlocking Software Test Based on Petri Net
GONG Jie
(School of ElectronicsInformation Engineering, Tongji University, Shanghai 201804, China)
Abstract: The railway interlocking software always have a strict test demand ,simulation is an important part of test. As a kind of formal program language, Petri-Net is veracity and integrality. It is very suitable for the safety-critical software test. In the paper, it proposes an idea abort simulation modeling at railway interlocking software test. Furthermore, it presents two examples on Petri-Net and Color Petri-Net. It will help to improve the system’s security and veracity.
Key words: interlocking; software test; modeling; Petri-Net
環境仿真技術是軟件測試的重要組成部分,它不僅要能夠模仿出被仿系統的正常運行行為,還要能夠實現故障注入的模擬。鐵路聯鎖軟件是對鐵路站場信號設備進行實時控制,以保證站內行、調車安全和提高作業效率為目的的一種安全軟件[1]。隨著鐵路提速與計算機聯鎖應用的普及,對于鐵路計算機聯鎖軟件的測試越來越普遍。為了能有效地提供一個與車站聯鎖系統的實際環境相仿的供檢測的環境,我們就希望在計算機聯鎖測試評估平臺上利用計算機系統仿真技術模擬出車站內部的聯鎖情況,同時也能夠實現故障注入的模擬。
作為建模工具的一種,Petri網是1962年由Petri.C.A在他的博士論文中作為網狀結構的信息流模型提出來的[3]。近年來,Petri網以及它的各種改進模型如: 有色Petri網等被廣泛地應用到了眾多復雜系統的離散事件仿真模型搭建工作中,為離散事件的仿真提供了不少新的方法。相對于傳統的馬式鏈等建模方法,Petri網作為一種形式化方法,它不僅能分析系統軟,硬件中多方面的特性(如功能性,安全性,可靠性,實時性等)而且對于計算機聯鎖這類安全性極高的安全苛求軟件還可檢測系統定義的一致性,完整性和精確性。基于Petri網的這些優點,考慮到對聯鎖軟件測試所要模擬的鐵路站場的信號設備動作均是離散事件,因而我們嘗試著將Petri網引入對聯鎖軟件的測試仿真之中。本文針對鐵路聯鎖三大件之一的道岔提出了基于Petri網的仿真建模方案。
1 車站聯鎖仿真
仿真簡而言之就是在模型上進行試驗的過程。車站聯鎖仿真是要仿出一個鐵路車站信號系統中現場的各種設備(信號機,道岔,軌道電路區段等)在聯鎖邏輯下由聯鎖控制、列車運行或故障事件所導致的狀態變化的平臺提供給被測軟件作為其測試的命令對象[1]。因此,仿真環境必須能正確模仿這三種信號設備的動作,包括能夠正確模擬信號機的燈光顯示變換、道岔的位置轉換、列車和車列在站內運行引起相應軌道區段的占用或出清等。由于軌道電路區段的變化還涉及列車的運行,因此仿真環境還需模擬站內列車的各種行、調車作業。由于安全苛求軟件對安全性的嚴格要求,仿真環境還必須做到能夠根據測試的要求注入故障,成為一個嵌入故障的仿真環境。以考察被測軟件對于故障的應對能力。在這里Petri網的使用可以有效的模擬各種設備的動作和故障注入,描述各個設備的狀態變化。
2 Petri網
隨著對Petri網研究的深入,各種Petri網層出不窮,但是目前在仿真領域應用最為廣泛的仍是基本Petri網與有色Petri網。在文獻[3]與[4]中有著對基本Petri網與有色Petri網明確的定義:
2.1 基本Petri網
基本Petri網是一個四元組PN=(S,T;F,M0 )[3]
1) P為由庫所(places)組成的一類有限集合
2)T為由變遷(transitions)組成的一類有限集合
3) F為網的流關系(flow relation):且滿足:
4)M0為基本Petri網PN的初始標識。
2.2 有色Petri網的結構
有色Petri網的定義有多種,在這里我們選用了Kurt Jensen所給出的經典定義:有色Petri網是一個多元組CPN=(∑,P,T,A,N,C,G,E,I)它滿足如下條件[4]:
1) ∑是一有限非空類型集合,稱為顏色集
2)P為由庫所(places)組成的一類有限集合
3)T為由變遷(transitions)組成的一類有限集合
4)A是有限的弧集,且滿足
5)N稱為節點(node)函數,定義為 N:A→P×T∩T×P
6)C稱為顏色(color)函數,定義為 C:P→∑
7)G稱為防護(guard)函數,定義為,G:T→expressions(expressions為表達式),且滿足:
其中Type為類型函數,Var是變量函數,Var(expression)為由expression中所含變量組成的集合。
8)E為弧表達式函數,定義為 E:A→expressions,且滿足:
這里的p(a)表示n(a)的庫所。
9)I為初始化函數,它將每一庫所映射成一常量表達式,且滿足:
有色Petri網與基本Petri網的不同之處在于其擁有較高的折疊性,可以有效的減少庫所的數量,將基本Petri網較難描述的模型簡單的表示出來,改變基本Petri網對復雜系統無法描述的缺點。
3 仿真建模實例
在仿真建模中可根據不同的設備要求來選擇要使用的Petri網的類型,對于狀態與事件較少的設備可以就使用基本Petri網來描述,而對于某些較為復雜的設備則要利用有色Petri網才能建立起。下面將會給出對基本道岔模型(基本Petri網)和含故障設置的道岔模型(有色Petri網)的建模實例。
3.1 道岔的基本Petri網模型
道岔在聯鎖系統中是用來提供給列車軌道轉換的裝置,用來保障列車進入正常進路區,正常情況下,它根據進路的建立命令的保持不同的狀態,因此在建立仿真模型的過程中,應把道岔所受的聯鎖控制以及其的所處狀態作為需要考慮的重要因素,而其物理位置、形狀、外殼顏色等物理特性均可以忽略不記[2]。選擇道岔的顯示狀態作為庫所,道岔所受的聯鎖控制作為變遷,可以很好地描述道岔的狀態轉換。由于道岔的當前狀態只有4種,用基本Petri網即可方便、直觀描述。如圖1,清楚的表明了基本道岔的狀態轉換。
表1詳細解釋了道岔基本Petri網模型中的各個庫所和變遷的物理意義,即離散事件的各個狀態與引發狀態變化的事件。例如,在定位鎖閉這一變遷(T1)觸發后,信號機就會由初始狀態定位狀態(S1)顯示為鎖閉狀態(S3)。當道岔發生解鎖的變遷(T5)發生后,道岔將會重新回到定位(S1)。上圖中的四開是指一種道岔岔尖保持不接觸的狀態的鐵路術語,是一種正常狀態,而并非指道岔失去表示。
假定Petri網的原始狀態 M0={1,0,0,0},則其的可達性圖參見圖2。
通過上述可達性圖可以清楚的看出對于每個狀態M,其托肯顯示出的都是單一道岔狀態,沒有出現多狀態或無狀態顯示的錯誤,且根據Petri網的定義我們可以判定上一模型具有良好的可達性、可逆性與活性。
3.2 含故障設置的道岔的有色Petri網模型
在基本道岔的基礎上,往往在許多的測試中要求加入一定的故障,來觀察道岔對于故障的處理能力,在這里就需要做故障恢復的考慮(記憶性),因此用基本的Petri網來描述軌道區段就不再合適了,所以改為選擇有色Petri網來描述軌道區段的狀態。其托肯構造如下所示:
Token={ID,STATE0,STATE1}
其中:ID表示區段的物理地址,STATE0表示道岔的當前狀態,STATE1表示道岔的上一狀態(在故障設置中也可以模糊化為一記憶態,即追溯為上一對于判決有用的狀態)。在這種托肯結構下,每個托肯就可以同時包含當前狀態與以前狀態的信息,原來在這種條件下,使用基本Petri網來描述軌道區段的狀態變化會導致庫所的急劇增加,模型非常復雜,因此我們選用有色Petri網來建立仿真模型(圖3),同一庫所可以含有不同顏色的托肯,大大簡化了模型。
模型中,庫所集P={S1,S2,S3,S4,S5}代表軌道道岔的狀態空間,S1: 定位;S2: 反位;S3:四開;S4:鎖閉;S5:失表示。變遷集T={T1,T2,T3,T4,T5,T6,T7,T8,T9,T10,T11,T12 }包括了進路的控制命令與故障設置命令兩個部分的事件所轉化成的變遷。
對于P當中的各個庫所,定義色集如下:
C(S1)={(ID,S1,S3), (ID,S1,S4)}
C(S2)={(ID,S2,S3), (ID,S2,S4)}
C(S3)={(ID,S3,S1), (ID,S3,S2), (ID,S3,S5)}
C(S4)={(ID,S4,S1), (ID,S4,S2)}
C(S5)={(ID,S5,S3)}
從上面可以看到,我們將當前狀態STATE0相同的托肯都定義在同一庫所中。
表2詳細解釋了道岔模型中的庫所和變遷的物理意義,即離散事件的各個狀態(多個狀態依據某一規則集中成同一個庫所)與引發狀態變化的事件。弧集合A={a1 ,a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16 ,a17, a18, a19, a20, a21, a22, a23, a24},表3給出了弧函數E的具體定義:
防護函數G定義為:G(T6)=V1, G(T8)=V2, G(T1)=V3, G(T4)=V4, G(T9)=V5, G(T10)=V6, G(T11)=V7, G(T12)=V8,其中:
V1= (ID,S4,S1),V2= (ID,S4,S2),V3= (ID,S3,S2),V4= (ID,S3,S1)
V5= (ID,S3,S1),V6= (ID,S3,S2),V7= (ID,S5,S1),V8= (ID,S5,S2)
在這里防護函數所起的作用就是對有色Petri中的托肯加以篩選的模塊,例如防護函數V1,對于庫所S4的色集包含了2種不同的顏色{(ID,S4,S1),(ID,S4,S2)}但是根據站場的實際仿真情況,只有定位鎖閉的道岔才能在定位解鎖的命令(T6)下回到定位狀態,即只有在前一狀態為定位(S1)情況下,處于鎖閉狀態(S4)的道岔才會轉化為區段持久故障占用(S1)。所以通過設立防護函數V2,在庫所S4中只允許顏色為(ID,S4,S1)的托肯才能夠觸發T6后轉化為(ID,S1,S4)。起到了一種對托肯的有條件的篩選作用。
圖1與3的模型僅僅表達了鐵路道岔的聯鎖仿真建模的部分內容,隨著測試內容的增加會有更多的變遷產生,但是從上述兩建模的實例可以看出而言,Petri網是非常適用于車站聯鎖的描述的。
4 結論
環境仿真是軟件測試的一個重要課題。在安全軟件的測試中,是影響測試的有效性和效率的關鍵問題。本文結合鐵路車站微機軟件測試平臺的研究課題深入探討了環境仿真建模的課題,提出了利用Petri網建模的思想來完成聯鎖仿真的建模。鐵路車站信號聯鎖系統的聯鎖邏輯關系非常的復雜,其仿真的建模過去長期使用馬式鏈來完成,結構較為復雜,且會出現描述不清的狀況。使用Petri網建模后,利用形式化語言的準確性,提高了測試的一致性,完整性和精確性,而且有利于直接轉化為具體的編程語言。
雖然上述的設計思想和理論以取得一定的成果,然而仍有有待改進之處。比如時間Petri等在建模的引進等,還需要進一步考慮。總體看來,本文利用Petri對聯鎖軟件測試仿真建模的嘗試,對于離散事件的仿真建模起到了一定的借鑒作用。
參考文獻:
[1] 吳芳美.鐵路安全軟件測試評估.北京:中國鐵道出版社,2001.
[2] 屠海瀅,任曉旭,吳芳美.論鐵路信號仿真的模型、算法及策略[J].上海鐵道大學學報,1998,19:3-4.
[3] 吳哲輝.Petri網導論[M].北京:機械工業出版社,2006.
[4] Kurt Jensen. Colored Petri Nets—Basic Concepts Analysis Methods and PracticalUse[M]. Second Edition. Germany: Springer, 1997:70-107.
[5] 屠海瀅.面向軟件測試的仿真環境系統研究及其在鐵路信號安全軟件測試中的實現[D].上海鐵道大學學位論文,1999.
注:本文中所涉及到的圖表、注解、公式等內容請以PDF格式閱讀原文