The temporal specification technique for operating systems mechanisms

A technique is presented for specifying properties of concurrent programs at different levels of detail. The author models the concurrent execution of several programs by interleaved execution sequences of system states. These states can contain additional global information about programs being suspended, or about current processor allocation. Then the author uses linear, propositional temporal logic for characterizing the properties of such sequences. This enables him to specify the safety and liveness properties of concurrent programming constructs such as semaphores and communication commands of CSP. He applies the technique for specifying the functions implemented by the lowest layers of an operating system, such as processor sharing and input/output, and the low-level mechanisms used for implementing these functions, such as interrupts.<>