Title
Model Checking Dynamic Memory Allocation in Operating Systems
Abstract
Most system software, including operating systems, contains dynamic data structures whose shape and contents should satisfy design requirements during execution. Model checking technology, a powerful tool for automatic verification based on state exploration, should be adapted to deal with this kind of structure. This paper presents a method to specify and verify properties of C programs with dynamic memory management. The proposal contains two main contributions. First, we present a novel method to extend explicit model checking of C programs with dynamic memory management. The approach consists of defining a canonical representation of the heap, moving most of the information from the state vector to a global structure. We provide a formal semantics of the method that allows us to prove the soundness of the representation. Secondly, we combine temporal LTL and CTL logic to define a two-dimensional logic, in time and space, which is suitable to specify complex properties of programs with dynamic data structures. We also define the model checking algorithms for this logic. The whole method has been implemented in the well known model checker SPIN, and illustrated with an example where a typical memory reader/writer driver is modelled and analyzed.
Year
DOI
Venue
2009
10.1007/s10817-009-9124-y
J. Autom. Reasoning
Keywords
Field
DocType
Dynamic memory allocation,Operating systems,Model checking
Abstraction model checking,Programming language,Model checking,C dynamic memory allocation,Computer science,Theoretical computer science,Heap (data structure),Soundness,System software,State vector,Algorithm,Canonical form,Operating system
Journal
Volume
Issue
ISSN
42
2-4
0168-7433
Citations 
PageRank 
References 
12
0.63
30
Authors
3
Name
Order
Citations
PageRank
María del Mar Gallardo114113.16
Pedro Merino220125.98
David Sanán37216.51