Skip to Main Content
 

Global Search Box

 
 
 
 

Files

File List


mattmatias_thesis.pdf (1.25 MB)

ETD Abstract Container

Abstract Header

Program Verification of FreeRTOS using Microsoft Dafny

Matias, Matthew John
http://rave.ohiolink.edu/etdc/view?acc_num=csu1400085349

Abstract Details

2014, Master of Science in Software Engineering, Cleveland State University, Washkewicz College of Engineering.
FreeRTOS is a popular real-time and embedded operating system. Real-time software requires code reviews, software tests, and other various quality assurance activities to ensure minimal defects. This free and open-source operating system has claims of robustness and quality [26]. Real-time and embedded software is found commonly in systems directly impacting human life and require a low defect rate. In such critical software, traditional quality assurance may not suffice in minimizing software defects. When traditional software quality assurance is not enough for defect removal, software engineering formal methods may help minimize defects. A formal method such as program verification is useful for proving correctness in real-time soft- ware. Microsoft Research created Dafny for proving program correctness. It contains a programming language with specification constructs. A program verification tool such as Dafny allows for proving correctness of FreeRTOS’s modules. We propose using Dafny to verify the correctness of FreeRTOS’ scheduler and supporting API.
Nigamanth Sridhar, PhD (Committee Chair)
Yongjian Fu, PhD (Committee Member)
Chansu Yu, PhD (Committee Member)
Computer Science
software verification; program verification; software engineering; formal methods; program correctness; Microsoft Dafny; FreeRTOS; computer science

Recommended Citations

Citations

  • Matias, M. J. (2014). Program Verification of FreeRTOS using Microsoft Dafny [Master's thesis, Cleveland State University]. OhioLINK Electronic Theses and Dissertations Center. http://rave.ohiolink.edu/etdc/view?acc_num=csu1400085349

    APA Style (7th edition)

  • Matias, Matthew. Program Verification of FreeRTOS using Microsoft Dafny. 2014. Cleveland State University, Master's thesis. OhioLINK Electronic Theses and Dissertations Center, http://rave.ohiolink.edu/etdc/view?acc_num=csu1400085349.

    MLA Style (8th edition)

  • Matias, Matthew. "Program Verification of FreeRTOS using Microsoft Dafny." Master's thesis, Cleveland State University, 2014. http://rave.ohiolink.edu/etdc/view?acc_num=csu1400085349

    Chicago Manual of Style (17th edition)

csu1400085349
1,127
© 2014, some rights reserved.Creative Commons License Program Verification of FreeRTOS using Microsoft Dafny by Matthew John Matias is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 3.0 Unported License. Based on a work at etd.ohiolink.edu.
This open access ETD is published by Cleveland State University and OhioLINK.