Lectures 3 and 4 - 24th September 2019 Flashcards Preview

CS4052 Logic and Software Verification > Lectures 3 and 4 - 24th September 2019 > Flashcards

Flashcards in Lectures 3 and 4 - 24th September 2019 Deck (26)
Loading flashcards...

What do atomic code blocks do in PROMELA?

They execute without interruption; all other processes wait until they are finished to prevent inter-process interference.


What are the properties of communication channels in PROMELA?

Unidirectional, specified, synchronous or asynchronous, can have one or multiple senders or receivers


How do you open and use communication channels in PROMELA?

Specify with chan type, send with !, receive with ?.


What are do blocks in PROMELA?

loops that are only broken with a break, return, etc in their code body


How does nondeterminism work in PROMELA?

Give multiple options for an operation to perform as with an NFA; all options (states) are evaluated in verification processes.


What are some ops that can be performed on comms channels in PROMELA?

length, if empty, if full, wait for specific message, and where to write received messages


Can active processes have arguments? Why?

No as they start themselves, so nothing to pass the arguments to them


Why would it make sense for the init() process to have an atomic block?

You don't want any active processes or passive processes it starts to interleave and interfere with the initialisation process


What are safety properties?

Formalised conditions to prevent unwanted behaviour or conditions from a system


What is the mutual exclusion property?

A safety property ensuring that at most one process is within a particular specified critical section of code


What are liveness properties?

Formalised conditions to ensure that some desired functionality will eventually be executed


What are the 3 main variants of liveness properties?

eventually: each process will eventually enter its critical section

repeated eventually: each process will enter its critical section infinitely often

starvation freedom: each waiting process will eventually enter its critical section


What are invariants?

A check made to ensure something is always of the same state or value: an example of a verifiable safety property which has to be true in all system states.


How are invariants implemented in PROMELA?

using the assert() method


What are labels in PROMELA?

A prefix to a statement that makes a particular location in a program's code referenceable


How can you check where a process is in its code in PROMELA?

[]@ is true iff the th process with the name is at the label


How can you extract local variables from processes in PROMELA?



What is the safe termination system property?

A safety property that checks whether all processes have reached a valid end state at the end of execution.


What is livelock?

When threads or processes are unable to progress due to them responding to each other during resource starvation, being stuck in an infinite loop of trying to get the resource.


How can you check for liveness in SPIN?

Label locations in the program as acceptable end states and check the processes reach them


What is fairness?

The evenness of the likelihood that different threads are able to advance whatever they are doing


What is unconditional fairness?

Every process gets its turn infinitely often


What is strong fairness?

Every process that is enabled infinitely often gets its turn infinitely often


What is weak fairness?

Every process that is continuously enabled from a certain time instant onwards gets its turn infinitely often


What variants of fairness can SPIN check for?

weak fairness


What are SPIN, ISPIN, and PROMELA, and how are they related?

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

ISPIN is a GUI for SPIN.

PROMELA is a verification modeling language used with the SPIN tool.