Lectures 0 to 2 - 17th September 2019

Question 1

What is logic verification?

Answer 1

Methods used to check the correctness of logical constructs

Question 2

What is software verification?

Answer 2

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

Question 3

What are formal methods?

Answer 3

Mathematical methods of verifying software against given specifications.

Question 4

What is model checking?

Answer 4

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

Question 5

Why is propositional logic insufficient for verifying software systems work?

Answer 5

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

Question 6

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

Answer 6

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

Question 7

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

Answer 7

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

Question 8

What is fault prevention?

Answer 8

ensuring a system has no faults

Question 9

What is fault tolerance?

Answer 9

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

Question 10

What is a fail safe?

Answer 10

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

Question 11

What are design faults?

Answer 11

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.

Question 12

What are fabrication faults?

Answer 12

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

Question 13

What are usage faults?

Answer 13

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

Question 14

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

Answer 14

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

Question 15

What is the difference between validation and verification?

Answer 15

validation = are we building the right thing;
verification = are we building the thing right.

Question 16

What are the two main types of verification techniques?

Answer 16

Static and dynamic

Question 17

What are some types of verification techniques?

Answer 17

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

Question 18

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

Answer 18

They can find faults but can’t guarantee their absence

Question 19

When can you use formal verification?

Answer 19

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

Question 20

What are some problems with software verification?

Answer 20

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

Question 21

What is a constraint solver?

Answer 21

Makes a solution directly from constraints

Question 22

What is a model checker?

Answer 22

Checks a model meets a given specification

Question 23

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

Answer 23

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

Question 24

What is model checking?

Answer 24

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

Question 25

What are formal methods?

Answer 25

Mathematical methods of verifying software against given specifications.

Question 26

What is SPIN?

Answer 26

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

Question 27

What is UPPAL?

Answer 27

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.).

Question 28

What is PROMELA?

Answer 28

A verification modeling language used with the SPIN tool.

Question 29

What is a formal model?

Answer 29

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

Question 30

What is a system model?

Answer 30

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

Question 31

What is a property specification?

Answer 31

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

Question 32

How does model checking work?

Answer 32

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

Question 33

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

Answer 33

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 ⊨ φ.

Question 34

What happens when a property is violated during model checking?

Answer 34

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

Question 35

What are some common sources of error?

Answer 35

resource sharing, concurrency, and multithreading

Question 36

What is temporal logic?

Answer 36

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".

Question 37

What are temporal operators?

Answer 37

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

Question 38

What is property specification logic?

Answer 38

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

Question 39

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

Answer 39

* 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?

Question 40

What is the state-space explosion problem?

Answer 40

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

Question 41

Which tool is PROMELA used by?

Answer 41

SPIN.

Question 42

What does the prototype keyword do in PROMELA?

Answer 42

Defines a process

Question 43

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

Answer 43

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

Question 44

What is process interleaving in PROMELA?

Answer 44

They can behave independently and execute in parallel

Question 45

Can you define global variables in PROMELA?

Answer 45

Yes

Question 46

What dies :: represent in PROMELA?

Answer 46

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

Question 47

What do naked boolean conditions do in PROMELA?

Answer 47

wait until true then continue execution

Question 48

What do label and goto statements do in PROMELA?

Answer 48

Label saves a line number, goto goes to a label

Question 49

What does the skip keyword do in PROMELA?

Answer 49

do nothing

Question 50

What are the desired properties of specification models?

Answer 50

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