Week 2: Promela I Flashcards
What is ProMeLa?
Promela is a verification modelling language for specifying concurrent processes
What is the focus of ProMeLa?
It is the modelling of process interaction
What are the possible results of bugs in concurrent processes?
- Deadlocks
- Race conditions
- Livelocks
What software does Promela use to check its models?
The Spin Model Checker
What does mtype do in ProMeLa?
It defines a custom data type (similar to ENUM) by enumerating its valid values
What functions prints in ProMeLa?
printf
How are loops expressed in ProMeLa?
With do…od statements
What is an option in ProMeLa?
A sequence of actions that a process executes in a single loop iteration
What is the minimum number of options a loop requires in ProMeLa?
1
What is the maximum number of options that can be selected at the beginning of each iteration?
1
What is an option’s guard?
An expression that may be evaluated to either true or false
What happens when two or more options can be selected in one iteration?
One of them is chosen randomly
What is non-determinism?
It is a condition in which two or more choices can be made and a selection of them cannot be influenced by the environment
What are the two types of non-determinism?
- Process-level determinism: which manifests when, within a process, two or more statements are selectable for execution
- System-level determinism: which manifests when two or more concurrent processes are each ready to execute one or more statements, in which case one process is non-deterministically scheduled for execution
