cliff@cs.man.ac.uk (Cliff Jones) (06/07/90)
A Case Study in Formal Methods THE WORKSHOP ** 10 July 1990 ** The increasing demand for high quality software has recently been underlined by the emergence of draft standards on safety related computer systems. In particular, the UK MoD Defence standard Def Stan 00-55 (Requirements for the Procurement of Safety Critical Software in Defence Equipment) mandates the use of formal methods and has focussed attention on what methodologies and tools can be used in the formal specification, development and verification of high integrity software. The purpose of the workshop is to give a simple but detailed example, especially for those with little knowledge of formal methods, which demonstrates some of the benefits to be obtained by using formal specifications. The case study to be discussed illustrates how a formal specification language (VDM) has been used to specify an international (ISO) banking standard which describes an approved message authenticator algorithm (MAA). Knowledge of VDM or the banking standard is not required. Comprehensive supporting documentation will be provided and there will be ample opportunity for discussion. The workshop will be presented by staff of the Software Engineering Group in NPL's Division of Information Technology and Computing, and by members of Program Validation Ltd. PROVISIONAL PROGRAMME 09.30 Registration and Coffee 10.00 Outline 10.15 Introduction to the MAA 10.45 Introduction to VDM 11.15 MAA in VDM 12.15 Discussion 12.30 Luncheon 13.45 Reassemble 14.00 Validation of the specification 14.30 Formal development of software 15.30 Tea 16.00 VDM tools 16.30 Discussion 17.00 Close For registration forms (or further information) please contact: G I Parkin (X7006, gip@seg.npl.co.uk) or G O'Neill (X7016, gon@seg.npl.co.uk) National Physical Laboratory, Teddington, Middlesex, TWLL 0LW. Telephone: 081 977 3222 (Switchboard) or 081 943 7006/7016.