Application name:

ConForm: The Experimental Development of a Trusted Gateway

Organisation:

British Aerospace (Systems & Equipment) Ltd., The Centre for Software Reliability, (University of Newcastle upon Tyne), IFAD A/S

Method:

VDM-SL

Tools:

The IFAD VDM-SL Toolbox

Domain:

Miscellaneous

Period:

13 months (part-time) during 1994 and 1995.

Size:

500-1000 lines of Visual C++ in the product

Description:

A trusted gateway reads messages (character strings) at an input port and decides the level of security of each message. The message is then output to an output post of the appropriate security level.

Two teams developed the gateway separately from the same requirements document. Both used RTM and Teamwork to record requirements and designs in Yourdon/Ward/Mellor data flow diagrams. One team additionally used VDM-SL for data types and process specifications. No formal proof or formal refinement.

System specification, software specification, implementation were all done by separate teams. Engineers had a one-week intensive training course in VDM-SL and access to outside experts on the language.

Conclusions:

Applying formal specification in the early system design phase greatly increases the rigour with which data definition and exceptional behaviour are considered. The number of queries raised against customer requirements is significantly increased. Consequently the VDM-SL trusted gateway design considers more error cases than the conventional design. Writing executable formal specifications in the system design phase allows a concrete contribution to be made to the system test plan; eases and improves confidence in the validation. The form of an executable specification may bias later software designs to use the same structure. Application was considered successful. Future application of data definition parts of VDM-SL are under consideration, especially production of reusable specifications of common message syntaxes.

Publications:

"Formal and Informal Specifications of a Secure System Component: first results in a comparative study" J.S. Fitzgerald, T.M. Brookes, M. Green and P.G. Larsen. In: M. Naftalin, T. Denvir, M. Bertran (eds.) FME'94: Industrial Benefit of Formal Methods. Proceedings of Formal Methods Europe Symposium (FME'94), LNCS 873. Springer-Verlag, 1994.

"Developing a Security-critical System using Conventional and Formal Methods". J.S. Fitzgerald, P.G. Larsen, T.M. Brookes and M. Green. To appear in M.G. Hinchey and J.P. Bowen (eds.). Applications of Formal Methods, Prentice-Hall International, Series in Computer Science. 1995.

"A Comparison of the Conventional and Formal Design of a Secure System Component". T.M. Brookes, M. Green, J.S. Fitzgerald and P.G. Larsen. In: E.V. Sorensen (ed.). Proceedings of the Nordic Seminar on Dependable Computing Systems, 1994, Technical University of Denmark, Lyngby, Denmark, Technical Report No. 352, August 1994. Also in the FACS Europe Newsletter, Vol. 1, No. 2, 1994.

Contact:

Name:	Dr. J.S. Fitzgerald
Organisation:	Centre for Software Reliability
Address:	Bedson Building University of Newcastle upon Tyne Newcastle upon Tyne NE1 7RU
Country:	UK
Phone number:	+44 (161) 2756136 or +44 (191) 2227999
Fax:	+44 (161) 2756236 or +44 (191) 2228788
E-mail:	John.Fitzgerald@newcastle.ac.uk
Personal website:	http://www.cs.man.ac.uk/fmethods/projects/essi-ConForm.html

URL:

http://www.cs.man.ac.uk/fmethods/projects/essi-ConForm.html

© copyright 2004 | Formal Methods Europe