Case for Formal Methods
Another week whizzes by! I still have no clue where this is going.
Things with my thesis still look...well... incomplete.
I have been working on an essay, partially part of my thesis, but I also have plans to write some free standing blogposts about the work I have done so far. Following is a sneak peak into the essay where I introduce formal methods.
Case for Formal Methods
In 2018 two students working on their master's thesis found a critical bug in a sub-module of a self-driving vehicle. The students were translating the Lateral State Manager's program into a state machine model1. They were able to produce a counterexample trace that allowed the engineers to simulate the incorrect behavior and then provide a fix.
This is surely not a one of case. History is replete with examples of small bugs that have led to fatal accidents. The Ariane-5 exploded mid-air 37 seconds after its launch due to faulty code2. Malfunction of the Therac-25 caused radiation overdoes, killing three patients3. Knight Capital Group lost \$450m after a software update4. Another famous instance is Intel’s “Pentium FDIV bug,” a hardware bug found in 1994 leading Intel to replace defective chips, costing the company some half-billion dollars. Subsequently, Intel began to expand its staff with formal methods experts 5.
Today, safety-critical and security-critical systems are being integrated into our daily lives. For example, autonomous vehicles are soon the default and no longer a luxury. Robots are being actively used for medical surgeries 6. Software and computers are used in medical implants7,8. Many of us rely on security for online banking, shopping, and so on. The inclusion of such systems into our daily lives is coupled with their increased complexity and functionality.
With computers and automated solutions getting more and more common, these devices' safety and reliability become of paramount importance. Formal methods provide a set of tools and methods for the design of reliable systems. Formal methods are techniques used to model complex systems as mathematical entities. By building such a model, designers can then verify the system's properties. Additionally, mathematical proofs can be offered as a complement to the system tests to show correctness. Since they can provide proofs for the correctness of systems, formal methods have been proclaimed to be the best means available for developing safe and reliable systems for a long time now. To many within the research community, the necessity of formal methods is now a given. However, from an industrial perspective, this hasn't been the case.
Although there has been some level of industrial acceptance of formal methods in the last few years, it is still far from realizing its full potential. Several reasons have been suggested for this situation: lack of accessible tools, high costs, incompatibility with existing development techniques, and requiring a certain level of mathematical sophistication.
- https://ieeexplore.ieee.org/document/8256223
- https://www.bugsnag.com/blog/bug-day-ariane-5-disaster
- https://www.bugsnag.com/blog/bug-day-race-condition-therac-25
- https://www.bugsnag.com/blog/bug-day-460m-loss
-
Pentium FDIV: The processor bug that shook the world | TechRadar
20 years already
- https://techxplore.com/news/2021-01-tiny-bio-inspired-swarm-robots-medical.html
-
IoT Medical Devices Transforming Healthcare with Implants and Wearables
IoT medical devices transforming healthcare can be connected and deliver information to cloud infrastructures enabling the transmission of medical data.
- https://www.chalmers.se/en/departments/e2/news/Pages/World%E2%80%99s-first-implanted-bionic-arm-on-test-in-global-competition-.aspx