Using formal reasoning on a model of tasks for FreeRTOS

DOI10.1007/s00165-014-0308-9zbMath1328.68044OpenAlexW2051536083MaRDI QIDQ903515

Deepak D'Souza, Shu Cheng, J. C. P. Woodcock

Publication date: 6 January 2016

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-014-0308-9

zbMATH Keywords

formal verificationFreeRTOSverified software initiativeZ/Eves

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theory of operating systems (68N25)

Related Items (1)

Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency

Uses Software

• Isabelle
• RAISE
• PVS
• ProofPower
• VeriFast
• Z/EVES
• Z
• FreeRTOS
• seL4

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Operating system verification---an overview
• Integrated formal methods. 6th international conference, IFM 2007, Oxford, UK, July 2--5, 2007. Proceedings.
• seL4 Enforces Integrity
• Z/Eves and the Mondex Electronic Purse
• The verified software initiative

This page was built for publication: Using formal reasoning on a model of tasks for FreeRTOS