2016 17th IEEE/ACIS International Conference on Software Engineering, Artificial Intelligence, Networking and Parallel/Distributed Computing (SNPD)
Download PDF

Abstract

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 pro-pose 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.
Like what you’re reading?
Already a member?
Get this article FREE with a new membership!

Related Articles