Lectures 5 and 6 - 1st October 2019 Flashcards Preview

CS4052 Logic and Software Verification > Lectures 5 and 6 - 1st October 2019 > Flashcards

Flashcards in Lectures 5 and 6 - 1st October 2019 Deck (37)
Loading flashcards...
1

Why do liveness properties require more than propositional logic? What is needed instead?

Liveness properties require perspective on possible future situations. Propositional logic alone doesn't require this.

Temporal logic is needed, as it includes temporal operators that fulfil this requirement.

2

Why can safety properties mostly be written with propositional logic?

They often do not require temporal logic, as they usually just describe a property that should hold in a state.

Temporal operators are required to express properties concerning executions and not just states.

3

What are never claims in Spin/PROMELA?

Code blocks that case the program to fail and give a trace of execution to an error whenever the statements (properties) in them evaluate to being true.

4

Are statements in never claims atomic? Why?

They can be thought of as being atomic within the never claim, as they execute one-by-one. They aren't atomic overall, however, as other processes can interleave inbetween them. This is because never claims get every other turn of execution.

5

How do never claims and assert() statements compare?

Asserts are more simple but less powerful. If able, just use an assert rather than a never claim.

6

What does it mean for a never claim to succeed?

It has found an error, represented as it terminating or infinitely going out of accepting labels in a loop. It will then cease the program's execution and provide a trace of execution to the error as a counterexample of the model's correctness.

7

Does a never claim or another process execute first after global variables are initialised?

A never claim. It always executes before any other process after any global variables have been initialised.

8

How do never claims execute with other processes?

They get every 2nd turn of execution.

9

Why do loops need true nondeterministic options?

They don't continue looping by default if they can't execute any options. To keep them looping, there must always be an option they can execute - be an option they can always execute.

10

How can never claims be specified more easily?

With linear temporal logic, which is then converted into an equivalent never claim.

11

What are LTL statements composed of?

They are made of atomic propositions and boolean and temporal operators.

12

How are LTL formulae included in PROMELA specifications?

Inline in the specification after the globals and before processes, in the format ltl[]'{''}'

13

What does the operator □ represent in LTL?

always

14

What does the operator ◇ represent in LTL?

eventually

15

What does the operator X represent in LTL?

next

16

What does the operator U represent in LTL?

strong until

17

What does the operator W represent in LTL?

weak until

18

What is the difference between the strong and weak until operations?

In strong until the second operand must eventually become true. Weak until holds if the first is always true and the second never becomes true.

19

What does the operator → represent in LTL?

implies

20

Which LTL operator can be used to represent an invariant system property?

p□q

21

Which LTL operator can be used to represent a reply system property?

p◇q

22

Which LTL operator can be used to represent a guranteed reply system property?

p→◇q

23

Which LTL operator can be used to represent a progress system property?

p□ ◇q

24

Which LTL operator can be used to represent a stability system property?

p◇ □q

25

Which LTL operator can be used to represent an exclusion system property?

p→¬q

26

What are the restrictions on the temporal logic of LTL formulae?

LTL formulae can only look at the present and future, and not the past.

27

What is a trace?

Trace = trace of execution = the chronological list of states of an execution of a model up to a certain point.

28

How do you represent a trace and property?

trace = t, property = p

relate the two with t ⊨ p iff t satisfies p

29

What does it mean for a formula to be satisfied over a trace?

If the formula is true for the trace. By default, with no temporal operators, it will just be if it is true in the initial state/s. For it to be true in all, □ a is needed, for it to be true in the second state/s, X a, etc.

30

What is the difference between a trace in PROMELA/SPIN and a trace of exection?

In PROMELA, traces of execution are called trails. Traces are atomic-like constructs that hold code blocks. Traces in PROMELA force communication sequences that must be valid across all executions of a program.