caa a22 4500 605516081 CHVBK 20210128100712.0 cr unu---uuuuu 210128e20150101xx s 000 0 eng 10.1007/s00165-014-0308-9 doi (NATIONALLICENCE)springer-10.1007/s00165-014-0308-9 Using formal reasoning on a model of tasks for FreeRTOS [Elektronische Daten] [Shu Cheng, Jim Woodcock, Deepak D'Souza] 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. British Computer Society, 2014 Verified software initiative nationallicence FreeRTOS nationallicence formal verification nationallicence Z/Eves nationallicence Cheng Shu Department of Computer Science, University of York, YO10 5GH, Deramore Lane, York, UK aut Woodcock Jim Department of Computer Science, University of York, YO10 5GH, Deramore Lane, York, UK aut D'Souza Deepak Dept of Computer Science and Automation, Indian Institute of Science, 560 012, Bangalore, India aut Formal Aspects of Computing Springer London 27/1(2015-01-01), 167-192 0934-5043 27:1<167 2015 27 165 https://doi.org/10.1007/s00165-014-0308-9 text/html Onlinezugriff via DOI BK010053 XK010053 XK010000 Metadata rights reserved Springer special CC-BY-NC licence nationallicence 1 research-article jats NATIONALLICENCE NATIONALLICENCE NL-springer NATIONALLICENCE 856 40 https://doi.org/10.1007/s00165-014-0308-9 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Cheng Shu Department of Computer Science, University of York, YO10 5GH, Deramore Lane, York, UK aut NATIONALLICENCE 700 1- Woodcock Jim Department of Computer Science, University of York, YO10 5GH, Deramore Lane, York, UK aut NATIONALLICENCE 700 1- D'Souza Deepak Dept of Computer Science and Automation, Indian Institute of Science, 560 012, Bangalore, India aut NATIONALLICENCE 773 0- Formal Aspects of Computing Springer London 27/1(2015-01-01), 167-192 0934-5043 27:1<167 2015 27 165