کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
422387 685078 2008 18 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
CVM – A Verified Framework for Microkernel Programmers
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
CVM – A Verified Framework for Microkernel Programmers
چکیده انگلیسی

CVM (communicating virtual machines) is a computational model for concurrent user processes interacting with a generic microkernel—supporting virtual memory—and devices. In this paper, we introduce the computational models needed to define CVM. Furthermore, we describe how CVM can be implemented by means of a concrete kernel, thus providing a trustworthy platform for microkernel programmers. Last but not least, we give an overview on the model formalization and implementation correctness proof, which has been conducted in the interactive theorem prover Isabelle for the most part. An endeavor like this is tedious and of a considerable complexity. Thus, we do not try to present all details, but provide references to publications covering specific aspects.

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