C-like Memory Model Based Verification Method for Complex Data Structures
Verification of complex data structures in the operating system kernel is an important approach to ensure high confidence of software.In order to verify the correctness of programs operating complex structures in the system,most recent methods based on high-level abstraction modeling and program structure decomposition struggle to meet the verification requirements of programs with complex data structures.In response to this problem,we propose a verification method based on the C-like memory model.First,based on memory blocks,complex data structure operations are defined and described in the form of functions,providing a formal description of the operational properties of memory objects.Second,grammar and semantics that conform to the description of complex structures are defined at the program level,and reasoning is conducted based on symbolic program logic.Experimental analysis and automated verification were conducted on complex data structures within the embedded operating system kernel of μC/OS-Ⅲ,assertions and verification condition scripts were solved using an automated theorem prover.
formal verificationcomplex data structuresprogram logicmemory modeloperating system kernel
万方数据
维普
