Journal | Formal Aspects of Computing |
---|
Date | Accepted/In press - 24 Jun 2014 |
---|
Date | E-pub ahead of print (current) - 20 Aug 2014 |
---|
Issue number | 1 |
---|
Volume | 27 |
---|
Number of pages | 25 |
---|
Pages (from-to) | 167-192 |
---|
Early online date | 20/08/14 |
---|
Original language | English |
---|
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.