Automatic Detection of Unspecified Expression Evaluation in FreeRTOS Programs

Abstract: Embedded systems are widely used in most electrical devices. They are often complex and safety-critical. Therefore, their reilability is significantlyimportant. 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 ANSI-C and C++ programs. In this thesis, we extend the CBMC tool to check and automatically detect a C/C++ code containing a form of unspecified behaviors, like function calls with arguments tht exhibit side effects which might be easily unnoticed by the programmers. Inn addition, the code can be configured properly to be used for ARM Cortex micro-controllers and FreeRTOS softwares