Formal and Informal Specifications of a Secure System Component: first results in a comparative study

Fitzgerald, JS; Brookes, TM; Green, MA; Larsen, PG

doi:10.1007/3-540-58555-9_85

Formal and Informal Specifications of a Secure System Component: first results in a comparative study

Lookup NU author(s): Professor John Fitzgerald, Dr Peter Larsen

Downloads

Full text for this publication is not currently held within this repository. Alternative links are provided below where available.

Abstract

This paper presents initial results in a comparative study of formal and conventional techniques in the design of a secure system component: a trusted gateway. The operation of a trusted gateway is briefly introduced. The industrial context of its development is described, as is the form of the experiment. So far, part-formal and conventional design specifications have been produced for the trusted gateway from a common informal requirements document. As part of this process, queries have been raised against the informal requirements. These have been carefully logged, and form the subject of a preliminary analysis presented here. These first results suggest that the use of a formal specification language (in this case VDM-SL) leads to an an increased number of queries, and a bias in the specifier's concerns towards data rather than design issues.