Verifying Rtuinos Using Vcc: From Approach To Practice

The correctness of implementation codes is important especially for safety-critical software which is usually written in C programming language. In this paper, we present a C code correctness verification framework (CVF for short) which is based on an automatic theorem proving tool---VCC, and propose a specification checking method to improve the correctness of verification specification codes. We use a real-time OS, RTuinOS1.0.2, to evaluate our CVF framework. And the result shows it is feasible and effective to apply CVF to a real system software. Besides, the experiments also show that the specification checking method is effective.