Brainscape's Knowledge GenomeTM

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


See full index

CS4052 Logic and Software Verification > Lectures 0 to 2 - 17th September 2019 > Flashcards

Lectures 0 to 2 - 17th September 2019 Flashcards

Formal methods and model checking

1
Q

What is logic verification?

A

Methods used to check the correctness of logical constructs

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

What is software verification?

A

Methods used to check the correctness of software and computer programs against predefined criteria and specifications.

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

What are formal methods?

A

Mathematical methods of verifying software against given specifications.

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

What is model checking?

A

Methods for formally, exhaustively, and automatically verifying finite-state concurrent systems.

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

Why is propositional logic insufficient for verifying software systems work?

A

It doesn’t allow us to talk about the future, which we must be able to do.

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

Why are formal methods useful for complex problems with multiple possibilities?

A

It’s hard to consider all possibilities when you just think about them yourself

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

What kind of systems should formal methods and verification be applied to?

A

Vital systems like ATC, flight controls, stock exchanges, and life support

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

What is fault prevention?

A

ensuring a system has no faults

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

What is fault tolerance?

A

adding compensation and handling for faults in a system’s design

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

What is a fail safe?

A

a safety barrier that ensures no fatal error arises from a fault

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

What are design faults?

A

Mistakes made in the process of planning the system which can lead to faults when the system is activated. They can be eliminated with verification methods.

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

What are fabrication faults?

A

Mistakes made with the hardware a system runs on that leads to incorrect behaviour.

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

What are usage faults?

A

Mistakes made regarding how humans use a system; for instance, wear, poor maintenance, and incorrect operation.

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

Why is fault avoidance more important in the design of hardware compared to software?

A

costs more to design and manufacture hardware; hardware bug fixes are almost impossible; higher quality is expected of hardware; time to market severely affects potential revenue

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

What is the difference between validation and verification?

A 
validation = are we building the right thing;
verification = are we building the thing right.
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
16
Q

What are the two main types of verification techniques?

A

Static and dynamic

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

What are some types of verification techniques?

A

peer review (static); software testing (dynamic); formal correctness proofs (static).

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

What can and can’t testing and simulation techniques do?

A

They can find faults but can’t guarantee their absence

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

When can you use formal verification?

A

When you have a formal model and set of requirements; you, therefore, need to be able to make a model from the problem specification

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

What are some problems with software verification?

A

can’t detect faults in hardware; result only correct if the model is; could also be errors in tools or programs that run the verification checks

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

What is a constraint solver?

A

Makes a solution directly from constraints

22
Q

What is a model checker?

A

Checks a model meets a given specification

23
Q

What is the difference between a constraint solver and model checker?

A

Constraint solver makes a solution directly from constraints, whereas a model checker checks the model used to verify a solution is correct against the initial specification

24
Q

What is model checking?

A

Using a finite state representation of a system (model) and a temporal logic-based property to check exhaustively whether the model satisfies a property

25
Q

What are formal methods?

A

Mathematical methods of verifying software against given specifications.

26
Q

What is SPIN?

A

A general tool for the logical verification of concurrent software in a rigorous and mostly automated fashion.

27
Q

What is UPPAL?

A

An integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays, etc.).

28
Q

What is PROMELA?

A

A verification modeling language used with the SPIN tool.

29
Q

What is a formal model?

A

A precise mathematical statement of the components of a system and the relationships between them

30
Q

What is a system model?

A

A state-based representation of a given system and how it works as a whole

31
Q

What is a property specification?

A

A formalised system specification that can be processed by a model checker

32
Q

How does model checking work?

A

They check if all possible states from the system model pass all property specifications (every property in each state), either passsing or failing with a counter example of when a property specification fails

33
Q

How are property specifications and system models related? How do we write this?

A

Property specifications are what a system should do, and a system model is how it does them. The system model = M and a property specification is φ. We write this as M ⊨ φ.

34
Q

What happens when a property is violated during model checking?

A

The model checker fails and gives the state and property where it fails as a counterexample.

35
Q

What are some common sources of error?

A

resource sharing, concurrency, and multithreading

36
Q

What is temporal logic?

A

Any system that can reason about propositions qualified in terms of time. For example, “I am always hungry”, “I will eventually be hungry”, or “I will be hungry until I eat something” rather than “I am hungry because x”.

37
Q

What are temporal operators?

A

A predefined operation that allows you to refer to the behaviour of a system over time

38
Q

What is property specification logic?

A

Logical systems used to define property specifications (?), such as temporal logic

39
Q

What are some useful system properties temporal logic allows us to specify?

A
  • functional correctness: does the system behave as expected?
  • reachability: is it possible to end up in a deadlock state?
  • safety: something bad never happens
  • liveness: something good will eventually happen
  • fairness: can, under certain conditions, an event occur repeatedly?
  • real-time properties: is the system acting on time?
40
Q

What is the state-space explosion problem?

A

When the number of states needed to model a complex system accurately easily exceeds the amount of available computer memory

41
Q

Which tool is PROMELA used by?

A

SPIN.

42
Q

What does the prototype keyword do in PROMELA?

A

Defines a process

43
Q

What are the two types of process in PROMELA and the difference between them?

A

Active and passive. Active processes start themselves, and passive processes must be called from another.

44
Q

What is process interleaving in PROMELA?

A

They can behave independently and execute in parallel

45
Q

Can you define global variables in PROMELA?

A

Yes

46
Q

What dies :: represent in PROMELA?

A

A nondeterministic operator - one of the options will be picked, as with a NFDA, and all will be tested

47
Q

What do naked boolean conditions do in PROMELA?

A

wait until true then continue execution

48
Q

What do label and goto statements do in PROMELA?

A

Label saves a line number, goto goes to a label

49
Q

What does the skip keyword do in PROMELA?

A

do nothing

50
Q

What are the desired properties of specification models?

A

Should be simple and small; small: carefully consider which data types should be used for the variables

CS4052 Logic and Software Verification (17 decks)

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