Date of Award

2014

Degree Type

Thesis

Department

Electrical and Computer Engineering

First Advisor

Sridhar, Nigamanth

Subject Headings

Computer software -- Verification, Real-time programming, Real-time data processing, Microcontrollers -- Programming, software verification program verification software engineering formal methods program correctness Microsoft Dafny FreeRTOS computer science

Abstract

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 suce 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 verication is useful for proving correctness in real-time software. Microsoft Research created Dafny for proving program correctness. It contains a programming language with specication constructs. A program verication 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

Download
COinS