next up previous
Next: 5 Status Up: High-Confidence Operating Systems 1 Previous: 3 Operational Modeling of


4 Verifying Models Against Requirements

In Section 3 we discussed how to use CCMs to model system-call interfaces. These models may be seen as detailed specifications that implementations should adhere to. In addition, other, simpler system requirements (e.g. ``a file is locked before it is accessed'') may be encoded as CCMs that act as monitors, entering bad states when an undesired system state is entered. Finally, detailed code-level CCMs can be used faithfully to model the actual behavior of a system call implementation, and can be obtained via compilation.

Given these different levels of models, one would like to check that they are in agreement, namely, that man-page models agree with requirements, that code models satisfy requirements, and that code models match man-page models. A traditional approach to handling this question involves the use of a refinement relation to check whether a given CCM refines (is faithful to) another CCM. Our methodology uses a novel, albeit mathematically equivalent, alternative that relies on the use of instrumented CCMs.

The basic idea behind this approach is the following. Given a high-level CCM (e.g., man-page model) and a lower-level one (e.g., code-level model), we use the former to track the execution of the latter. The state space of the resulting instrumented CCM is then explored to see if the wrapper ever enters a bad state (i.e., raises an unintended exception); if so, an error trace leading from the start state of the instrumented CCM is reported to the user for debugging purposes. Essentially, the instrumented CCM checks that the CCM in question refines its specification. The modularity property of refinement checking allows such checks to be performed at the level of component CCMs.

In order for the instrumented-CCM approach to verification to be practical, the state-explosion problem must be overcome: the number of states to in the instrumented CCM is likely to be intractably large. One approach to coping with state explosion is to use abstractions to eliminate distinctions between data values and thus reduce the number of distinct states. We are investigating using a combination of data and predicate abstraction [2] to obtain good abstractions.

A well-known drawback of abstraction-based techniques is the false-positive problem: a path to an error state may exist in the abstracted system that is not possible in the concrete system, owing to the loss of too much information in the abstracted conditional statements. To combat this problem our method uses counter-examples generated during reachability analysis to successively refine the data abstractions used: see the directed edge from ``Instrumented CCMs'' to ``Error'' in Figure 1. If an error trace is detected in the abstracted CCM, the trace is replayed on the unabstracted CCM to see if it is feasible. If not, conditions on transitions are modified to refine the abstracted CCM, increasing the size of its state space but eliminating the possibility of the spurious trace. We are developing an efficient algorithm for symbolically checking the feasibility of an error path in the instrumented CCM and returning the corresponding abstraction predicates if the path is not feasible.

We are also investigating the problem of constructing a minimal instrumented CCM for a given specification CCM and a corresponding implementation CCM. The smaller the wrapper (instrumentation), the smaller the overhead incurred during monitoring and verification. Once a property has been verified, its wrapper can be removed from the instrumented CCM and code, also leading to reduced overhead.


next up previous
Next: 5 Status Up: High-Confidence Operating Systems 1 Previous: 3 Operational Modeling of
Erez Zadok 2002-06-30