File preview
SOFTWARE SAFETY
Gerard J. Holzmann
gh@jpl.nasa.gov
IS THERE A PROBLEM?
2
PROBLEM 1: SOFTWARE GROWS
example: spacecraft control
Mariner 1969
172,000,0000 (shuttle+ground software)
KNCSL
1000000 100000 10000 1000 100 10 1 30 3000 470000 470,0000 8000 600000 175000 32000
4M
the software for Mariner 6 (1969) was 128 words of assembler: equivalent to about 30 lines in C (It had a backup control system in hardware.)
3
PROBLEM 2: RESIDUAL DEFECTS
defect insertion
reqs
design
coding
testing
residual defects after testing
defect removal defect propagation the requirements can be faulty or ambiguous and they are often incomplete for a good process: 1-10 per KNCSL for a great process: 0.1-1 per KNCSL i.e., it is rarely zero
4
PREVENTION, DETECTION, CONTAINMENT
the process we introduced at JPL
• A lab-wide coding standard focused on risk-related rules
• with automated compliance verification • A software developer certification process
• courses focused on SE principles and risk reduction
• A senior managers course, focused on software risk • many senior managers have limited exposure to software
• An emphasis on tool-based analysis (and not just people-based)
• including tool-based code review
• based on strong static source code analysis
• and daily checks for coding-rule compliance
• routine logic model checking for safety-critical parts of the design
5
SYSTEM SAFETY
Design Principles: the first layer of defense simplicity redundancy diversity
Paranoia: the second layer of defense
simplified backup
fault containment
6
SOFTWARE SAFETY
• simplicity • software modules with well-defined rules for module composition; decoupling; fire-walls • redundancy • emphasis on using assertions • N-version programming is of limited value
•J.C. Knight and N.G. Leveson, “An Experimental Evaluation of the Assumption of Independence in Multiversion Programming,” IEEE Trans. on SoftwareEngineering,Vol. SE-12, No. 1 (Jan 1986), pp. 96-109. •L. Sha. “Using Simplicity to Control Complexity,” IEEE Software, July-August 2001, pp. 20-28.
• diversity • hierarchical redundancy: hierarchies of increasingly
simple and more strongly verifiable modules
7
DO ASSERTIONS MAKE A DIFFERENCE?
MSR-TR-2006-54
“with an increase in assertion density there is a statistically significant decrease in fault density”
There are 250,000 assertions in the Microsoft Office source code (25M SLOC) i.e., 1% of the code [C.A.R. Hoare2003]
8
AN OUNCE OF PREVENTION
Source: “Customer-centered products – creating successful products through smart requirements management,” Ivy F. Hooks & Kristin A. Farry, Amacom, NY, 2001, 272 pgs, ISBN 13-978-0-8144-0568-0
“The difference between a thing that can break and a thing that can't break is that when the thing that can't break breaks then it can't be fixed.”
(Hitchhiker's Guide to the Galaxy, Book 5)
10
THE JPL CODING STANDARD FOR C LEVELS OF COMPLIANCE
• • • • • • LOC-1: language compliance LOC-2: predictable execution LOC-3: defensive coding LOC-4: code clarity LOC-5: MISRA shall compliance LOC-6: MISRA should compliance
11
THE POWER OF 10 RULES
1. 2. 3. 4. 5. 6. 7. Restrict to simple control flow constructs Do not use recursion and give all loops a fixed upper-bound Do not use dynamic memory allocation after initialization Limit functions to no more than ~60 lines of text Use minimally two assertions per function on average Declare data objects at the smallest possible level of scope Check the return value of non-void functions; check the validity of parameters 8. Limit the use of the preprocessor to file inclusion and simple macros 9. Limit the use of pointers. Use no more than N level of dereferencing 10. Compile with all warnings enabled, and use source code analyzers
http://spinroot.com/p10/
12
Gerard J. Holzmann
gh@jpl.nasa.gov
IS THERE A PROBLEM?
2
PROBLEM 1: SOFTWARE GROWS
example: spacecraft control
Mariner 1969
172,000,0000 (shuttle+ground software)
KNCSL
1000000 100000 10000 1000 100 10 1 30 3000 470000 470,0000 8000 600000 175000 32000
4M
the software for Mariner 6 (1969) was 128 words of assembler: equivalent to about 30 lines in C (It had a backup control system in hardware.)
3
PROBLEM 2: RESIDUAL DEFECTS
defect insertion
reqs
design
coding
testing
residual defects after testing
defect removal defect propagation the requirements can be faulty or ambiguous and they are often incomplete for a good process: 1-10 per KNCSL for a great process: 0.1-1 per KNCSL i.e., it is rarely zero
4
PREVENTION, DETECTION, CONTAINMENT
the process we introduced at JPL
• A lab-wide coding standard focused on risk-related rules
• with automated compliance verification • A software developer certification process
• courses focused on SE principles and risk reduction
• A senior managers course, focused on software risk • many senior managers have limited exposure to software
• An emphasis on tool-based analysis (and not just people-based)
• including tool-based code review
• based on strong static source code analysis
• and daily checks for coding-rule compliance
• routine logic model checking for safety-critical parts of the design
5
SYSTEM SAFETY
Design Principles: the first layer of defense simplicity redundancy diversity
Paranoia: the second layer of defense
simplified backup
fault containment
6
SOFTWARE SAFETY
• simplicity • software modules with well-defined rules for module composition; decoupling; fire-walls • redundancy • emphasis on using assertions • N-version programming is of limited value
•J.C. Knight and N.G. Leveson, “An Experimental Evaluation of the Assumption of Independence in Multiversion Programming,” IEEE Trans. on SoftwareEngineering,Vol. SE-12, No. 1 (Jan 1986), pp. 96-109. •L. Sha. “Using Simplicity to Control Complexity,” IEEE Software, July-August 2001, pp. 20-28.
• diversity • hierarchical redundancy: hierarchies of increasingly
simple and more strongly verifiable modules
7
DO ASSERTIONS MAKE A DIFFERENCE?
MSR-TR-2006-54
“with an increase in assertion density there is a statistically significant decrease in fault density”
There are 250,000 assertions in the Microsoft Office source code (25M SLOC) i.e., 1% of the code [C.A.R. Hoare2003]
8
AN OUNCE OF PREVENTION
Source: “Customer-centered products – creating successful products through smart requirements management,” Ivy F. Hooks & Kristin A. Farry, Amacom, NY, 2001, 272 pgs, ISBN 13-978-0-8144-0568-0
“The difference between a thing that can break and a thing that can't break is that when the thing that can't break breaks then it can't be fixed.”
(Hitchhiker's Guide to the Galaxy, Book 5)
10
THE JPL CODING STANDARD FOR C LEVELS OF COMPLIANCE
• • • • • • LOC-1: language compliance LOC-2: predictable execution LOC-3: defensive coding LOC-4: code clarity LOC-5: MISRA shall compliance LOC-6: MISRA should compliance
11
THE POWER OF 10 RULES
1. 2. 3. 4. 5. 6. 7. Restrict to simple control flow constructs Do not use recursion and give all loops a fixed upper-bound Do not use dynamic memory allocation after initialization Limit functions to no more than ~60 lines of text Use minimally two assertions per function on average Declare data objects at the smallest possible level of scope Check the return value of non-void functions; check the validity of parameters 8. Limit the use of the preprocessor to file inclusion and simple macros 9. Limit the use of pointers. Use no more than N level of dereferencing 10. Compile with all warnings enabled, and use source code analyzers
http://spinroot.com/p10/
12