|
Abstract : |
This paper describes an experiment evaluating the application of formal techniques to the modelling and development of a security-critical system to high (ITSEC) levels of assurance. The experiment has been done in a commercial environment by engineers working within an existing development process. Two independent teams of engineers in British Aerospace have been concurrently developing a message processing system (a trusted gateway). Both teams use CASE technology (Yourdon with Ward & Mellor's extensions supported by requirements traceability tools), but one team additionally uses the formal specification language VDM-SL. Tool support is available for both the CASE techniques and VDM-SL. In this paper we consider the merits of various forms of specification of the trusted gateway, emphasising the value of validating the specification by using it as a direct simulation of the system. 1, |
