Detection of Runtime Errors in MISRA C Programs: A Deductive Approach
| Autor: | Babita Sharma, S. Ramesh, Ajith K. John, A. K. Bhattacharjee, S. D. Dhodapkar |
|---|---|
| Rok vydání: | 2007 |
| Předmět: |
Statement (computer science)
Theoretical computer science MISRA C Division by zero Programming language Computer science Control (management) Specification language Type (model theory) computer.software_genre Automated theorem proving TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Transition system computer |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783540751007 SAFECOMP |
| DOI: | 10.1007/978-3-540-75101-4_46 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|