µQC: a property-based testing framework for L4 microkernels Online publication date: Fri, 18-May-2018
by Cosmin Dragomir; Lucian Mogosanu; Mihai Carabas; Razvan Deaconescu; Nicolae Tapus
International Journal of Critical Computer-Based Systems (IJCCBS), Vol. 8, No. 1, 2018
Abstract: As the complexity of software is increasing, traditional testing methods are unable to provide a high level of assurance for critical software systems, particularly operating system kernels, which represent the root of trust in computing systems. At the same time, formal verification is costly and difficult even for small system software such as microkernels, which are relied on for applications with high security and/or safety requirements, e.g., automotive and cellular radio. Our work closes a trade-off between the strong guarantees of formal verification and the flexibility of traditional software testing methods such as unit testing. We argue that this trade-off can be readily closed by property-based testing. In this paper we present µQC, a property-based testing framework for L4 microkernels. We illustrate our prototype by evaluating a significant subset of the L4 API (threading and scheduling) starting from its specification.
Existing subscribers:
Go to Inderscience Online Journals to access the Full Text of this article.
If you are not a subscriber and you just want to read the full contents of this article, buy online access here.Complimentary Subscribers, Editors or Members of the Editorial Board of the International Journal of Critical Computer-Based Systems (IJCCBS):
Login with your Inderscience username and password:
Want to subscribe?
A subscription gives you complete access to all articles in the current issue, as well as to all articles in the previous three years (where applicable). See our Orders page to subscribe.
If you still need assistance, please email subs@inderscience.com
Our Blog 
Follow us on Twitter 
Visit us on Facebook