The National Physical Laboratory’s pioneering role in modern-day computing is well known; not least because of Alan Turing’s design of the ACE (Automatic Computing Engine) and Donald Davies’ development of packet switching.

NPL has also maintained an interest in theoretical computer science and formal methods over the years. This presentation begins with a summary of NPL’s work in this area; it includes:

  • Exploring the use of formal methods in the standardisation of communications protocols
  • A survey undertaken in the 1990s on the take up (or lack thereof) of formal methods within industry
  • Work undertaken with the Department of Computer Science of the University of York as part of the EU-funded Traceability for Computationally Intensive Metrology (TraCIM) project. This work explored the use of the formal specification language Z to provide clear, complete and unambiguous statements of mathematics to be implemented in measurement software

The presentation ends with some thoughts about how this work could be pursued further; e.g. the use of modelling languages UML and SysML.

Attendee feedback would be appreciated.


Speaker: Keith Lines


Speaker Bio:

Keith Lines applies experience gained in almost 30 years of working with NPL's scientists, administrators and support staff to help ensure that NPL activities in software development continue to meet the requirements of NPL's ISO 9001 and TickITplus certifications.

Formal aspects of computing have been an interest since he was a student at the University of Kent in the mid-1980s.

He is a member of the BCS.


Refreshments will be available from 5.15pm. The talk will start at 6pm.

Formal Methods: The National Physical Laboratory’s Experiences - FACS
Date and time
17 March, 6:00pm - 9:00pm
BCS, The Chartered Institute for IT
Ground Floor
25 Copthall Avenue