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

• Main Authors: Jing-Jie Lin, 林靖婕
• Other Authors: 蔡益坤
• Format: Others
• Language: zh-TW
• Published: 2013
• Online Access: http://ndltd.ncl.edu.tw/handle/92795290242215847446

碩士 === 國立臺灣大學 === 資訊管理學研究所 === 101 === 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.