Lectures 5 and 6 - 1st October 2019 Flashcards
Never claims, LTL formulae, and Trace
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.
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.
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.
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.
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.
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.
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.
How do never claims execute with other processes?
They get every 2nd turn of execution.
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.
How can never claims be specified more easily?
With linear temporal logic, which is then converted into an equivalent never claim.
What are LTL statements composed of?
They are made of atomic propositions and boolean and temporal operators.
How are LTL formulae included in PROMELA specifications?
Inline in the specification after the globals and before processes, in the format ltl[]’{‘’}’
What does the operator □ represent in LTL?
always
What does the operator ◇ represent in LTL?
eventually
What does the operator X represent in LTL?
next
