The Formal Analysis For The Safety Of Safety-Critical Software

With the rapid development of information technology, the scale of the software has expanded and the system has become more and more complex. At the same time, more and more basic areas are highly dependent on the computer, such as aerospace, electronic commerce, telemedicine, etc. With the growing complexity of computer system and social dependence on information technology, people have spent more and more attention on the increasingly demands for reliability and safety of software. Software failure can lead to serious consequences, especially for safety-critical systems, even a very small software error can lead to the collapse of the whole system, and there will be catastrophic consequences. Therefore, how to ensure the safety of the software has become a key issue of modern software technology development.The safety of the software system should be guaranteed throughout the entire Software Life Cycle. The correctness of the high-level design cannot ensure the correctness of the code, so the code should be tested too. With the increase of the scale and the complexity of the software, traditional detection methods cannot meet the demands anymore. Modal Checking as an automatic formal method can find errors efficiently.After analysis of the storage module and management module of a safety-critical software, the paper deals with model checking of the safety-critical software via LLBMC in order to point out the faults in the design and implementation of the software. LLBMC has a high-precision memory model. In this paper, the source code C has been transformed to LLVM IR, and the problems to verify will be solved by SMT solvers. Some safety specifications about the safety-critical software have been proposed which will be tested as assertions of the model checking. The main question of the model checking for software is state explosion. Experiments have been done to analyze the effect of some parameters in the model checking, such as max-function-call-depth, max-loop-iteration, etc. For the state explosion, this paper proposes some methods to reduce the state space, such as diminish the depth of function calls, diminish the variable space, and cut branches with Breadth First Search. Experiments prove that, with the combination of these several state reduction methods, the system can be tested eventually.This paper is about formal verifications of memory errors and logic errors of the software module, including memory leak, illegal memory deal locations, reading overflows memory, writing overflows memory and other memory errors, and some logic errors of the software. Besides, the errors have been found can be tracked, which is useful to analyze and modify these errors. Following the approach outlines in this paper to detect and positioning errors existing in software implementation effectively, this offers reliable guarantee for enhancing the safety of software.