My graduate school research was motivated by a difficulty we have doing real creative engineering in operating systems that may seem ridiculous to people who don’t work in the field. The problem is that we can’t describe the problem. What an operating system does is complicated beyond the expressive capability of the mathematics we have at hand so we end up with vague gesturing, making applications work, and commitments to support existing APIs which are themselves mostly defined by what existing implementations do. One result is that there are embarrassing errors in nearly every commercial OS. Another result is that OS development has stagnated. Compare to databases where at least the relational algebra idea has allowed researchers to think about what the damn thing is supposed to do at some reasonable level of abstraction. Formal methods research has produced nearly nothing of use to engineers – the only useful parts have been the automated validation programs and those have advanced mostly because of the increasing power of the machines used to run the validation algorithms. All this by way of introducing another attempt to clarify the primitive recursive basis of compositional state machine theory.
Download here. (updated to improve fonts!)
Applications paper on the unfortunately acronymed Proportional Integral Derivative controllers on the way.