Title: µQC: a property-based testing framework for L4 microkernels

Authors: Cosmin Dragomir; Lucian Mogosanu; Mihai Carabas; Razvan Deaconescu; Nicolae Tapus

Addresses: Faculty of Automatic Control and Computers, University POLITEHNICA of Bucharest, Splaiul Independentei nr. 313, Sector 6, Bucuresti, Romania ' Faculty of Automatic Control and Computers, University POLITEHNICA of Bucharest, Splaiul Independentei nr. 313, Sector 6, Bucuresti, Romania ' Faculty of Automatic Control and Computers, University POLITEHNICA of Bucharest, Splaiul Independentei nr. 313, Sector 6, Bucuresti, Romania ' Faculty of Automatic Control and Computers, University POLITEHNICA of Bucharest, Splaiul Independentei nr. 313, Sector 6, Bucuresti, Romania ' Faculty of Automatic Control and Computers, University POLITEHNICA of Bucharest, Splaiul Independentei nr. 313, Sector 6, Bucuresti, Romania

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.

Keywords: software testing; property-based testing; L4 microkernel; application programming interface; API.

DOI: 10.1504/IJCCBS.2018.091826

International Journal of Critical Computer-Based Systems, 2018 Vol.8 No.1, pp.1 - 24

Accepted: 24 Aug 2017
Published online: 18 May 2018 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article