Industry Use
The growth in complexity of designs increases the importance of formal verification techniques in the hardware industry. 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.
As of 2011, several operating systems have been formally verified: NICTA's Secure Embedded L4 microkernel, sold commercially as seL4 by OK Labs; OSEK/VDX based real-time operating system ORIENTAIS by East China Normal University; Green Hills Software's Integrity operating system; and SYSGO's PikeOS.
Read more about this topic: Formal Verification
Famous quotes containing the word industry:
“Whatever I may be, I want to be elsewhere than on paper. My art and my industry have been employed in making myself good for something; my studies, in teaching me to do, not to write. I have put all my efforts into forming my life. That is my trade and my work.”
—Michel de Montaigne (1533–1592)
“Do not put off your work until tomorrow and the day after. For the sluggish worker does not fill his barn, nor the one who puts off his work; industry aids work, but the man who puts off work always wrestles with disaster.”
—Hesiod (c. 8th century B.C.)