Title: A Verified Specification of TLSF Memory Management Allocator Using State Monads
Abstract: Formal verification of real-time services is important because they are usually associated with safety-critical systems. In this paper, we present a verified Two-Level Segregated Fit (TLSF) memory management model. TLSF is a dynamic memory allocator and is designed for real-time operating systems. We formalize the specification of TLSF algorithm based on the client requirements. The specification contains both functional correctness of allocation and free services and invariants and constraints of the global memory state. Then we implement an abstract TLSF memory allocator using state monads in Isabelle/HOL. The allocator model is built from a high-level view and the details of data structures are simplified but it covers all the behavioral principles and procedures of a concrete TLSF implementation. Finally, we verify that our TLSF model is correct w.r.t. the specification using a verification condition generator (VCG) and verification tools in Isabelle/HOL.
Publication Year: 2019
Publication Date: 2019-01-01
Language: en
Type: book-chapter
Indexed In: ['crossref']
Access and Citation
Cited By Count: 2
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot