Dr David Williams
Dr David M. Williams is Lecturer in Secure Systems at the Department of Computer Science, University of Surrey. David returned to Surrey in May 2016, having previously studied for his PhD here between 2007 and 2011.
Prior to his current appointment he worked as Principal Research Engineer at Thales UK, where he worked on the design and implementation of products conforming to emerging industry standards for trust and key management. Between 2011 and 2014, David worked as Postdoctoral Researcher within the Theoretical Computer Science group at VU University Amsterdam on and NWO funded project entitled "Design and Analysis of Secure Distributed Protocols (DASDiP)".
Dr David M. Williams' PhD focused on the Formal Modelling and Analysis of Buyer-Seller Watermarking protocols. The success of his approach was evident from the number of flaws identified in published protocols proposed for copyright protection of digital content.
Dr David M. Williams is an (ISC)^2 Certified Information Systems Information Systems Security Professional.
His research interests include protocol verification, process algebra, formal methods, distributed systems, concurrency, cyber security, trusted execution environments and federated identity management.
- COM3017/COMM037 - Information Security Management (2016/17)
(LTL) properties. In particular, the results presented in this paper allow properties to be established for
abstract system models, and identify conditions to ensure that the properties (suitably translated) continue to
hold as those models are developed through refinement. There are several novel elements to this achievement:
(1) we identify conditions that allow LTL properties to be mapped across refinement chains; (2) we provide
translations of LTL predicates to reflect the introduction through refinement of new events and the renaming
and splitting of existing events; (3) we do this for an extended version of LTL particularly suited to Event-B,
including state predicates and enabledness of events, which can be model-checked at the abstract level. Our
results are more general than any previous work in this area, covering liveness in the context of anticipated
events, and relaxing constraints between adjacent refinement levels. The approach is illustrated with a case
study. This enables designers to develop event based models and to consider their execution patterns so that
liveness and fairness properties can be verified for Event-B systems.