Detection of runtime errors in MISRA C programs: A deductive approach

Abstract

In this paper, we describe a method for detecting runtime errors for programs which are written in an industrially sponsored safe subset of C called MISRA C. The method is based on a novel model of C programs: each C program is modeled as a typed transition system encoded in the specification language accepted by PVS theorem prover. Since the specification is strongly typed, proof obligations are generated, for possible type violations in each statement in C, when loaded in the PVS theorem prover which need to be discharged. The technique does not require execution of the program to be analysed and is capable of detecting runtime errors such as array bound errors, divide by zero, arithmetic overflows and underflows etc. Based upon the method, we have developed a tool, which converts MISRA C programs into PVS specifications automatically. The tool has been used in checking runtime errors in several programs developed for real-time control applications. © Springer-Verlag Berlin Heidelberg 2007.