Controlled owicki-gries concurrency: reasoning about the preemptible eChronos embedded operating system

Carroll Morgan
Carroll Morgan

MARS, 2015.

Cited by: 11|Bibtex|Views38|DOI:https://doi.org/10.4204/EPTCS.196.2
EI
Other Links: academic.microsoft.com|dblp.uni-trier.de|arxiv.org

Abstract:

We introduce a controlled concurrency framework, derived from the Owicki-Gries method, for describing a hardware interface in detail sufficient to support the modelling and verification of small, embedded operating systems (OS's) whose run-time responsiveness is paramount. Such real-time systems run with interrupts mostly enabled, inclu...More

Code:

Data:

Full Text
Your rating :
0

 

Tags
Comments