What is dynamic testing
invoking faults and detecting failures through execution of program code on an actual execution platform
Advantages of dynamci test
quick and scalable techniques
natural extension of programming skills
Disadvantage of dynamic testing
No proof of correctness (can’t prove absence of bugs)
static analysis
approximate programme into mathematical structure
use analysis techniques to detect a fixed category of faults
refine approximate by removing false negatives
What is model checking
Translate program or spec into a behavioural model on abstract machine
Correctness properties as logical formula ( Timed computational tree logic)
check whetehr behaviour satisfies formula producing counter example if not
how model checking works
A model checker exhaustively explores all reachable execution paths of a system model and verifies whether a specified logical property holds on every path; if so, the system model satisfies the property.
what it needs:
. Finite state space
. Property expressed in logic ( we will then check propery holds in every state of state space)
Advantages of static analysis
scalable and efficient
useful for common faults ( div by 0 , null ptr …)
Disadvantages of static analysis
1) Usually for a fixed property
-Not flexible -> as they are usually for a fixed property ( will have to design your own algorithm for new type of fault not in common faults
2) possibility of false negatives
- ( as it overapproximates to ensure
soundness)
read
specify system descriptions in terms of Timed Automata ( concurrent models ) which can send messages to and from each other
Specify properties in terms of Timed Computational Tree Logic
read
Handshake: one sender ↔ one enabled receiver (blocks / deadlocks if none)
Broadcast: one sender → all enabled receivers (message lost if none)
