Using Formal Specification as a Documentation Tool: A Case Study

This paper describes an ongoing effort to use formal specification as a documentation tool for System V/MLS, an AT&T UNIX(TM) System V-based multi-level secure operating system. It is shown that by carefully embedding formal specifications into existing prose documentation, one can substantially improve the quality of the documentation. An ambiguity that existed in the original System V/MLS security policy documentation is shown to have been identified, removed, and corrected as a result of this formal approach.