N. He and M.S. Hsiao (USA)
Formal methods, Verification and Validation
ION FOR FORMAL VERIFICATION OF EMBEDDED SOFTWARE Nannan He and Michael S. Hsiao <{nhe, hsiao}@vt.edu> Bradley Department of Electrical and Computer Engineering Virginia Tech, Blacksburg, VA, 24060, USA ABSTRACT Model checking is an important formal verification technique. Bounded Model Checking may also be applied to software programs, and it relies on a Boolean satisfiability problem (SAT) solver to explore the state space of the finite state program in C. It considers each variable as a bit-vector and transforms the unwound program traces into a propositional formula for satisfiability checking. However, this flattened Boolean formula loses the structural information in the program which can be utilized to direct the state exploration. In this paper, we propose a structural model of the program that explicitly represents data and control dependencies. We also reduce the safety property checking of embedded software to verifying the invariant property on the monitor output of the model. Then we symbolically simulate the model to implement complete input coverage for formal verification. To simplify the complexity of symbolic simulation, we apply the counterexample-guided abstraction-refinement procedure to automatically abstract property relevant constraints in order to construct a weakening abstraction of the structural model. The experimental results suggest that this approach can formally verify some properties with a small number of symbolic simulation runs.
Important Links:
Go Back
