State and history in operating systems
arXiv:0805.2749
Abstract
A method of using recursive functions to describe state change is applied to process switching in UNIX-like operating systems.
A method based on sequence dependent functions is used to specify and understand the operation of process switch in UNIX like systems