In the recently started and still ongoing research reported here, the ASM (Abstract State Machines) method is used as a practically viable method for defining, in a rigorous but concise way, satisfactory models for OS kernels and to prove properties of interest for them. A main goal is to make these models refinable in a controllable way to executable code.
OS Kernel Model
in: V. Diekert, K. Weicker, N. Weicker (Eds): Informatik als Dialog zwischen Theorie und Anwendung. Festschrift fuer Volker Claus zum 65.Geburtstag. Vieweg+Teubner, Wiesbaden 2009, ISBN 978-3-8348-0824-0
ModelingMessagePassing
in: Proc.ABZ'2010, Springer LNCS 5977 pp.20-33 ISBN 978-3-642-11810-4