History of Formal Methods
Formal mathematical techniques have been in use from the time the Ancient Greeks such as Plato and Pythagoras. The understanding of how to use them has evolved and updated as new mathematics were discovered.
The discoveries of Newton, Leibniz, Laplace and Lagrange significantly changed the mathematical landscape that later changed the engineering landscape. George Boole described his logic and Ada Lovelace developed and proved programs for Charles Babbage to use on the first computer.
At the turn of the 20th Century Hilbert proposed his program of work to ground all existing theories to a finite, complete set of axioms, and provide a proof that these axioms were consistent - i.e. a set of formal mechanistic rules that could be followed to prove a mathematical statement. Gödel and Turing proved the limitations of this approach, but in the late 1940’s Alan Turing annotated the properties of program states to outline a proof of correctness of a sequential program.
This independently followed through the 1960’s by Floyd, Hoare and Naur who recommended using axiomatic techniques to prove programs meet their specifications and then Dijkstra used formal rules to aid the development of non-deterministic programs. This step represented the basis for Formal Methods as a separate academic discipline (more detail can be found in a paper written by B Cohen at City University).
Since then, the use of Formal Methods has steadily increased by governments and industry across the world. Various security standards evolved eventually into the Common Criteria and the UK MOD developed a software safety standard (Defence Standard 00-55) which, although not current, is still available for free download.
The analysis of programs using abstract interpretation and proof was developed in the late 1970s and early 1980s at the Royal Signals and Radar Establishment (RSRE) to develop a tool called MALPAS and, under funding from RSRE, the SPADE tool at Southampton University. RSRE also funded the development of the SPARK subset of Ada with additional funds from the Royal Aerospace Establishment the SPARK examiner tool was developed. These tools were spun out into the company Program Validation Limited (PVL) that a number of years later was acquired by Praxis Ltd. RSRE funded PVL to develop a formal semantics to a subset of the SPARK programming language. The language and proof tools were used in engine control systems, flight control systems and security applications on a number of continents.
The Z formal specification language was released under an ISO standard and the Vienna Development Method (VDM) and the B- Method were used in the development of a number of railway signalling systems in various countries. Model checking techniques were developed, notably Communicating Sequential Processes (CSP) from Oxford University and PVS and NuSMV have been the basis of a number of both government sponsored and purely industrial developments. Perhaps the most notable use of Formal techniques has been their adoption within the hardware development community and virtually all processors as used in laptops, etc. are developed using such techniques.
RSRE along with other Government research establishment was amalgamated into the Defence Evaluation and Research Agency (DERA). Through various projects and collaboration with subject matter experts around the world, the UK Government’s world renowned research agency developed tools to assist with formal verification. This culminated in supporting the certification of various systems on the Typhoon the fighter aircraft as the Agency transferred to QinetiQ plc. In 2012, D-RisQ Ltd took on the development of the tools to commercial release.
Please contact us to discuss with a D-RisQ consultant how we can help your organisation.