在1977年RATP為了改善RER A地鐵線，采用當(dāng)時(shí)最新的安全計(jì)算機(jī)技術(shù)研發(fā)了名為SACEM的自動(dòng)列車保護(hù)系統(tǒng)(Automatic Train Protection) ，該系統(tǒng)采用嚴(yán)格的開發(fā)模型，運(yùn)行在單處理器上，使用MODULA-2語(yǔ)言編寫了6萬(wàn)多行代碼，被認(rèn)為是絕對(duì)安全的自動(dòng)列車保護(hù)系統(tǒng)。

然而，RATP在1989年采用了Jean-Raymond Abrial和Stephane Natkin提出的Z語(yǔ)言(基于Hoare邏輯的形式化語(yǔ)言)對(duì)SACEM系統(tǒng)進(jìn)行追溯建模，最終發(fā)現(xiàn)了20個(gè)不安全的場(chǎng)景。從那時(shí)候起，RATP決定在安全關(guān)鍵系統(tǒng)中使用形式化方法進(jìn)行開發(fā)，這也促成了業(yè)界第一條全自動(dòng)無(wú)人駕駛地鐵線路巴黎14號(hào)線的誕生。1998年巴黎14號(hào)線的成功運(yùn)營(yíng)具有里程碑的意義，奠定了在現(xiàn)代軌道交通信號(hào)系統(tǒng)中的CBTC系統(tǒng)(基于通信的列車自動(dòng)控制系統(tǒng)：Communication Based Train Control System)的研發(fā)中應(yīng)該使用形式化方法的趨勢(shì)。

巴黎14號(hào)線是由西門子公司(Siemens)采用B語(yǔ)言開發(fā)的，大約編寫了11.5萬(wàn)行代碼。B語(yǔ)言也是由Jean-Raymond Abrial提出的，同Z語(yǔ)言一樣支持根據(jù)規(guī)范編寫代碼。但不同于Z語(yǔ)言的是，B語(yǔ)言面向的層級(jí)稍低，不僅可以進(jìn)行形式化規(guī)范的精化，更專注于代碼的精化，因而B語(yǔ)言比Z語(yǔ)言更適合實(shí)現(xiàn)形式化的規(guī)約。這種使用形式方法進(jìn)行開發(fā)的安全性在補(bǔ)充測(cè)試階段(驗(yàn)證測(cè)試、集成測(cè)試等)得到了確認(rèn)，結(jié)果在這個(gè)系統(tǒng)上沒(méi)有發(fā)現(xiàn)任何bug。除了安全保證外，與經(jīng)典方法相比，形式化方法還具有成本效益，這是一個(gè)非常重要的優(yōu)勢(shì)。在成功應(yīng)用到巴黎14號(hào)線之后，B方法又在巴黎1號(hào)線信號(hào)系統(tǒng)改造和歐洲阿麗亞娜5號(hào)火箭上得到成功應(yīng)用。

不過(guò)，1998年后在RATP眾多供應(yīng)商中僅有西門子(Siemens)和阿爾斯通(Alstom)兩家繼續(xù)使用B方法進(jìn)行其他項(xiàng)目軌交信號(hào)系統(tǒng)的研發(fā)，而以安薩爾多Ansaldo，泰雷茲Thales，阿海琺Areva為代表的供應(yīng)商則選擇使用SCADE產(chǎn)品進(jìn)行軌交信號(hào)系統(tǒng)的開發(fā)，還有其他供應(yīng)商使用Petri網(wǎng)或者Ada語(yǔ)言行開發(fā)……之后西門子和阿爾斯通在不少項(xiàng)目上也開始使用SCADE進(jìn)行大規(guī)模的研發(fā)。值得一提的是，Z語(yǔ)言和Lustre語(yǔ)言都是創(chuàng)立于上世紀(jì)80年代初，之后又分別演進(jìn)出了B語(yǔ)言(Event B語(yǔ)言)和SCADE語(yǔ)言。在同樣都是形式化語(yǔ)言的基礎(chǔ)上，B語(yǔ)言的語(yǔ)法語(yǔ)義的掌握既需要專家的長(zhǎng)期支持，又需要經(jīng)常實(shí)踐才能達(dá)到一定的門檻；而SCADE語(yǔ)言是基于模型的開發(fā)驗(yàn)證工具及可橋接的第三方工具更多，這可能是其應(yīng)用更廣泛的原因。

圖表1: RATP的CBTC和聯(lián)鎖項(xiàng)目中的供應(yīng)商與采用的形式化開發(fā)技術(shù)

為了在評(píng)估軟件系統(tǒng)時(shí)能獨(dú)立于各供應(yīng)商選用開發(fā)的形式化模型，RATP根據(jù)內(nèi)部的安全政策，研制出了獨(dú)立的工具鏈，并在此基礎(chǔ)上提出了PERF（Proof Executed over a Retro-engineered Formal model）方法論。PERF是在系統(tǒng)開發(fā)之后執(zhí)行的一種形式化證明方法。與諸如B方法這類貫穿于系統(tǒng)的開發(fā)階段的形式化技術(shù)不同，PERF的驗(yàn)證技術(shù)僅在V流程開發(fā)周期的右側(cè)上升階段(即驗(yàn)證階段)應(yīng)用。即使在系統(tǒng)開發(fā)的早期階段沒(méi)有計(jì)劃要使用形式化方法來(lái)驗(yàn)證，這種技術(shù)依然允許在后期應(yīng)用形式化方法。除了確保開發(fā)階段的獨(dú)立性之外，從安全的角度來(lái)看，PERF還具有以下與形式化開發(fā)方法相關(guān)的強(qiáng)大特性：

• 屬性驗(yàn)證的窮盡性

• 通過(guò)形式化建模來(lái)確認(rèn)需求本身，這種建模揭示了需求中任何含糊不清或缺乏準(zhǔn)確性的地方

PERF對(duì)應(yīng)的完整工具鏈，是圍繞一個(gè)驗(yàn)證引擎進(jìn)行構(gòu)建，將模型檢查和歸納證明技術(shù)相結(jié)合。該工具鏈基于傳統(tǒng)Lustre語(yǔ)言(與SCADE同宗同源)，能以同步語(yǔ)言的方式描述要檢查系統(tǒng)的形式化模型。此外，PERF工具鏈還包括幾個(gè)“基本構(gòu)建塊”，它們能以不同的方式組織以解決特定問(wèn)題。這樣就可以用于不同類型的驗(yàn)證。因此，PERF工具鏈可以通過(guò)調(diào)整其用途來(lái)用于不同的項(xiàng)目，這意味著工程師可以利用單一工具的專業(yè)知識(shí)進(jìn)行工作。

PERF工作流如圖表1，其形式化引擎有三個(gè)輸入，三個(gè)輸出。

左側(cè)輸入的是源軟件(可以是SCADE，Ada或C代碼)被轉(zhuǎn)換成一個(gè)的形式化的HLL語(yǔ)言后，再傳給形式化分析引擎Proof engine。右側(cè)輸入的是將安全需求改為全部或部分安全屬性，也用HLL語(yǔ)言實(shí)現(xiàn)。左側(cè)的形式化模型和右側(cè)的形式化屬性構(gòu)成一個(gè)證明結(jié)構(gòu)。中間輸入的是某些情況下可能會(huì)包含描述環(huán)境模型的約束或假設(shè)，也需要用HLL語(yǔ)言實(shí)現(xiàn)。這個(gè)環(huán)境模型對(duì)于消除不可能的情況和更好地指導(dǎo)證明過(guò)程非常有用。

所有三個(gè)模型(軟件、安全屬性和環(huán)境)都輸入到形式化分析引擎中進(jìn)行運(yùn)算后，中間輸出的是檢查的安全屬性是否有效；右側(cè)輸出的是在正確驗(yàn)證屬性的情況下，可提交鑒定的日志，以供審查方追溯用于驗(yàn)證安全屬性的操作步驟；左側(cè)輸出的是在屬性無(wú)效的情況下，引擎可提供了這些屬性被篡改的反例。

圖表2: PERF工作流

上面提到的HLL語(yǔ)言，是一種基于數(shù)據(jù)流的、聲明性的同步語(yǔ)言，也具有形式化的語(yǔ)法和語(yǔ)義。它類似于Lustre或SCADE，但具有稍微豐富的類型系統(tǒng)(標(biāo)準(zhǔn)標(biāo)量和結(jié)構(gòu)化類型、函數(shù)、謂詞、層次枚舉等)，這些類型上有一組廣泛的運(yùn)算符(包括基本的前、后時(shí)態(tài)運(yùn)算符)，以及旨在表達(dá)通用安全規(guī)范的特定結(jié)構(gòu)(對(duì)有限集、約束、證明義務(wù)等的量化)。

第一次應(yīng)用PERF的成本相當(dāng)于基于驗(yàn)證測(cè)試活動(dòng)的傳統(tǒng)方法成本。這一初始成本主要根據(jù)供應(yīng)商使用的開發(fā)方法而對(duì)工具進(jìn)行的必要調(diào)整，并建立了適當(dāng)?shù)牧鞒獭６谖磥?lái)處理變更(非回歸測(cè)試和影響評(píng)估)時(shí)，形式化證明的成本將顯著下降，這使得PERF在項(xiàng)目的整個(gè)生命周期內(nèi)更具優(yōu)勢(shì)。

和使用其他形式化方法一樣，為應(yīng)對(duì)程序的狀態(tài)空間爆炸問(wèn)題，都可能需要對(duì)程序進(jìn)行切片，精化，抽象等處理。在使用PERF時(shí)，RATP也提出了推薦的精化refinement與抽象abstraction的方法。

某案例目標(biāo)系統(tǒng)的實(shí)現(xiàn)是分別基于SCADE模型和ADA手寫代碼。在開發(fā)階段，系統(tǒng)被分解成與SCADE操作符或ADA代碼塊（主要是過(guò)程）對(duì)應(yīng)的多個(gè)組件。然后在組件級(jí)別執(zhí)行抽象。直接影響所研究的安全屬性組件不作修改，因?yàn)樗鼈冋切枰治龅膶?duì)象。而其他組件可以抽象為表示所有可能的行為，這是通過(guò)忽略組件的所有實(shí)現(xiàn)細(xì)節(jié)并將抽象（未定義）值作為輸出來(lái)執(zhí)行的。由此產(chǎn)生的抽象模型比原始模型更為通用；它是包含原始行為集的超集。證明安全屬性在此超集上有效，意味著此安全屬性對(duì)于其任何子集(特別是原行為子集)仍然有效。

抽象通過(guò)去掉組件的所有不必要的細(xì)節(jié)，大大降低了模型的復(fù)雜度。值得注意的是，抽象組件輸出的狀態(tài)空間變得比原始組件輸出的狀態(tài)空間大，因?yàn)樗浅橄蠼M件輸出的超集，這在理論上會(huì)加劇狀態(tài)空間爆炸問(wèn)題。然而，在實(shí)踐中，與忽略所有中間變量引起的狀態(tài)空間縮減相比，輸出的這種增加是微不足道的。

抽象原則如下圖所示。以一個(gè)由3個(gè)組件組成的系統(tǒng)為例。不同的組件通過(guò)輸入/輸出通道進(jìn)行交互，以實(shí)現(xiàn)完整的系統(tǒng)行為。如果我們考慮只有組件2影響給定屬性的情況，則在右側(cè)給出用于驗(yàn)證該屬性的系統(tǒng)的最佳抽象。整個(gè)系統(tǒng)的復(fù)雜性降低到了現(xiàn)在所考慮組件的復(fù)雜性。

圖表3: 抽象前和抽象后的概覽

抽象過(guò)程可以迭代地應(yīng)用到系統(tǒng)的不同層次，從整個(gè)系統(tǒng)到組件的原子功能。在案例研究中，抽象能顯著地減少目標(biāo)系統(tǒng)的大小和復(fù)雜性。這種規(guī)模的縮減使得驗(yàn)證活動(dòng)成為可行的。除了驗(yàn)證之外，抽象過(guò)程還幫助我們更好地理解被驗(yàn)證的系統(tǒng)及其不同的組件。然而，這種抽象技術(shù)的有兩個(gè)主要缺點(diǎn)。一是需要時(shí)間來(lái)確定給定屬性的最小抽象模型。二是要獲得一個(gè)只包含必需組件的抽象模型，需要付出相當(dāng)大的努力。目標(biāo)是找到抽象層次與所獲得的抽象模型的復(fù)雜度之間的最佳折衷。這種復(fù)雜的自底向上的解決方案也可以與自上而下的屬性精化改進(jìn)方法相耦合，以減少驗(yàn)證復(fù)雜性。

圖表4: 抽象與精化的V模型圖

精化過(guò)程從頂層規(guī)范開始，可嘗試逐步進(jìn)行，以達(dá)到目標(biāo)抽象模型。抽象過(guò)程則相反，它從系統(tǒng)的具體實(shí)現(xiàn)開始，去除不必要的細(xì)節(jié)，以便得到只包含高級(jí)規(guī)范的抽象模型。

安全屬性的精化過(guò)程不應(yīng)該自動(dòng)化，它需要CBTC軟件和系統(tǒng)專家與安全評(píng)估工程師的合作，以達(dá)到合理的水平。驗(yàn)證活動(dòng)的自動(dòng)化是可行的，可確保手動(dòng)精化過(guò)程是正確的。抽象過(guò)程可以是部分自動(dòng)化的并僅由CBTC軟件專家來(lái)操作。抽象過(guò)程的結(jié)果也可以用于未來(lái)演進(jìn)版本的自動(dòng)化影響分析，未來(lái)演進(jìn)版本的回歸分析可以忽略，因?yàn)樗鼈儾粫?huì)影響已驗(yàn)證的行為。

RATP已經(jīng)在下列巴黎地鐵線路上應(yīng)用PERF進(jìn)行了形式化驗(yàn)證。

圖表5: 2011年后形式化方法在RATP的應(yīng)用統(tǒng)計(jì)

其中泰雷茲, 安薩爾多和阿爾斯通(前阿海琺的相關(guān)部門)開發(fā)了線路1,4,8,12的聯(lián)鎖系統(tǒng)和線路3,5,9,13的CBTC系統(tǒng)的軌旁和車載部分。圖表6是RATP應(yīng)用PERF方法論的統(tǒng)計(jì)，藍(lán)色進(jìn)度條顯示的是使用PERF方法進(jìn)行安全評(píng)估項(xiàng)目的百分比，PERF對(duì)右側(cè)使用SCADE模型開發(fā)部分的安全評(píng)估達(dá)到近100%，代碼量也遠(yuǎn)超前面三種開發(fā)手段，可見SCADE模型與PERF方法論的工具鏈?zhǔn)菢O其匹配的。

圖表6: PERF的應(yīng)用統(tǒng)計(jì)

使用SCADE工具開發(fā)的13號(hào)線CBTC軌旁項(xiàng)目，生成了6百萬(wàn)行代碼。在該項(xiàng)目的某子系統(tǒng)上根據(jù)3個(gè)通用安全規(guī)范精化出了110個(gè)安全屬性。在應(yīng)用PERF提出的精化和抽象方法后，對(duì)其中一個(gè)安全屬性進(jìn)行形式化分析。在未抽象前，其形式化證明耗費(fèi)了275G內(nèi)存，用時(shí)4小時(shí)30分鐘；而抽象后，其形式化證明僅耗費(fèi)了20G內(nèi)存，用時(shí)3分鐘20秒。

[2] Benaissa N, Bonvoisin D, Feliachi A, et al. The PERF approach for formal verification[C]//International Conference on Reliability, Safety, and Security of Railway Systems. Springer, Cham, 2016: 203-214.

[3] Fredj M, Leger S, Feliachi A, et al. OVADO[C]//International Conference on Reliability, Safety and Security of Railway Systems. Springer, Cham, 2017: 87-98.

[4] B method.[EB/OL].https://en.m.wikipedia.org/wiki/B-Method

[5] Coupoux P. Combination of Formal Methods for Creating a Critical Application[J]. Formal Methods Applied to Industrial Complex Systems, 2014: 353-389.

[6] Formal techniques in CBTC software development [EB/OL].Oct 22,2009

[7] Feliachi A, Bonvoisin D, Chaou S, et al. Formal verification of system-level safety properties on railway software[J]. Congrès Lambda Mu 20 de Ma?trise des Risques et de S?reté de Fonctionnement, 11-13 Octobre 2016, Saint Malo, France, 2016.