The organizing principle of our approach is that an ounce of modeling is worth a pound of debugging. In particular, we advocate the use of formal operational modeling as a methodology that can fundamentally and dramatically improve how OS software, and indeed any low-level system software, is developed. We envision these models being used throughout the OS development and deployment process, as active (i.e., executable) documentation for designers and application developers; as mechanically analyzable requirements and design artifacts; and as bases for reliable implementations.
The specific modeling formalism we are using, concurrent class machines (CCMs) , extends basic finite-state machines with features capturing a variety of object-oriented (OO) concepts, including classes and inheritance, objects and object creation, method invocation and exceptions, multithreading, guarded commands, and abstract collection types. The CCM model builds on our previous work in the formal modeling of hierarchic reactive systems, e.g. , and provides an intuitive, graphical notation for modeling system behavior at different levels of abstraction. In contrast with existing OO design notations, CCMs also possess a mathematically precise operational semantics that defines the execution steps that CCM models can engage in; this semantics makes CCM models candidates for a variety of different mechanical analyses. Figure 1 shows how CCMs provide a uniform basis for requirements analysis, verification, and code generation:
A central idea in our approach is that of an instrumented CCM, where a CCM describing the implementation of an OS system call is combined with the CCM of the corresponding system-call interface or CCM of the requirements. Man-page CCMs can also be instrumented by combining them with requirements CCMs they must adhere to.