Formally modelling and verifying the FreeRTOS real-time operating system

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.