Peter Madden) (by way of Duncan Frissell <madden@mpi-sb.mpg.de> writes:
Applications of formal methods in software engineering depend critically on the use of automated theorem provers to provide improved support for the development of safety critical systems. Potentially catastrophic consequences can derive from the failure of computerized systems upon which human lives rely such as medical diagnostic systems, air traffic control systems and defence systems (the recent failure of the computerized system controlling the London Ambulance Service provides an example of how serious software failure can be).
and Perry responds:
I far prefer trusting robust and failsafe engineering in such situations. Theorem provers can't account for what happens when the one in a billion DRAM corruption occurs, or someone kicks the cable connecting the machine to its disks, or when a nut shoots the sensors, or whatever. Well built systems fail in a safe manner because of good engineering design -- as an example, in we hope that the motor controller might die but the motor won't eat itself anyway no matter what garbage it puts out. Such design is needed whether the systems are "formally proven" or not -- and frankly, I can't see formal proofs having much of an impact given that you are in the end simply shifting the problem to bug-free specifications and yet still have to worry about failures in the system.
Hence comes my response: I think that both formal methods and defense-in-depth are important in building an effective protection program. - Formal methods are very important for detecting flaws and producing what is commonly called "Fault Intollerance", but - Defense-in-depth is important because there are no perfect technical defenses. This is commonly called "Fault Tollerance" The most secure (and often highest quality) systems combine fault intollerance with fault tollerance to produce high quality parts and a system that continues operating safely even when those high quality parts fail. -- -> See: Info-Sec Heaven at URL http://all.net Management Analytics - 216-686-0090 - PO Box 1480, Hudson, OH 44236