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.