Brainscape's Knowledge GenomeTM

Browse over 1 million classes created by top students, professors, publishers, and experts.


See full index

Software Engineering > Week 10 Software Validation and Verification > Flashcards

Week 10 Software Validation and Verification Flashcards

1
Q

What is validation?

A

Making sure the software is doing the right thing. It is measured against the users needs.

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
2
Q

What is verification?

A

Ensuring the software is doing things right, it is measured against the SRS and source code implementation.

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
3
Q

What are the two types of analysis you can perform?

A 
Dynamic analysis (testing/execution)
Static analysis (verification/code)
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
4
Q

What is formal verification? What are its 3 components

A
  1. Framework for modelling systems.
  2. A specification language.
  3. A verification method.
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
5
Q

What are the classifications of approaches to verification?

A
  1. Proof based or model based?
  2. The degree of automation.
  3. Full vs property verification.
  4. Intended domain of the application.
  5. Pre vs post development.
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
6
Q

What is Automated theorem proving?

A

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.

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
7
Q

Is ATP fully automated?

A

No, it is very difficult and so requires manual human performance.

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
8
Q

What is model checking?

A

A model based formal verification.
System is represented by a model.
Verification involves showing if M satisfies the specification.

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
9
Q

Is model checking automatic?

A

Yes, usually for finite models.

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
10
Q

What does the specification describe within ATP and Model checking

A

Whole behaviour or a single property.

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
11
Q

What is the intended domain of formal verification?

A

Hardware/software/sequential/concurrent/reactive and terminating systems.

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
12
Q

(ATP) What is decidability?

A

A verification is decidable if there is an effective procedure that decides whether the theorem is a member of the theory.

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
13
Q

(ATP) What is decidability?

A

A verification is decidable if there is an effective procedure that decides whether the theorem is a member of the theory.

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
14
Q

(ATP) What is semi-deciability?

A

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 well did you know this?
1
Not at all
2
3
4
5
Perfectly
15
Q

How is a system described in ATP?

A

Utilising formal logic.

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
16
Q

How do logical formalisms affect ATP.

A

It is a cost/benefit decision between automation/expressiveness/validity.

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
17
Q

What is a shortcoming of ATP?

A

Logical proofs are unwieldy and time consuming, it must be done manually.

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
18
Q

How is model checking implemented?

A

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.

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
19
Q

What approach towards finding bugs does Model Checking use?

A

A systematic approach.

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
20
Q

Where is Model Checking primarily used?

A
  1. Verification of control oriented properties.
  2. Hardware verification.
  3. Checking data oriented properties.
  4. Software checking
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
21
Q

How are properties represented in Model Checking, what about the system?

A

Properties usually use temporal logic.

System is a reachability graph.

22
Q

What is Linear Time (LTL) vs Branching Time (CTL) logic?

A

LT: Every moment has a unique successor,
-Infinite sequences (words)
CTL: Every moment has several succesors.
- Infinite tree.

23
Q

How does LTL work?

A
  • 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.
24
Q

What is a transition system?

A

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.
25
Q

What are reachable states?

A

Obtained from the initial state through a sequence of enabled transitions.

26
Q

What are executions in a transition system?

A

The set of maximal paths.

27
Q

Why is it hard to test embedded systems

A

Because if the input space becomes very large it is very hard to model and test these inputs.

28
Q

What is the problem with model checking?

A

State explosion.

29
Q

What is static analysis?

A

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.

30
Q

What is human analysis of a program called?

A

Program comprehension or code review.

31
Q

What are the key defect types that static analysis can catch?

A 
Issues with:
Security,
Memory safety
Resoure leaks
API protocols,
Exceptions
Encapsulation
Data races
32
Q

How does SAT work?

A

Passes a bunch of CNF propositional clauses AND’d into the SAT.

33
Q

What is SMT?

A

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

34
Q

How does symbolic execution work?

A

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.

35
Q

What are the benefits of Symbolic Execution?

A

It allows you to find which value or property will lead you to a certain path. This creates high test coverage.

36
Q

What does a path constraint represent in symbolic execution?

A

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.

37
Q

What do all paths within a program form?

A

The programs execution tree.

38
Q

What state does symbolic execution maintain instead of concrete state?

A

Symbolic state where each variable maps to symbolic values.

39
Q

What is a path condition?

A

A quantifier free formula which encodes all branch decisions taken so far.

40
Q

Draw the path constraints for this image.

A
41
Q

How can you check for x/y when y = 0 using symbolic execution.

A

Create a branch when y = 0 and another when y != 0.

42
Q

What are some issues with classic symbolic execution?

A
  • Loops, recursion.
  • Path explosion
  • Heap modelling.
  • SMT solver limitations.
  • Environment problems/
  • Coverage issue, complexity of execution tree makes it difficult to penetrate deeper.
43
Q

What is concolic execution?

A

Concolic = Concrete + symbolic
It combines classical testing with automatic program analysis.
Also called dynamic symbolic execution.

44
Q

What does DSE do?

A

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.

45
Q

Steps of DSE

A
  1. Generate a random input.
  2. Execute the program concretely and simultaneously whilst collecting all path constraints on the way.
  3. Negate the last conjuct.
  4. Solve the resulting constraint to get the concrete input for the alternative path.
46
Q

How does DSE actually work?

A

The concrete input will explore paths randomly the symbolic execution will generate the input which will lead you down the alternative path.

47
Q

Why is DSE so powerful?

A

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.

48
Q

How/when can ATP used in systems?

A

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.

49
Q

How/when can model checking be used?

A

To sum up, machine critical, properties to check and not many lines of code,
Use model checking.

50
Q

How/when should static analysis be used?

A

To sum up, modules which scale very quickly or change much and which also require further testing use static analysis and particularly DSE.

Software Engineering (5 decks)

Brainscape helps you reach your goals faster, through stronger study habits.
© 2024 Bold Learning Solutions. Terms and Conditions