2. modelling programs with transition systems(from concurrent programs to transitions systems)
3. types of correctness properties(safety,liveness)
4.fairness assumptions and their use
5. LTL
5.1 understand LTL specifications
5.2 formalise properties in LTL
6. Automa-based LTL model checking
6.1 buchi automata and their relationship to LTL
6.2 model-checking algorithm(apply to simple examples)
7. symbolic modelling of systems(Init,Trans)
8. symbolic modelling of (boolean) programs
8.1 understand /apply encoding of different programs statements
9. symbolic model checking
9.1 algorithm for computing reachable states
9.2 checking simple safety properties
9.3 checking LTL properties
10. ROBDDs
10.1 definition, construction, variable orderings
10.2 logical operations on BDDs and their use
10.3 use of BDDs for computing reachability
Q&A
Loop invariant: it must be true in the very beginning, it's preserved by every execution including the last one. And it's always true in the loop, no matter how many times the loop executes.
Loop variant : some variables can change during each loop, so that the loop could have a condition to stop.
Describe the approach of bounded model-checking for the reachability problem.
First, we decide a positive integer k, and check whether the target is reached in k steps. We encode the BMC problem as a SAT problem then the problem become:
x, Init(x), Target(x), Trans(x,x'), K
And transferred to boolean formula k. k is satifiable if target(x) is reachable from init(x) with in k steps following trans(x,x'). If we can't reach in k steps then we try k+1 steps until we meet the bound.
What is the difference between Gray box, Black box, and White box
Black-box: creating a specification test-case without looking at code.
White-box: access / looking at the code and predict which case can fail.
Grey-box: combination of both black-box and white-box. Using specification and knowledge of the code.
What is the meaning of Failure, Fault and Error?
Failure: observed incorrect behavior with respect to the expected behavior.
Fault: a defect in software causing it to fail to perform its required function.
Error: an incorrect internal state.
What is the difference between Testing and Debugging?
Testing is concerned with finding failures, but Debugging is concerned with associating failures to faults.
What is tuple (D, Or)?
D is the test data contain (PD: input parameters, SD: initial state)
Or is an Oracle containing (R: return value, Sf: final state)
What is Statement coverage, Branch Coverage, and Condition coverage?
Statement coverage is making sure all the stages are executed
Branch coverage is making sure all the paths though are executed
Condition coverage is making sure all conditions [if-condition e.g., if((x1) || (y1))] are executed.
* if you using Brach coverage and Condition coverage, this already make sure all the cases are covered *
What is Concolic?
It is a combination of “Concrete” and “Symbolic” trying to make a progress when analysis using symbolic execution gets stuck.
