Week 10 Software Validation and Verification Flashcards
What is validation?
Making sure the software is doing the right thing. It is measured against the users needs.
What is verification?
Ensuring the software is doing things right, it is measured against the SRS and source code implementation.
What are the two types of analysis you can perform?
Dynamic analysis (testing/execution) Static analysis (verification/code)
What is formal verification? What are its 3 components
- Framework for modelling systems.
- A specification language.
- A verification method.
What are the classifications of approaches to verification?
- Proof based or model based?
- The degree of automation.
- Full vs property verification.
- Intended domain of the application.
- Pre vs post development.
What is Automated theorem proving?
A formal proof based verification.
The system description is a set of formula called the theory.
The specification is another formula called the theorem.
You need to prove that theorem conforms to the theory.
Is ATP fully automated?
No, it is very difficult and so requires manual human performance.
What is model checking?
A model based formal verification.
System is represented by a model.
Verification involves showing if M satisfies the specification.
Is model checking automatic?
Yes, usually for finite models.
What does the specification describe within ATP and Model checking
Whole behaviour or a single property.
What is the intended domain of formal verification?
Hardware/software/sequential/concurrent/reactive and terminating systems.
(ATP) What is decidability?
A verification is decidable if there is an effective procedure that decides whether the theorem is a member of the theory.
(ATP) What is decidability?
A verification is decidable if there is an effective procedure that decides whether the theorem is a member of the theory.
(ATP) What is semi-deciability?
When a verification is semi-decidable, it means that the procedure can always tell when the theorem is in the theory, however it cannot tell if the theorem is not in the theory.
How is a system described in ATP?
Utilising formal logic.
How do logical formalisms affect ATP.
It is a cost/benefit decision between automation/expressiveness/validity.
What is a shortcoming of ATP?
Logical proofs are unwieldy and time consuming, it must be done manually.
How is model checking implemented?
The system is modeled as a state machine, the specification is again written using logic.
Using logic you traverse the state machine to see if your specification holds.
This will result in either an OK or error trace.
What approach towards finding bugs does Model Checking use?
A systematic approach.
Where is Model Checking primarily used?
- Verification of control oriented properties.
- Hardware verification.
- Checking data oriented properties.
- Software checking
How are properties represented in Model Checking, what about the system?
Properties usually use temporal logic.
System is a reachability graph.
What is Linear Time (LTL) vs Branching Time (CTL) logic?
LT: Every moment has a unique successor,
-Infinite sequences (words)
CTL: Every moment has several succesors.
- Infinite tree.
How does LTL work?
- Uses connectives referring to the future
- Models time as an infinite sequence of states. (computation path)
- The future is not determined, we should several paths for different futures
- Ultimately, only one path is realised.
What is a transition system?
It is composed of 3 things.
- A set of states.
- A binary relation between states
- Labelling function, each state has a set of propositions which are true for that state.
What are reachable states?
Obtained from the initial state through a sequence of enabled transitions.
What are executions in a transition system?
The set of maximal paths.
Why is it hard to test embedded systems
Because if the input space becomes very large it is very hard to model and test these inputs.
What is the problem with model checking?
State explosion.
What is static analysis?
Static program analysis is the analysis of software without actually executing programs. Usually performed on the source code by an automated tool. Static analysis generally catches errors which result from inconsistent adherence to simple mechanical design rules.
What is human analysis of a program called?
Program comprehension or code review.
What are the key defect types that static analysis can catch?
Issues with: Security, Memory safety Resoure leaks API protocols, Exceptions Encapsulation Data races
How does SAT work?
Passes a bunch of CNF propositional clauses AND’d into the SAT.
What is SMT?
SMT recieves the propositional formula phi (also used in SAT) it then returns whether or not phi is satisfiable.
SMT can go beyond typical propositional logic can work with functions and arrays.
SMT is used by SE
How does symbolic execution work?
Rather then provide concrete values to parameters, we give them symbolic values and now the various control flow branchs that exist add extra constraints to these symbolic values. Ultimately we can solve for what values are necessary at any point in the CFG.
What are the benefits of Symbolic Execution?
It allows you to find which value or property will lead you to a certain path. This creates high test coverage.
What does a path constraint represent in symbolic execution?
All the inputs that induce program execution to go down a specific path. Solving this will give you a representative input which causes the program to go down that specific path.
What do all paths within a program form?
The programs execution tree.
What state does symbolic execution maintain instead of concrete state?
Symbolic state where each variable maps to symbolic values.
What is a path condition?
A quantifier free formula which encodes all branch decisions taken so far.
Draw the path constraints for this image.
How can you check for x/y when y = 0 using symbolic execution.
Create a branch when y = 0 and another when y != 0.
What are some issues with classic symbolic execution?
- Loops, recursion.
- Path explosion
- Heap modelling.
- SMT solver limitations.
- Environment problems/
- Coverage issue, complexity of execution tree makes it difficult to penetrate deeper.
What is concolic execution?
Concolic = Concrete + symbolic
It combines classical testing with automatic program analysis.
Also called dynamic symbolic execution.
What does DSE do?
The intention is to visit deep into the program execution tree.
Program is executed with both concrete and symbolic inputs.
Start off the execution with a random input.
Especially useful for remote procedure call.
Steps of DSE
- Generate a random input.
- Execute the program concretely and simultaneously whilst collecting all path constraints on the way.
- Negate the last conjuct.
- Solve the resulting constraint to get the concrete input for the alternative path.
How does DSE actually work?
The concrete input will explore paths randomly the symbolic execution will generate the input which will lead you down the alternative path.
Why is DSE so powerful?
It is an example of hybrid analysis,
Concrete execution guides symbolic execution, overcoming the incompleteness of the theorem prover.
Whilst symbolic execution guides concrete execution, this ultimately increases program code coverage.
How/when can ATP used in systems?
ATP is best used where there are not many changes introduced.
Best used for kernel and OS.
To sum up: Machine critical, don’t change that much ATP.
How/when can model checking be used?
To sum up, machine critical, properties to check and not many lines of code,
Use model checking.
How/when should static analysis be used?
To sum up, modules which scale very quickly or change much and which also require further testing use static analysis and particularly DSE.
