Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation
The reliability and security of safety-critical real-time systems are of utmost importance
because the failure of these systems could incur severe consequences (eg, loss of lives or …
because the failure of these systems could incur severe consequences (eg, loss of lives or …
Integrating formal schedulability analysis into a verified OS kernel
Formal verification of real-time systems is attractive because these systems often perform
critical operations. Unlike non real-time systems, latency and response time guarantees are …
critical operations. Unlike non real-time systems, latency and response time guarantees are …
Complx: A verification framework for concurrent imperative programs
S Amani, J Andronick, M Bortin, C Lewis… - Proceedings of the 6th …, 2017 - dl.acm.org
We propose a concurrency reasoning framework for imperative programs, based on the
Owicki-Gries (OG) foundational shared-variable concurrency method. Our framework …
Owicki-Gries (OG) foundational shared-variable concurrency method. Our framework …
Secure mathematically-assured composition of control models
The Secure Mathematically-Assured Composition of Control Models project SMACCM has
developed new tools for building UAV software that is provably secure against many classes …
developed new tools for building UAV software that is provably secure against many classes …
Toward compositional verification of interruptible os kernels and device drivers
An operating system (OS) kernel forms the lowest level of any system software stack. The
correctness of the OS kernel is the basis for the correctness of the entire system. Recent …
correctness of the OS kernel is the basis for the correctness of the entire system. Recent …
Compositional virtual timelines: verifying dynamic-priority partitions with algorithmic temporal isolation
Real-time systems power safety-critical applications that require strong isolation among
each other. Such isolation needs to be enforced at two orthogonal levels. On the micro …
each other. Such isolation needs to be enforced at two orthogonal levels. On the micro …
[PDF][PDF] Type Systems for Systems Types
L O'Connor - 2019 - unsworks.unsw.edu.au
Type Systems for Systems Types Page 1 Type Systems for Systems Types Author: O'Connor,
Liam Publication Date: 2019 DOI: https://doi.org/10.26190/unsworks/21495 License: https://creativecommons.org/licenses/by-nc-nd/3.0/au …
Liam Publication Date: 2019 DOI: https://doi.org/10.26190/unsworks/21495 License: https://creativecommons.org/licenses/by-nc-nd/3.0/au …
A generic approach for the certified schedulability analysis of software systems
Embedded systems often need to react in a timely manner. Life-critical or mission-critical
ones require assurance that they comply with these real-time requirements. In particular …
ones require assurance that they comply with these real-time requirements. In particular …
CleanQ: a lightweight, uniform, formally specified interface for intra-machine data transfer
R Haecki, L Humbel, R Achermann, D Cock… - arXiv preprint arXiv …, 2019 - arxiv.org
We present CleanQ, a high-performance operating-system interface for descriptor-based
data transfer with rigorous formal semantics, based on a simple, formally-verified notion of …
data transfer with rigorous formal semantics, based on a simple, formally-verified notion of …
Analyzing FreeRTOS Scheduling Behaviors with the Spin Model Checker
CK Lin, BY Wang - arXiv preprint arXiv:2205.07480, 2022 - arxiv.org
FreeRTOS is a real-time operating system with configurable scheduling policies. Its
portability and configurability make FreeRTOS one of the most popular real-time operating …
portability and configurability make FreeRTOS one of the most popular real-time operating …