During this period the ICL High Assurance Team has undertaken a variety of applications in the secure systems area as well as a major technology development R&D project which has resulted in the ICL ProofPower system, a proof tool supporting formal reasoning in Higher Order Logic and Z.
Lead the team engaged in the formal modelling and verification of the OWR, a device developed by ICL under contract to HMG and certified by HMG as ``exceeding the requirements for UKL6'' (a level of assurance corresponding to DoD A1 level), probably the most highly assured secure device in the world. Contributed to consultancy contracts for HMG concerning methods for the formal modelling of secure systems and the application of those methods to secure systems developments for HMG.
Conceived of the FST project ``Foundations and Tools for Formal Verification'', established the project and managed through to a succesful conclusion resulting in the ProofPower system supporting formal specification and proof in Higher Order Logic and Z, including prototype support for the Spark Annotation Language..
Made an important technical contribution to the approach to support of Z in HOL, including formal specifications of the semantic mappings. Involved in the ongoing development of the Z standard.
January 1986 - November 1987
Formal Methods consultant applying formal methods to high assurance secure systems.
Contributed to early formal modelling work for CESG, undertaking the first translation of formal models from Z to HOL for purposes of formal proof. Played a leading role in the establishment of techniques for using HOL to reason about specifications in Z.