Verification Flashcards
What is validation?
Validation ensures that the software systems meets the customers expectations
(are we building the right system?)
What is verification?
Verification ensures correctness against system specification
(are we building the system right?)
Static Verification Techniques
do not require executing the program
- code review
- static checking (automated analyses)
- formal verification (program satisfies formal property)
Dynamic Verification Techniques
require a program to be executed
- Testing
- runtime monitoring (check for safety/security vialoations)
Code review - definition
structured inspection process, performed in a team, to find possible defects
Code review - advantages and obstacles
+ distribute knowledge among team
+ can find defects before they show in tests
+ can improve code quality
+ no executable system required
- only work well when properly conducted
- team members may feel criticized or not productive
Steps in test Design
- identify and analyze the responsibilities of the IUT
- add test cases based on
- use case, design, minimal successs guarantess - determine how verdict is reached through providing expected results
-> testing must be based on fault model
Which aspects of testing can be automated?
- running the tests
- generating test inputs
- generating test verdict (test oracle)
What can be achieved by testing?
establish sufficient trust into the system
Definition - Test (Data) Point
is a specific value for
- a test case input or
- a state variable
Definition - Test Case
consists of
- pretest state of the IUT
- test point/ condition
- expected results
Definition - Test Suite
Collection of test cases
Definition - Test Run
execution of a test suite on the IUT
Structural Coverage - Statement Coverage (SC)
all statements were executed at least once
Structural Coverage - Basic Block Coverage (BBC)
(Basic Block: max sequence of instructions without branch points)
all basic block are executed at least once
Structural Coverage - Branch Coverage (BC)
all edges in the CFG were executed at least once
Structural Coverage - Path Coverage (PC)
all path in the CFG were executed at least once
unachievable in practice
Logic Coverage - Decision Coverage (DC)
any decisions in the program were at least once false and once true
(desicion: a < b && c == d)
Logic Coverage - Condition Coverage (CC)
any conditions in the program were at least once false and once true
(condition: a < b, c == d (from a < b && c == d))
Logic Coverage - Modifies Condition-Decision Coverage (MCDC)
for one occurrence condition c in decision d
- d evaluates at least twice
- once where c is false
- once where c is true
- d evaluates differently in both cases
- and other conditions in d evaluated identically or not evaluated at least once
(often required when developing safety-critical software)
Automated Test Case Generation
White Box
- Syntactic approaches: scanning for contitions, evaluation -> suitable to achieve logic based coverage criteria
- Symbolic execution: unwinding CFG with symbolic values -> suitable to achieve also structural coverage criteria
Black Box
- analysis of input data or model of IUT
Automatic Static Verification Techniques
Static Checking (based on CFG)
- Runtime exceptions, liveness, information flow
- fully automated
- many false positives
- scales reasonably well
Bug Finding
