Acceleration of Bounded Model Checking based on Satisfiability-Modulo-Theories for Embedded Software Designs
Leyuan Liu · Kyushu University Institutional Repository (QIR) (Kyushu University) · 2014
Software has become a critical part of our lives nowadays.Many software affects public security and our health care, such as those used in nuclear reactors, modern avionics system controllers, and artificial cardiac pacemaker etc. Consequentially, human life has become more and more dependent on the services provided by these systems.Embedded software is a very important proportion of such applications.Software failures in embedded systems are usually life-threatening and expensive in most cases.However, the complexity of embedded software increases substantially, which makes it challenging to develop techniques for ensuring highly reliable embedded software while considering the complexity, especially in the development of concurrent embedded software.Proposing formal verification techniques to improve the reliability of embedded software is the topic of this thesis.In particular, the emphasis is put on verifying the correctness of designs rather than source code of embedded software.Verifying designs have the advantage that it helps to reveal bugs in the early phase of a software development process, and thus, avoid the expensive costs that are generally required for revising a bug found in source code.Among the existing various formal verification techniques, satisfiability-modulo-theory (SMT) based bounded model checking (BMC) is adopted in this thesis.SMT-based BMC has the potential to avoid the notorious state-space explosion problem often suffered by other automated verification techniques such as explicit model checking and BDD-based symbolic model checking.Regarding embedded software designs, the thesis considers those developed