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.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Andrews Z, Bryans J, Fitzgerald J, Hughes J, Payne R, Pierce K, Riddle S (2011) Modelling and refinement of the Mondex electronic purse in VDM. Technical Report Series 1308, Newcastle University School of Computing Science
Arthan R (2012) ProofPower. http://www.lemma-one.com/ProofPower/
Barry R (2012) FreeRTOS Reference Manual—API functions and configuration options. PDF book available from http://shop.freertos.org
Barry R (2012) Using the FreeRTOS real time kernel—a practical guide. PDF book available from http://www.freertos.org
Egon B, Craig I (2009) Modeling an operating system kernel. In: Diekert V, Weicker K, Weicker N (eds) Informatik als Dialog zwischen Theorie und Anwendung. Vieweg+Teubner, pp 199–216
Jacobs FPB, Smans J (2010) A quick tour of the verifast program verifier. In: APLAS 2010. Lecture notes in computer science, vol 6461. Springer, Berlin
Butler M, Yadav D (2008) An incremental development of the Mondex system in Event-B. Formal Aspects Comput J 20(1): 61–77
Craig ID (2006) Formal models of operating system kernels. Springer, Berlin
Craig ID (2007) Formal refinement for operating system kernels. Springer, Berlin
Déharbe D, Galvão S, Moreira AM (2009) Formalizing FreeRTOS: first steps. In: Oliveira MVM, Woodcock J (eds) Formal methods: foundations and applications, 12th Brazilian symposium on formal methods, SBMF 2009, Gramado, Brazil, August 19–21, 2009, Revised selected papers. Lecture notes in computer science, vol 5902. Springer, Berlin, pp 101–117
Ferreira J, He G, Qin S (2012) Automated verification of the FreeRTOS scheduler in HIP/SLEEK. In: 6th international symposium on theoretical aspects of software engineering (TASE’12), 4–6 July
Freitas L, Woodcock J (2008) Mechanising Mondex with Z/EVES. Formal Aspects Comput J 20(1)
Freitas L, Woodcock J (2009) A chain datatype in Z. Int J Softw Inf 3(2–3): 357–374
George C, Haxthausen AE (2008) Specification, proof, and model checking of the Mondex electronic purse using RAISE. Formal Aspects Comput 20(1): 101–116
Hoare CAR, Misra J, Leavens GT, Shankar N (2009) The Verified Software Initiative: a manifesto. ACM Comput Surv 41(4)
Hoare CAR (2003) The verifying compiler: a grand challenge for computing research. J ACM 50(1): 63–69
Haneberg D, Schellhorn G, Grandy H, Reif W (2008) Verification of Mondex electronic purses with KIV: from transactions to a security protocol. Formal Aspects Comput J 20(1): 41–59
Jones C, O’Hearn P, Woodcock J (2006) Verified software: a grand challenge. IEEE Comput 39(4): 93–95
Jones CB, Pierce KG (2007) What can the π-calculus tell us about the Mondex purse system? In: 12th international conference on engineering of complex computer systems (ICECCS 2007), 10–14 July 2007, Auckland, New Zealand. IEEE Computer Society, pp 300–306
Jones C, Woodcock J (2008) Special issue on Mondex. Formal Aspects Comput 20(1)
Klein G, Elphinstone K, Heiser G, Andronick J, Cock D, Derrin P, Elkaduwe D, Engelhardt K, Kolanski R, Norrish M, Sewell T, Tuch H, Winwood S (2009) seL4: formal verification of an OS kernel. In SOSP, pp 207–220
Kuhlmann M, Gogolla M (2008) Modeling and validating Mondex scenarios described in UML and OCL with USE. Formal Aspects Comput J 20(1): 79–100
Klein G (2009) Operating system verification—an overview. Sadhana 34(1):27–69
Klein G (2010) A formally verified OS kernel. Now what? In Kaufmann M, Paulson LC (eds) Interactive theorem proving, first international conference, ITP 2010, Edinburgh, UK, July 11–14, 2010. Proceedings. Lecture notes in computer science, vol 6172. Springer, Berlin, pp 1–7
Klein G (2010) From a verified kernel towards verified systems. In: Ueda K (ed) Programming languages and systems—8th Asian Symposium, APLAS 2010, Shanghai, China, November 28–December 1, 2010. Proceedings. Lecture notes in computer science, vol 6461. Springer, Berlin, pp 21–33
Klein G (2010) The L4.verified project—next steps. In: Leavens GT, O’Hearn PW, Rajamani SK (eds) Verified software: theories, tools, experiments, third international conference, VSTTE 2010, Edinburgh, UK, August 16–19, 2010. Proceedings. Lecture notes in computer science, vol 6217. Springer, berlin, pp 86–96
Kong W, Ogata K, Futatsugi K (2007) Algebraic approaches to formal analysis of the Mondex electronic purse system. In: Davies J, Gibbons J (eds) Integrated formal methods, 6th international conference, IFM 2007, Oxford, UK, July 2–5, 2007, Proceedings. Lecture Notes in Computer Science, vol 4591. Springer, Berlin, pp 393–412
Labrosse JJ (2002) MicroC OS I: The real time kernel. Newnes
Lin Y (2010) Formal analysis of FreeRTOS. Master’s thesis, University of York
Muehlberg JT, Freitas L (2011) Verifying FreeRTOS: from requirements to binary code. In: Bendisposto J, Jones C, Leuschel M, Romanovsky A (eds) Proceedings of the 11th international workshop on automated verification of critical systems (AVoCS 2011). Electronic communications of the EASST, vol 10, pp 1–2
Mistry J (2011) FreeRTOS and multicore, September. MSc Dissertation, Department of Computer Science, University of York
Mühlberg JT, Lüttgen G (2010) Symbolic object code analysis. In: van de Pol J, Weber M (eds) Model checking software—17th international SPIN Workshop, Enschede, The Netherlands, September 27–29, 2010. Proceedings, Lecture Notes in Computer Science, vol 6349. Springer, berlin, pp 4–21
Mistry J, Naylor M, Woodcock J (2013) FreeRTOS and multicore
Meisels I, Saaltink M (1997) Z/Eves 1.5 Reference Manual. ORA Canada, TR-97-5493-03d
Owre S, Shankar N, Rushby J (2012) PVS. http://pvs.csl.sri.com/
Paulson L (2012) Isabelle. http://www.cl.cam.ac.uk/research/hvg/isabelle/
Pronk C (2010) Verifying FreeRTOS: a feasibility study. Technical Report TUD-SERG-2010-042, Delft University of Technology, Software Engineering Research Group
Ramananandro T (2008) Mondex, an electronic purse: Specification and refinement checks with the Alloy model-finding method. Formal Aspects Comput J 20(1):21–39
Saaltink M (1999) Z/Eves 2.0 Mathematical Toolkit. ORA Canada, TR-99-5493-05b
Saaltink M (1999) Z/Eves 2.0 User’s Guide. ORA Canada, TR-99-5493-06a
Spivey JM (1992) The Z notation: a reference manual. Series in Computer Science, 2nd edn. Prentice Hall International
Sewell T, Winwood S, Gammie P, Murray TC, Andronick J, Klein G (2011) seL4 enforces integrity. In: Marko C, van Eekelen JD, Geuvers H, Schmaltz J, Wiedijk F (eds) Interactive theorem proving—second international conference, ITP 2011, Berg en Dal, The Netherlands, August 22–25, 2011. Proceedings. Lecture notes in computer science, vol 6898. Springer, Berlin
Woodcock J, Davies J (1996) Using Z: specification, refinement, and proof. International series in computer science. Prentice-Hall, Englewood Cliffs
Woodcock J (2006) First steps in the Verified Software Grand Challenge. IEEE Comput 39(10): 57–64
Woodcock J, Stepney S, Cooper D, Clark J, Jacob J (2008) The certification of the Mondex electronic purse to ITSEC Level E6. Formal Aspects Comput 20(1)
Author information
Authors and Affiliations
Corresponding author
Additional information
Cliff Jones
Rights and permissions
About this article
Cite this article
Cheng, S., Woodcock, J. & D’Souza, D. Using formal reasoning on a model of tasks for FreeRTOS. Form Asp Comp 27, 167–192 (2015). https://doi.org/10.1007/s00165-014-0308-9
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-014-0308-9