ΜQC: a property-based testing framework for L4 microkernels. (2018)

• Record Type: Journal Article
• Authors: Dragomir, Cosmin; Mogosanu, Lucian; Carabas, Mihai; Deaconescu, Razvan; Tapus, Nicolae
• Is Part Of: International journal of critical computer-based systems. Volume 8:Number 1(2018)
• Page Start: 1
• Page End: 24
• Publication Date: 2018
• Subjects: software testing -- property-based testing -- L4 microkernel -- application programming interface -- API; Computer systems -- Periodicals; Computer architecture -- Periodicals; 004
• Languages: English
• ISSNs: 1757-8779

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.