top-level specification and reviews to check the top-level specification against
the requirements. The formal security policy model and the formal top-level
specification are written in Z, a formal specification language, while the detailed
design derived from the top-level specification is written in CSP.