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 journalArticle

Published copy (DOI)

Author(s)

Department/unit(s)

Publication details

JournalFormal Aspects of Computing
DateE-pub ahead of print - 20 Aug 2014
DatePublished (current) - 2015
Issue number1
Volume27
Pages (from-to)167-192
Early online date20/08/14
Original languageEnglish

Abstract

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