By the same authors

From the same journal

From the same journal

Using formal reasoning on a model of tasks for FreeRTOS

Research output: Contribution to journalArticlepeer-review

Published copy (DOI)



Publication details

JournalFormal Aspects of Computing
DateAccepted/In press - 24 Jun 2014
DateE-pub ahead of print (current) - 20 Aug 2014
Issue number1
Number of pages25
Pages (from-to)167-192
Early online date20/08/14
Original languageEnglish


FreeRTOS is an open-source real-time microkernel that has a wide community of users. We present the formal specification of the behaviour of the task part of FreeRTOS that deals with the creation, management, and scheduling of tasks using priority-based preemption. Our model is written in the Z notation, and we verify its consistency using the Z/Eves theorem prover. This includes a precise statement of the preconditions for all API commands. This task model forms the basis for three dimensions of further work: (a) the modelling of the rest of the behaviour of queues, time, mutex, and interrupts in FreeRTOS; (b) refinement of the models to code to produce a verified implementation; and (c) extension of the behaviour of FreeRTOS to multi-core architectures. We propose all three dimensions as benchmark challenge problems for Hoare’s Verified Software Initiative.

    Research areas

  • Verified software initiative, FreeRTOS, formal verification, Z/Eves.

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations