Using formal reasoning on a model of tasks for FreeRTOS
| LEADER | caa a22 4500 | ||
|---|---|---|---|
| 001 | 605516081 | ||
| 003 | CHVBK | ||
| 005 | 20210128100712.0 | ||
| 007 | cr unu---uuuuu | ||
| 008 | 210128e20150101xx s 000 0 eng | ||
| 024 | 7 | 0 | |a 10.1007/s00165-014-0308-9 |2 doi |
| 035 | |a (NATIONALLICENCE)springer-10.1007/s00165-014-0308-9 | ||
| 245 | 0 | 0 | |a Using formal reasoning on a model of tasks for FreeRTOS |h [Elektronische Daten] |c [Shu Cheng, Jim Woodcock, Deepak D'Souza] |
| 520 | 3 | |a 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. | |
| 540 | |a British Computer Society, 2014 | ||
| 690 | 7 | |a Verified software initiative |2 nationallicence | |
| 690 | 7 | |a FreeRTOS |2 nationallicence | |
| 690 | 7 | |a formal verification |2 nationallicence | |
| 690 | 7 | |a Z/Eves |2 nationallicence | |
| 700 | 1 | |a Cheng |D Shu |u Department of Computer Science, University of York, YO10 5GH, Deramore Lane, York, UK |4 aut | |
| 700 | 1 | |a Woodcock |D Jim |u Department of Computer Science, University of York, YO10 5GH, Deramore Lane, York, UK |4 aut | |
| 700 | 1 | |a D'Souza |D Deepak |u Dept of Computer Science and Automation, Indian Institute of Science, 560 012, Bangalore, India |4 aut | |
| 773 | 0 | |t Formal Aspects of Computing |d Springer London |g 27/1(2015-01-01), 167-192 |x 0934-5043 |q 27:1<167 |1 2015 |2 27 |o 165 | |
| 856 | 4 | 0 | |u https://doi.org/10.1007/s00165-014-0308-9 |q text/html |z Onlinezugriff via DOI |
| 898 | |a BK010053 |b XK010053 |c XK010000 | ||
| 900 | 7 | |a Metadata rights reserved |b Springer special CC-BY-NC licence |2 nationallicence | |
| 908 | |D 1 |a research-article |2 jats | ||
| 949 | |B NATIONALLICENCE |F NATIONALLICENCE |b NL-springer | ||
| 950 | |B NATIONALLICENCE |P 856 |E 40 |u https://doi.org/10.1007/s00165-014-0308-9 |q text/html |z Onlinezugriff via DOI | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Cheng |D Shu |u Department of Computer Science, University of York, YO10 5GH, Deramore Lane, York, UK |4 aut | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Woodcock |D Jim |u Department of Computer Science, University of York, YO10 5GH, Deramore Lane, York, UK |4 aut | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a D'Souza |D Deepak |u Dept of Computer Science and Automation, Indian Institute of Science, 560 012, Bangalore, India |4 aut | ||
| 950 | |B NATIONALLICENCE |P 773 |E 0- |t Formal Aspects of Computing |d Springer London |g 27/1(2015-01-01), 167-192 |x 0934-5043 |q 27:1<167 |1 2015 |2 27 |o 165 | ||