Software Correctness Flashcards
What is the main structure of the essay? (10)
• Introduction - what is buggy software
• Why it’s important - implications
○ Medical/nuclear - fatal (Therac-25 1986-87)
○ Embedded systems - finance (Intel Pentium 1994)
○ High risk/complex science - robust (Mars Orbiter 1998)
• How to combat buggy software - preventions
○ Good software practice
○ Fault tolerance systems
○ Formal verification
○ Programming language innovations
What are implications of buggy software? (3)
- In safety-critical systems, such as nuclear reactor controllers or medical software, errors could be fatal
- In embedded and commerical systems, such as processors, errors could have financial impact due to being recalled
- In high risk/complex systems, such as scientific experiments, non robust software could be
Expand on the first implication
If software is incorrect or ‘buggy’ in a safety-critical system, such as a nuclear reactor controller or medicals surgery system, then a software error could cause loss of human life
Give an example of the first implication (2)
- Therac-25, a radiation therapy machine that killed 4 and injured 2 people in 1986-1987
- Exposed patients to massive overdoses of radiation; due to the controlling software that had bugs in it, and no hardware interlocks or fault tolerance to deal with the software bugs.
Expand on the second implication
Software errors could also have financial consequences, such as embedded systems being recalled or compensation for commercial sold systems injuring and failing.
Give an example of the second implication (2)
- Intel Pentium processor bug 1994, a bug affected the FPU and cost Intel around $400 million to recall and fix.
- The bug caused the processor to return incorrect decimal results when dividing a number.
Expand on the third implication
High risk and cost complex systems require very robust software, such as expensive scientific experiments.
Give an example of the third implication (2)
- Mars Climate Orbiter 1999, communication with the probe was lost when a software bug caused an error in a momentum adjustment.
- The software outputted the calculated the momentum adjustment in the wrong units, causing the probe to fly too close to the planet and disintegrated.
What are the ways to combat buggy software? (4)
- a. Good software practice
- b. Fault tolerance systems
- c. Formal verification
- d. Programming language innovations
a. What does good software practice mean?
Conforming to common rules of software development to improve the quality of software code
a. What is an advantage & disadvantage of good software practice? (2)
- Used to build up the integrity of software and ensure robustness and reliability
- Takes more time which could otherwise be spent implementing new features
a. What are two approaches to good software practice? (2)
- Test Driven Development (TDD)
* Code Review
a. What is Test Driven Development?
Writing tests before you write just enough production code to fulfill that test and refactoring
a. What is Code Review?
A systematic examination of source code, where a developer walks through the code
b. What are Fault Tolerance Systems?
Systems that can continue to function in presence of failures or faults in its hardware or software.
b. What is an advantage & disadvantage of Fault Tolerance Systems? (2)
- Can ensure the running of a safety critical or expensive system by implementing fail safes.
- Economic cost as well as additional space and weight required, can be impractical for systems such as space ships
b. What are two approaches to Fault Tolerance Systems? (2)
- Erlang
* Chaos Monkey
b. What is Erlang? (2)
- A programming language designed for developing robust and reliable programs for servers and embedded systems.
- The error handling mechanisms in Erlang are designed for building fault tolerant systems as opposed to simply protecting systems from program exceptions.
b. What is Chaos Monkey?
A software tool developed by Netflix engineers to ensure the robustness and resiliency of their Amazon Web Services by simulating failures of certain services bu shutting down some virtual machines.
c. What is Formal Verification?
Mathematically proving the correctness of a design with respect to a mathematical formal specification.
c. What is an advantage & disadvantage of Formal Verification? (2)
- Allows exhaustive testing of a system and defines an explicit understanding of the system
- Difficult and time consuming to write a specification using a mathematical proof instead of an English specification.
c. What are two approaches to Formal Verification? (2)
- Model Checking
* Equivalence Checking
c. What is Model Checking?
Verifies whether a particular set of properties holds true for a design.
c. What is Equivalence Checking?
Compares two versions of a design to make sure they are functionally equivalent.
