安全攸關軟體驗證方法與工具之研究

A Study of Methods and Tools for Verifying Safety-Critical Software

林靖婕(Jing-Jie Lin)

指導教授 ： 蔡益坤

國立臺灣大學/管理學院/資訊管理學研究所/碩士(2013年)

https://doi.org/10.6342/NTU.2013.02375

摘要

安全攸關軟體的錯誤將導致人類傷亡，因此其正確性極為重要。安全攸關軟體典型為即時的多執行緒程式。多執行緒以執行多個並行活動，即時程式設計以確保滿足嚴格的時間限制。即時的多執行續程式設計易於犯錯，部分錯誤詭祕而難以用測試或模擬來發現。因此此類安全攸關軟體需要使用正規驗證方法加以檢查。
現今有許多方法及工具來支援即時多執行緒程式在功能及時間正確性上的正規驗證，每種方法或工具提供程式所涵蓋問題的部分解決方案。然而這些方法及工具由不同機構進行開發，因此選擇適合的工具或方法組合變得不易。為了實際驗證一程式，需要花費許多時間努力熟悉在不同領域的工具，並選擇適當的工具組合來完成驗證。在此論文中，我們對此類方法及工具做一精選，並介紹如何實行驗證。為使說明更易理解，我們以一具代表性的控制器程式為範例，此程式用以控制化學反應爐之溫度。論文中詳細說明功能正確性及時間正確性的驗證細節，並指出用以驗證的模型和實際程式間是否存在差異，以及是否存在現今工具無法支援的任務。我們以此論文建立一基準案例，透過此案例可迅速而容易地對現今即時多執行緒程式的正規驗證科技有一定的了解與評估。

關鍵字

正規方法 ； 模型檢查 ； 多執行緒程式 ； 即時系統 ； 靜態分析 ； 時間量測分析 ； 最差情況執行時間

並列摘要

Safety-critical software is software whose failure harm people or even cause deaths, so the correctness of such software is very important. Safety-critical software is typically a real-time and multithreaded program. Multithreading is required because of multiple concurrent activities. Real-time programming is required to guarantee strict timing constraints. Real-time multithreaded programs are prone to mistakes, and some bugs in such programs are subtle and difficult to find using testing or simulation. Thus it is desirable to apply formal verification on such safety-critical programs.
Nowadays, there are many methods and tools that support formal verification of the functional and timing correctness of real-time multithreaded programs. Each method or tool provides parts of solutions to the issue involved. Unfortunately, the methods and tools have traditionally been developed separately by different communities, and it is nontrivial to assemble a suitable collection of them. To practically verify a program, one needs to spend much effort and time on getting familiar with the tools located in different domains, and to select an adequate tool collection to complete the verification tasks. In this thesis, we review a selection of methods and tools and show how they may be used to carry out the verification tasks. To provide a more comprehensive illustration, we consider a representative controller program as our target program, which is a temperature controller for chemical reactor protection. We delineate the details for verification of the functional correctness and timing correctness of the program. We also point out whether there exist differences between the model for verification and the real program, and whether there exist tasks that are not supported by current tools. In doing so, we establish a benchmark case and with it obtain a partial yet informative assessment of the readiness of current technology for formal verification of real-time multithreaded programs.

並列關鍵字

Formal Methods ； Model Checking ； Multithreading ； Real-Time Systems ； Static Analysis ； Timing Analysis ； WCET

參考文獻

[47] L. d. Moura and N. Bjorner. Z3: An effcient SMT solver. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 4963 of LNCS, pages 337{340, 2008.

[37] Md. I. Hossain and N. S. Chowdhury. A practical approach on model checking with modex and spin. In International Journal of Electrical and Computer Sciences, volume 11, pages 1{7, 2011.

[21] E. M. Clarke, O. Grumberg, and D. A. Peled. Model checking. The MIT Press, 1999.

[3] DO-178B/ED-12B. Software Considerations in Airborne Sstems and Equipment Certification

[4] Frama-C software analyzers. http://frama-c.com/.