کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
422383 685078 2008 18 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
A Formal Model of Memory Peculiarities for the Verification of Low-Level Operating-System Code
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
A Formal Model of Memory Peculiarities for the Verification of Low-Level Operating-System Code
چکیده انگلیسی

This paper presents our solutions to some problems we encountered in an ongoing attempt to verify the micro-hypervisor currently developed within the Robin project. The problems that we discuss are (1) efficient automatic reasoning for type-correct programs in virtual memory, and (2) modeling memory-mapped devices with alignment requirements. The discussed solutions are integrated in our verification environment for operating-system kernels in the interactive theorem prover PVS. This verification environment will ultimately be used for the verification of the Robin micro-hypervisor. As a proof of concept we include an example verification of a very simple piece of code in our environment.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 217, 21 July 2008, Pages 79-96