形式化方法（軟體可靠性方法）在實際工作中如何應用？

01-05

形式化方法的核心就是形式化語言，以及基於形式化語言構建出來的系統的形式化模型。

對於一些 safety critical 的系統（例如航空航天、高鐵動車、核電等）來說其系統的行為必須是可以預測的，即某些行為（死鎖、data race）等都是不允許的。而一般的軟體工程方法（測試）無法保證這些系統屬性的實現。因此需要將這些系統用語義明確的形式化語言進行建模，繼而採用模型監測、定理證明的方法對目標屬性進行驗證。

工業界位某些類型的系統（如高鐵上的動力控制系統等）的開發流程和實現制定了許多標準，如 IEC 61508（The IEC 61508 standard deals with the functional safety of electrical/electronic systems and programmable electronic (E/E/EP).），以及大量的衍生標準。只有通過這些標準，才能達到很多設備要求的安全等級（如 SIL 4），才能在市面上賣。

而這些標準在工程中的實現，需要形式化工具的支持。

例如，賣幾百萬一套的 SCADE Suite，其建模語言為 SSM（Graphical Esterel） + Lustre，都是很著名的形式化語言。通過對經過驗證的模型進行代碼生成，實現高質量的系統。

而 Mathworks 的系列工具 Simulink、 Polyspace 也是各種標準加持。

驗證方面，模型檢測工具、定理證明器（Coq、Isabelle、ACL2 等）、SMT Solver（Z3等）都是可以採用的方向，工程實踐中很多會結合多種方法。

總之，形式化方法既需要花（很多）錢購買工具，還要花錢（及很長時間）培訓人員使用，成本很高。但因其能夠降低安全攸關係統的風險，在一些行業中仍然是不可或缺的。

前段時間，一個來自日本的大牛人說，其實這個東西用到現實生活上還是很難的，需要大量大量的人力。。。

軟體測試，程序分析，以及。。。

編譯器

現在運用於工業界的形式化方法都是80年代的老方法了。真正新的有效地其實還不合適投入工業界。成本太高