Hendrik Tews, Tjark Weber, Erik Poll, Marko van Eekelen, and Peter van Rossum. Technical Report ICIS-R08011, Radboud University Nijmegen, May 2008.
This document contains one major result of work package 4 (kernel specification and verification) of the Robin project: a formal specification of the Nova interface. The specification consists of three main parts: (1) a definition of an abstract internal state for the Nova micro-hypervisor, (2) a description of the operations of the hypervisor in imperative pseudo-code that accesses and modifies the internal state, and (3) a combination of big-step denotational and small-step operational semantics to give semantics to the pseudo code as state modifying functions.
@techreport{tews08specification,
author = {Tews, Hendrik and Weber, Tjark and Poll, Erik and Eekelen, Marko van and Rossum, Peter van},
title = {Formal {Nova} Interface Specification},
number = {ICIS--R08011},
institution = {Radboud University Nijmegen},
month = may,
year = {2008}
}