Program Verification of FreeRTOS using Microsoft Dafny

Bibliographic Details
Main Author:	Matias, Matthew John
Language:	English
Published:	Cleveland State University / OhioLINK 2014
Subjects:	Computer Science software verification program verification software engineering formal methods program correctness Microsoft Dafny FreeRTOS computer science
Online Access:	http://rave.ohiolink.edu/etdc/view?acc_num=csu1400085349

id	ndltd-OhioLink-oai-etd.ohiolink.edu-csu1400085349
record_format	oai_dc
spelling	ndltd-OhioLink-oai-etd.ohiolink.edu-csu14000853492021-08-03T06:25:03Z Program Verification of FreeRTOS using Microsoft Dafny Matias, Matthew John Computer Science software verification program verification software engineering formal methods program correctness Microsoft Dafny FreeRTOS computer science FreeRTOS is a popular real-time and embedded operating system. Real-timesoftware requires code reviews, software tests, and other various quality assuranceactivities to ensure minimal defects. This free and open-source operating system hasclaims of robustness and quality [26]. Real-time and embedded software is foundcommonly in systems directly impacting human life and require a low defect rate.In such critical software, traditional quality assurance may not suffice in minimizingsoftware defects. When traditional software quality assurance is not enough for defectremoval, software engineering formal methods may help minimize defects. A formalmethod such as program verification is useful for proving correctness in real-time soft-ware. Microsoft Research created Dafny for proving program correctness. It containsa programming language with specification constructs. A program verification toolsuch as Dafny allows for proving correctness of FreeRTOS’s modules. We proposeusing Dafny to verify the correctness of FreeRTOS’ scheduler and supporting API. 2014-05-28 English text Cleveland State University / OhioLINK http://rave.ohiolink.edu/etdc/view?acc_num=csu1400085349 http://rave.ohiolink.edu/etdc/view?acc_num=csu1400085349 unrestricted This thesis or dissertation is protected by copyright: some rights reserved. It is licensed for use under a Creative Commons license. Specific terms and permissions are available from this document's record in the OhioLINK ETD Center.
collection	NDLTD
language	English
sources	NDLTD
topic	Computer Science software verification program verification software engineering formal methods program correctness Microsoft Dafny FreeRTOS computer science
spellingShingle	Computer Science software verification program verification software engineering formal methods program correctness Microsoft Dafny FreeRTOS computer science Matias, Matthew John Program Verification of FreeRTOS using Microsoft Dafny
author	Matias, Matthew John
author_facet	Matias, Matthew John
author_sort	Matias, Matthew John
title	Program Verification of FreeRTOS using Microsoft Dafny
title_short	Program Verification of FreeRTOS using Microsoft Dafny
title_full	Program Verification of FreeRTOS using Microsoft Dafny
title_fullStr	Program Verification of FreeRTOS using Microsoft Dafny
title_full_unstemmed	Program Verification of FreeRTOS using Microsoft Dafny
title_sort	program verification of freertos using microsoft dafny
publisher	Cleveland State University / OhioLINK
publishDate	2014
url	http://rave.ohiolink.edu/etdc/view?acc_num=csu1400085349
work_keys_str_mv	AT matiasmatthewjohn programverificationoffreertosusingmicrosoftdafny
_version_	1719436308969947136

Program Verification of FreeRTOS using Microsoft Dafny

Similar Items