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...
Main Author: | |
---|---|
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 |