C Bounded Model Checker to Detect Unspecified Expression in FreeRTOS

Abstract

The Embedded systems are widely used in most electrical devices. They are often complex and safety –critical. Therefore their reliability is significantly important. Among many techniques to verify a system, model checking models a system into temporal logic and can be used to assert a desired property on it. CBMC is a bounded model checker for ANSIC and C++ programs. In this paper , it is extended the CBMC tool to check and automatically detect a C/C++ code containing a form of un specified behaviors, like function calla with arguments that exhibits side effects which might be easily un noticed by the programmers. In addition, the code can be configured properly to be used for Arm Cortex micro softwares..