White Rose University Consortium logo
University of Leeds logo University of Sheffield logo York University logo

Formally modelling and verifying the FreeRTOS real-time operating system

Cheng, Shu (2014) Formally modelling and verifying the FreeRTOS real-time operating system. PhD thesis, University of York.

[img]
Preview
Text (PDF file for the thesis)
Thesis.pdf
Available under License Creative Commons Attribution-Noncommercial-No Derivative Works 2.0 UK: England & Wales.

Download (1373Kb) | Preview
[img] Archive (The model and proof scripts(can be used by Z/Eves and ProZ) of the FreeRTOS model, Multi-core model and Task model with promotion, VCC annotated FreeRTOS source code and Test performed with FreeRTOS during the work.)
Archive.zip
Available under License Creative Commons Attribution-Noncommercial-No Derivative Works 2.0 UK: England & Wales.

Download (20Mb)

Abstract

Formal methods is an alternative way to develop software, which applies math- ematical techniques to software design and verification. It ensures logical consistency between the requirements and the behaviour of the software, because each step in the development process, i.e., abstracting the requirements, design, refinement and implementation, is verified by mathematical techniques. However, in ordinary software development, the correctness of the software is tested at the end of the development process, which means it is limited and incomplete. Thus formal methods provides higher quality software than ordinary software devel- opment. At the same time, real-time operating systems are playing increasingly more important roles in embedded applications. Formal verification of this kind of software is therefore of strong interest. FreeRTOS has a wide community of users: it is regarded by many as the de facto standard for micro-controllers in embedded applications. This project formally specifies the behaviour of FreeRTOS in Z, and its consistency is ver- ified using the Z/Eves theorem prover. This includes a precise statement of the preconditions for all API commands. Based on this model, (a) code-level annotations for verifying task related API are produced with Microsoft’s Verifying C Complier (VCC); and (b) an abstract model for extension of FreeRTOS to multi-core architectures is specified with the Z notation. This work forms the basis of future work that is refinement of the models to code to produce a verified implementation for both single and multi-core platforms.

Item Type: Thesis (PhD)
Related URLs:
Keywords: Verified Software Initiative, Formal Methods, Z, FreeRTOS, Verification, VCC, Multi-core, Z/Eves.
Academic Units: The University of York > Computer Science (York)
Identification Number/EthosID: uk.bl.ethos.684619
Depositing User: Mr Shu Cheng
Date Deposited: 06 May 2016 11:58
Last Modified: 08 Sep 2016 13:34
URI: http://etheses.whiterose.ac.uk/id/eprint/12671

You do not need to contact us to get a copy of this thesis. Please use the 'Download' link(s) above to get a copy.
You can contact us about this thesis. If you need to make a general enquiry, please see the Contact us page.

Actions (repository staff only: login required)