Automatic Detection of Unspecified Expression Evaluation in FreeRTOS Programs

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 o...

Full description

Bibliographic Details
Main Author: Khodayari, Shahrzad
Format: Others
Language:English
Published: Uppsala universitet, Institutionen för informationsteknologi 2014
Online Access:http://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-228289
id ndltd-UPSALLA1-oai-DiVA.org-uu-228289
record_format oai_dc
spelling ndltd-UPSALLA1-oai-DiVA.org-uu-2282892014-07-10T17:02:13ZAutomatic Detection of Unspecified Expression Evaluation in FreeRTOS ProgramsengKhodayari, ShahrzadUppsala universitet, Institutionen för informationsteknologi2014Embedded 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 Student thesisinfo:eu-repo/semantics/bachelorThesistexthttp://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-228289IT ; 14 022application/pdfinfo:eu-repo/semantics/openAccess
collection NDLTD
language English
format Others
sources NDLTD
description 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
author Khodayari, Shahrzad
spellingShingle Khodayari, Shahrzad
Automatic Detection of Unspecified Expression Evaluation in FreeRTOS Programs
author_facet Khodayari, Shahrzad
author_sort Khodayari, Shahrzad
title Automatic Detection of Unspecified Expression Evaluation in FreeRTOS Programs
title_short Automatic Detection of Unspecified Expression Evaluation in FreeRTOS Programs
title_full Automatic Detection of Unspecified Expression Evaluation in FreeRTOS Programs
title_fullStr Automatic Detection of Unspecified Expression Evaluation in FreeRTOS Programs
title_full_unstemmed Automatic Detection of Unspecified Expression Evaluation in FreeRTOS Programs
title_sort automatic detection of unspecified expression evaluation in freertos programs
publisher Uppsala universitet, Institutionen för informationsteknologi
publishDate 2014
url http://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-228289
work_keys_str_mv AT khodayarishahrzad automaticdetectionofunspecifiedexpressionevaluationinfreertosprograms
_version_ 1716707219986186240