Refinement-based verification of the FreeRTOS scheduler in VCC

Sumesh Divakaran; Deepak D’Souza; Anirudh Kushwah; Prahladavaradan Sampath; Nigamanth Sridhar; Jim Woodcock

doi:10.1007/978-3-319-25423-4_11

Refinement-based verification of the FreeRTOS scheduler in VCC

Sumesh Divakaran
, Deepak D’Souza
, Anirudh Kushwah
, Prahladavaradan Sampath
, Nigamanth Sridhar
, Jim Woodcock

Research output: Chapter in Book/Report/Conference proceeding › Chapter › peer-review

6 Scopus citations

Abstract

We describe our experience with verifying the schedulerrelated functionality of FreeRTOS, a popular open-source embedded real-time operating system. We propose a methodology for carrying out refinement-based proofs of functional correctness of abstract data types in the popular code-level verifier VCC. We then apply this methodology to carry out a full machine-checked proof of the functional correctness of the FreeRTOS scheduler. We describe the bugs found during this exercise, the fixes made, and the effort involved.

Original language	English
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Place of Publication	deu
Publisher	Springer [email protected]
Pages	170-186
Number of pages	17
Volume	9407
DOIs	https://doi.org/10.1007/978-3-319-25423-4_11
State	Published - Jan 1 2015
Event	Formal Methods and Software Engineering - 17th International Conference on Formal Engineering Methods, {ICFEM} 2015, Paris, France, November 3-5, 2015, Proceedings - Duration: Jan 1 2015 → …

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Publisher	Springer [email protected]
Volume	9407
ISSN (Print)	03029743
ISSN (Electronic)	16113349

Conference

Conference	Formal Methods and Software Engineering - 17th International Conference on Formal Engineering Methods, {ICFEM} 2015, Paris, France, November 3-5, 2015, Proceedings
Period	01/1/15 → …

Access to Document

10.1007/978-3-319-25423-4_11

Cite this

Divakaran, S., D’Souza, D., Kushwah, A., Sampath, P., Sridhar, N., & Woodcock, J. (2015). Refinement-based verification of the FreeRTOS scheduler in VCC. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9407, pp. 170-186). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9407). Springer [email protected]. https://doi.org/10.1007/978-3-319-25423-4_11

Divakaran, Sumesh ; D’Souza, Deepak ; Kushwah, Anirudh et al. / Refinement-based verification of the FreeRTOS scheduler in VCC. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 9407 deu : Springer [email protected], 2015. pp. 170-186 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inbook{3867d9157631434495bac0f602f8baec,

title = "Refinement-based verification of the FreeRTOS scheduler in VCC",

abstract = "We describe our experience with verifying the schedulerrelated functionality of FreeRTOS, a popular open-source embedded real-time operating system. We propose a methodology for carrying out refinement-based proofs of functional correctness of abstract data types in the popular code-level verifier VCC. We then apply this methodology to carry out a full machine-checked proof of the functional correctness of the FreeRTOS scheduler. We describe the bugs found during this exercise, the fixes made, and the effort involved.",

author = "Sumesh Divakaran and Deepak D{\textquoteright}Souza and Anirudh Kushwah and Prahladavaradan Sampath and Nigamanth Sridhar and Jim Woodcock",

year = "2015",

month = jan,

day = "1",

doi = "10.1007/978-3-319-25423-4\_11",

language = "English",

volume = "9407",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer [email protected]",

pages = "170--186",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

note = "Formal Methods and Software Engineering - 17th International Conference on Formal Engineering Methods, \{ICFEM\} 2015, Paris, France, November 3-5, 2015, Proceedings ; Conference date: 01-01-2015",

}

Divakaran, S, D’Souza, D, Kushwah, A, Sampath, P, Sridhar, N & Woodcock, J 2015, Refinement-based verification of the FreeRTOS scheduler in VCC. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 9407, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9407, Springer [email protected], deu, pp. 170-186, Formal Methods and Software Engineering - 17th International Conference on Formal Engineering Methods, {ICFEM} 2015, Paris, France, November 3-5, 2015, Proceedings, 01/1/15. https://doi.org/10.1007/978-3-319-25423-4_11

Refinement-based verification of the FreeRTOS scheduler in VCC. / Divakaran, Sumesh; D’Souza, Deepak; Kushwah, Anirudh et al.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 9407 deu: Springer [email protected], 2015. p. 170-186 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9407).

Research output: Chapter in Book/Report/Conference proceeding › Chapter › peer-review

TY - CHAP

T1 - Refinement-based verification of the FreeRTOS scheduler in VCC

AU - Divakaran, Sumesh

AU - D’Souza, Deepak

AU - Kushwah, Anirudh

AU - Sampath, Prahladavaradan

AU - Sridhar, Nigamanth

AU - Woodcock, Jim

PY - 2015/1/1

Y1 - 2015/1/1

N2 - We describe our experience with verifying the schedulerrelated functionality of FreeRTOS, a popular open-source embedded real-time operating system. We propose a methodology for carrying out refinement-based proofs of functional correctness of abstract data types in the popular code-level verifier VCC. We then apply this methodology to carry out a full machine-checked proof of the functional correctness of the FreeRTOS scheduler. We describe the bugs found during this exercise, the fixes made, and the effort involved.

AB - We describe our experience with verifying the schedulerrelated functionality of FreeRTOS, a popular open-source embedded real-time operating system. We propose a methodology for carrying out refinement-based proofs of functional correctness of abstract data types in the popular code-level verifier VCC. We then apply this methodology to carry out a full machine-checked proof of the functional correctness of the FreeRTOS scheduler. We describe the bugs found during this exercise, the fixes made, and the effort involved.

UR - https://www.scopus.com/inward/record.uri?partnerID=HzOxMe3b&scp=84949186339&origin=inward

UR - https://www.scopus.com/inward/citedby.uri?partnerID=HzOxMe3b&scp=84949186339&origin=inward

U2 - 10.1007/978-3-319-25423-4_11

DO - 10.1007/978-3-319-25423-4_11

M3 - Chapter

VL - 9407

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 170

EP - 186

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

PB - Springer [email protected]

CY - deu

T2 - Formal Methods and Software Engineering - 17th International Conference on Formal Engineering Methods, {ICFEM} 2015, Paris, France, November 3-5, 2015, Proceedings

Y2 - 1 January 2015

ER -

Divakaran S, D’Souza D, Kushwah A, Sampath P, Sridhar N, Woodcock J. Refinement-based verification of the FreeRTOS scheduler in VCC. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 9407. deu: Springer [email protected]. 2015. p. 170-186. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-25423-4_11

Refinement-based verification of the FreeRTOS scheduler in VCC

Abstract

Publication series

Conference

Access to Document

Other files and links

Cite this