Title: Towards Formal Verification of Dynamic Memory Allocator Properties Using BIP Framework
Abstract: Dynamic storage allocation (DSA) algorithms play an important role in the Real-Time Operating systems (RTOSs) community. It allows the RTOS to use limited memory efficiently. To ensure the DSA properties of a dynamic memory allocator, it is important to verify the implementation of its DSA algorithms. However, most previous works ignore memory interactive behaviors and just verify individually each function involved in DSA. Our main contribution in this paper is to verify the consistency of the memory interactive properties and its implementation. For this purpose, we use the BIP (Behavior, Interaction, Priority) Framework to deal with abstract behaviors, properties, and cross references to implementation code. We chose the TLSF as a testbed for formal verification of dynamic memory allocator properties and have produced a verification of TLSF. Both the behavior operations and property requirements of the TLSF have been specified in the BIP framework and the entire verification process is automated.
Publication Year: 2021
Publication Date: 2021-10-19
Language: en
Type: article
Indexed In: ['crossref']
Access and Citation
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot