Formal verification: Difference between revisions - Wikipedia

Line 26:

A slightly different (and complementary) approach is [[program derivation]], in which efficient code is produced from [[functional programming|functional]] specifications by a series of correctness-preserving steps. An example of this approach is the [[Bird-Meertens Formalism]], and this approach can be seen as another form of [[correct by construction|correctness by construction]].

==== Formal Verification of Operating System ====

The safety of a computer is dependent on the safety of the kernel.Functional correctness in case of a kernel means the implementation completely follows the high level abstract specifications.The common approach for ensuring safety of a kernel is by reducing the amount of privileged code thus reducing the exposure to bugs.We can guarantee absence of bugs by mathematically proving that the kernel implementation follows formal specifications and that it is free from programmer induced defects.<ref>{{cite journal|coauthors=Gerwin Klein,Kevin Elphinstone,Gernot Heiser. June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt,Rafal Kolanski , Michael Norrish , Thomas Sewell , Harvey Tuch , Simon Winwood|title=seL4: Formal Verification of an OS Kernel}}</ref>

==Verification and validation==

Line 40 ⟶ 44:

==Industry usage==

The growth in complexity of designs increases the importance of formal verification techniques in the hardware industry.<ref>{{cite journal|doi=10.1109/LICS.2003.1210044|title=Formal verification at Intel|year=2003|last1=Harrison|first1=J.|pages=45–54}}</ref><ref>[http://portal.acm.org/citation.cfm?id=800667 Formal verification of a real-time hardware design]. Portal.acm.org (1983-06-27). Retrieved on 2011-04-30.</ref> At present, formal verification is used by most or all leading hardware companies, but its use in the software industry is still languishing. This could be attributed to the greater need in the hardware industry, where errors have greater commercial significance. Because of the potential subtle interactions between components, it is increasingly difficult to exercise a realistic set of possibilities by simulation. Important aspects of hardware design are amenable to automated proof methods, making formal verification easier to introduce and more productive.<ref>[http://www.cl.cam.ac.uk/~jrh13/slides/types-04sep99/slides1.pdf Formal Verification in Industry]</ref>

Formal verification techniques prove out to be highly useful in the area of Medical science where life of a human being is at stake and accuracy of the algorithm used, for example for operating on a patient, is the most important and with in the area of aviation industry where errors are not acceptable.<ref>{{cite web|title=Formal methods|url=http://www.rspa.com/spi/formal-methods.html}}</ref>

{{As of|2011}}, several operating systems have been formally verified:

NICTA's Secure [[L4 microkernel family#University of New South Wales and NICTA | Embedded L4 microkernel]], sold commercially as [[seL4]] by OK Labs; Green Hills Software's [[Integrity (operating system) | Integrity operating system]]; and [[SYSGO]]'s [[PikeOS]].<ref>Christoph Baumann, Bernhard Beckert, Holger Blasum, and Thorsten Bormer [http://www-wjp.cs.uni-saarland.de/publikationen/Ba10EW.pdf Ingredients of Operating System Correctness? Lessons Learned in the Formal Verification of PikeOS]</ref><ref>