基于精確需求定義方法的列車自動保護（ATP）軟件開發(fā)＊

常 鳴

（卡斯柯信號有限公司，200071，上海／／工程師）

軟件開發(fā)過程中，需求是用戶與產品提供商，或系統(tǒng)分析師與開發(fā)團隊間的契約，其質量影響著最終產品的開發(fā)進度及其質量。一份精確、完整、一致、可追溯的需求規(guī)格書，可避免開發(fā)人員的理解偏差，極大幫助后續(xù)的設計編碼以及測試工作；并且，通過細致的需求分析，可以在開發(fā)的早期階段發(fā)現潛在問題，及時修復，降低處理問題的代價。

在ATP（列車自動保護）等安全苛求軟件的開發(fā)中，尤其應強調需求的質量。此類產品開發(fā)周期和使用壽命較長，需求變化相對不大，但對于安全和可靠性要求非常高，必須要做到軟件的每一步都是可控、可預測和可驗證的。

一些傳統(tǒng)的需求分析方法，如基于UML（統(tǒng)一建模語言）的用例分析等，在商業(yè)軟件開發(fā)中應用廣泛，其特征是比較直觀和易于理解；但圖形化方法往往缺乏嚴格的語義定義，且用例描述以自然語言形式，難于精確規(guī)范期望軟件的行為，容易使開發(fā)人員產生歧義。因此，傳統(tǒng)方法更適合于非安全軟件或者系統(tǒng)級需求的定義，不適于安全苛求軟件的需求定義。

應用基于數學符號推理的Z或VDM（維也納開發(fā)方法）等形式化需求建模，以及在此基礎上的形式化證明和代碼自動生成，是目前最嚴謹的軟件開發(fā)方式。法國阿爾斯通的URBALIS城市軌道交通信號產品中的車載ATP軟件，采用B方法開發(fā)，已在巴黎、米蘭、北京、上海等超過50個項目中得到應用。然而，形式化方法的困難在于其數學語言晦澀難懂，且開發(fā)流程和工具與當前開發(fā)者熟悉的方式不同，需要較長時間的學習才能應用。

在iCC200型車載ATP開發(fā)中，使用了一種“基于精確需求定義”的方法，在軟件需求層面，采用易于開發(fā)人員理解的“偽代碼”形式，精確定義每條功能需求，以此消除自然語言描述的模糊性。該方法有以下特點：

（1）針對每個功能點，定義特定的“需求變量”，作為一條需求。該變量可以被其他需求所引用，但只能在本條需求中被修改。

（2）使用類似“偽代碼”的語法規(guī)則，表示需求變量的產生條件。對于周期更新的變量，體現出時間先后關系。

（3）軟件需求自身是完備的。從邊界來看，所有的外部輸入和輸出之間可由一系列需求變量的相互引用關系所鏈接，組成功能鏈。

（4）每條“需求變量”都是可觀測的。其最終運行結果能在軟件維護工具上顯示，用于確認其正確性。

（5）每條需求都是可追溯的，通過唯一的標簽標記該需求。軟件需求來自系統(tǒng)級的分配，而每條需求也要被設計實現所覆蓋。

1 需求階段

根據EN 50128的開發(fā)模型，軟件需求應當來自系統(tǒng)需求或相應安全分析結果的分配。按照自上而下的設計方法，需求粒度逐漸變細，即系統(tǒng)設計階段的需求描述較粗，而軟件級需求非常精確。

例如系統(tǒng)需求［iTC＿CC－SyRS－0278］，表示車載控制器（CC）在限制人工模式（RM）時應當監(jiān)控車速是否超過項目可配置的限速值，若超過則應輸出緊急制動。系統(tǒng)需求描述如下：

［iTC＿CC－SyRS－0278］

當選擇的駕駛模式是RM時，如果列車超過Driving＿mode／Restrictive＿manual／Limit＿speed速度（項目配置的安全參數），CC將觸發(fā)緊急制動。

＃Category＝Functional

＃Contribution＝SIL4

＃Allocation＝ATP Software

＃ Source ＝ ［iTC－SyAD－0104］，［iTC－CCSSHA－0070］

［End］

在ATP軟件需求規(guī)格書中，會有多條軟件需求追溯上述［iTC＿CC－SyRS－0278］，通過＃Source進行標識。以軟件需求［iTC＿CC＿ATP－SwRS－0497］為例，定義需求變量RMoverSpeed作為RM下是否超速的判斷標識，需求如下：

［iTC＿CC＿ATP－SwRS－0497］

RMoverSpeed，布爾量，監(jiān)控列車速度是否超過RM模式的限速值。判斷條件如圖1所示。

1）當判斷結果為TRUE，表示車速超過RM模式限速；

2）當判斷結果為FALSE，表示車速未超過RM模式限速。

＃Category＝Functional

＃Contribution＝SIL4

＃Source＝［iTC＿CC－SyRS－0278］，［iTC＿CC＿ATP－SwHA－0121］

［End］

圖1 RM超速判斷條件

可以看到，基于精確需求定義方法的ATP軟件需求完全符合EN 50128在以下方面的要求。

（1）唯一性和一致性：對于需求變量，僅在定義它的需求中描述其設置和判斷條件；其他需求中僅可引用該變量，但不能修改，從而避免相同功能在多處描述引起不一致的問題。例如在RMoverSpeed的賦值中引用了RMselectedDrivingMode和TrainMaxSpeed等其他需求變量作為判斷條件，但不會修改它們，以此保持需求的唯一性和一致性。

（2）清晰性和精確性：需求中以偽代碼形式明確定義了RMoverSpeed的初值，運行中取真假值，以及保持不變（即等于上周期值）的條件。如此避免了自然語言描述的含混不清。此外，通過（k）或（k－1）標識，說明使用的是本周期還是上周期的結果，具有時間準確性。

（3）完備性：一般來說，由多個軟件需求形成功能鏈，共同完成某個系統(tǒng)功能。功能鏈從軟件的輸入開始，經過一系列處理，最后到軟件的輸出。圖2所示為RM超速判斷的功能鏈，通過一系列需求變量 如 RMselectedDrivingMode，TrainMaxSpeed，ValidTrainSpeed，TrainStopped等，處理了從軟件外部獲取的輸入信息，作為RMoverSpeed的判斷條件；而 RMoverSpeed本身，也被 Emergency－Break需求所引用，作為輸出緊急制動的條件之一。所有軟件需求形成的功能鏈，共同實現從外部輸入到輸出的完整的ATP功能。

（4）可追溯性：iCC200開發(fā)中，每條需求和設計均分配有唯一的標簽，使用Reqtify工具進行追蹤，由獨立的人員進行可追溯性驗證。精確定義的需求，也便于開發(fā)人嚴格按照需求實現。在發(fā)現缺陷后，需提交變更請求（CR）進行問題追蹤。如果需求和實現均有誤，則必須先修改需求文檔，再提交子CR修改相應的設計和代碼，避免需求與實現不一致的情況。

圖2 RM超速判斷功能鏈

（5）可驗證性：驗證（Verification）一般是通過分析（或測試）手段，檢查本階段的工作是否在完整性、正確性和一致性方面滿足之前階段的要求?；诰_需求定義的方法，驗證人員通過檢查如圖2所示的功能鏈，可清晰地判斷出ATP軟件是否實現了系統(tǒng)需求中期望的功能。

（6）可維護性：在軟件需求中所有定義的“需求變量”，均能夠在維護診斷工具中記錄并回放顯示。因此，維護人員可通過檢查功能鏈路上所有相關需求變量的狀態(tài)，來確認軟件功能是否被正確實現；如果發(fā)生了問題，也可以據此分析出產生錯誤的原因。

（7）可測試性：因為每條需求均由“偽代碼”定義，故可以方便地進行測試。具體在本文第3節(jié)說明。

2 設計編碼階段

應用基于精確需求定義的方法，雖然在需求階段已明確定義了軟件要完成的功能，但并未涉及所有的實現細節(jié)。以下方面，要在設計編碼階段細化：

（1）非功能性需求。需求規(guī)格書中以圖1形式描述的主要是功能性需求，對于非功能性需求要在設計中體現。

（2）算法優(yōu)化。每條需求均以自身定義的“需求變量”為中心，但對于不同的需求變量可能存在相似的判斷條件。在設計時可合并這部分內容，優(yōu)化算法。

（3）具體硬件的驅動或庫函數接口。需求規(guī)格書中不涉及此類內容。

（4）抽象數據類型或通用算法實現。需求定義中使用到的抽象數據類型（如鏈表）或算法（如遍歷）等，需設計時細化。

（5）數據結構的定義。

（6）模塊執(zhí)行的先后順序和調用關系等。需求規(guī)格書一般以場景或功能模塊為基礎進行劃分，而在設計時需要轉換為實際的進程或者函數模塊。

圖3是基于精確需求定義方法與傳統(tǒng)開發(fā)方法的工作流示意圖，縱軸和橫軸分別表示目標產品期望包括的信息內容和實現細節(jié)。圖3中實線表示的是基于精確需求定義方法的工作路徑，而虛線表示傳統(tǒng)方法的工作實現路徑?？煽吹剑诰_需求定義的方法要求在早期的需求分析階段，就盡可能多的識別出產品所需包括的信息內容，而在設計編碼階段主要是實現技術細節(jié)；傳統(tǒng)的開發(fā)方法，往往是隨著開發(fā)的深入，逐漸識別出更多的信息內容并加以實現。

圖3 基于精確需求定義方法與傳統(tǒng)軟件開發(fā)方法的工作比較

實際上，基于精確需求定義的方法在需求分析階段已完成了絕大部分的功能分拆和定義工作，因此開發(fā)中所需的設計和編碼時間會小于傳統(tǒng)方法。圖4所示為iCC100（BM）與iCC200兩代ATP產品的開發(fā)投入比較，二者的規(guī)模類似。iCC100（BM）使用傳統(tǒng)開發(fā)方法，而iCC200使用了基于精確需求定義的方法?？梢钥吹剑罕M管iCC200的需求階段投入是iCC100（BM）的一倍，但在設計和編碼階段卻節(jié)省了三分之一；更重要的是，精確定義的需求有效防止了由于理解偏差而導致的實現錯誤，顯著減少了在測試階段由于發(fā)現問題而返工所需的時間和人力。如圖4所示，同樣達到出口標準時，iCC200在測試階段的投入只有iCC100（BM）的一半。

圖4 iCC100（BM）與iCC200的開發(fā)投入比較

此外，對于安全苛求系統(tǒng)，所有內容均應進行安全分析，若識別為安全需求則必須應用安全技術對潛在的危險進行防護。如果按照傳統(tǒng)方法，到了開發(fā)的中后期階段，可能仍會發(fā)現新的安全相關項，這必將導致增加或修改既有的安全設計，不但影響開發(fā)進度，更有可能引入安全隱患。因此，在開發(fā)的前期階段，應盡可能完整地識別出所有開發(fā)內容，這對于安全苛求系統(tǒng)是非常重要的。另一方面，安全苛求系統(tǒng)的需求變化相對較少，但生命周期可長達數十年，這也使得在開發(fā)前期階段投入更多的時間和人力成為可能。

3 測試階段

軟件的單元測試和集成測試，可參照傳統(tǒng)方法進行。而基于精確需求定義的方法，對軟件產品的確認測試工作非常便利。根據EN 50128定義，確認（Validation）是指通過分析或測試手段，判斷最終產品是否滿足其需求的定義。從實際經驗來看，軟件確認測試是評判軟件是否達到開發(fā)目標的最重要手段。

依據安全軟件開發(fā)要求，軟件確認測試用例應當嚴格依據軟件需求撰寫，即需要在用例中明確設定被測需求的前置輸入條件和期望輸出結果。應用精確需求定義方法，需求變量的期望值及其對應條件已很明確，因此相應測試用例的輸入輸出結果也可以被精確定義，進一步使得基于腳本的自動化測試成為可能。例如，針對RMoverSpeed的確認測試，可根據圖1中的條件，模擬設定TrainMaxSpeed或ValidTrainSpeed等值的狀態(tài)，通過ATP軟件維護工具，觀察在不同條件組合下RMoverSpeed是否按照期望變化。

當根據CR發(fā)生需求或實現變更后，需進行軟件確認測試回歸。對于精確需求定義的ATP軟件，回歸測試涉及的用例范圍可依據以下原則進行確定。

（1）直接修改項。例如修改了RMoverSpeed需求（或實現）的判斷條件，那么該條需求對應的測試用例必需進行回歸。

（2）直接影響項。除“直接修改”外，如果RMoverSpeed所引用的RMselectedDrivingMode或TrainMaxSpeed需求（或實現）發(fā)生變更，那么RMoverSpeed對應的測試用例也必須進行回歸。

（3）間接影響項。除“直接修改”和“直接影響”外，如果修改了RMoverSpeed所引用的RMselectedDrivingMode或TrainMaxSpeed等需求（或實現），那么諸如EmergencyBreak等引用了RMoverSpeed的需求所對應的測試用例，也應挑選部分進行回歸。

4 結語

基于精確需求定義方法開發(fā)的iCC200型車載控制器，已經通過了TUV萊茵的第三方安全認證，并在上海張江實訓線上完成了中期試驗。

基于精確需求定義的開發(fā)方式，能夠解決需求描述中的精確性和完備性問題，并在系統(tǒng)的可追溯性驗證和確認測試中表現出比傳統(tǒng)方法更好的效果。雖然本方法要求在前期開發(fā)階段就進行大量細致的需求分析工作，但可有效減少后續(xù)設計和實現階段的技術和安全風險，這對安全苛求系統(tǒng)軟件的開發(fā)是非常重要。

此外，如果描述精確需求的“偽代碼”能遵循或可轉化為特定的模型語言，則可作為應用形式化方法建模和證明的基礎，并通過自動工具產生最終的軟件代碼，進一步縮短開發(fā)周期，更能提高軟件的安全性和可靠性。

［1］CENELEC EN 50128—2011.Railway applications－Communications，signalling and processing systems－Software for railway control and protection systems［S］.

［2］朱雪峰，金芝.關于軟件需求中的不一致性管理［J］.軟件學報，2005，16（7）：1221.

［3］燕飛.軌道交通列車運行控制系統(tǒng)的形式化建模和模型檢驗方法研究［D］.北京：北京交通大學，2006.

［4］斯多（Stahl T），沃爾特（Volter M）.模型驅動軟件開發(fā)：技術、工程與管理［M］.楊華，高猛，譯.北京：清華大學出版社，2009.