Exam: Question 2 Flashcards
PROMELA & SPIN
How do you specify real-world systems in PROMELA?
- define global variables with “#define”
- make proctypes for all processes that do logic
- add comms if needed
- add init process to start proctypes without active keyword
How do you specify real-world systems in PROMELA, using synchronous comms?
- define global variables with “#define”
- make proctypes for all processes that do logic
- add init process to start proctypes without active keyword
- set up (unidirectional) channels for each possible direction of data transfer
- set up mtype of possible message types
- set up a byte array to hold data
- add getting logic with ? and sending logic with !
How do you show whether a PROMELA system may livelock?
go through possible execution scenarios from initialisation and find if they may cause each other to infinitely compete for a resource but still perform some action or change state
What is livelock?
A livelock is similar to a deadlock, except that the states of the processes involved in the livelock constantly change with regard to one another, none progressing.
A real-world example of livelock occurs when two people meet in a narrow corridor, and each tries to be polite by moving aside to let the other pass, but they end up swaying from side to side without making any progress because they both repeatedly move the same way at the same time.
Which PROMELA construct can be used to show that between two send communication actions there is always another communication?
A trace. A trace or notrace declaration does not specify new behaviour but instead states a correctness requirement on existing behaviour in the remainder of the system.
How can you make a constraint in PROMELA to show that between two send communication actions there is always another communication?
An event trace declaration that specifies the correctness requirement that send operations on channel q1 alternate with receive operations on channel q2. It also checks that all send operations on q1 are (claimed to be) exclusively messages of type a and all receive operations on channel q2 are exclusively messages of type b. This is written as follows:
mtype = { a, b }; // message type
trace {
do
:: q1!a; q2?b
od
}
How can you show whether a PROMELA specification holds a constraint?
Consider different possible considerations to find whether or not any possible execution does not satisfy the constraint and use it as proof of counterexample; otherwise, it does holds.
What is weak fairness?
“Every process that is continuously enabled from a certain time instant onwards gets its turn infinitely often.”
What is strong fairness?
“Every process that is enabled infinitely often gets its turn infinitely often.”
What is unconditional fairness?
“Every process gets its turn infinitely often.”
What is the difference between weak, strong, and unconditional fairness?
unconditional = processes always get turns infinitely often
strong = all processes enabled infinitely often get turns infinitely often
weak = all processes constantly enabled from a given time get turns infinitely often
What does it mean to check a PROMELA property under strong/weak fairness?
!
How do you write a PROMELA never claim to prove or disprove a LTL property?
!
How do you specify real-world systems in PROMELA, using asynchronous comms?
!
How can SPIN check for livelocks?
!
What does it mean for a PROMELA specification to not terminate correctly?
!
How do you show whether it is possible for a PROMELA specification to not terminate correctly?
!
How can SPIN be used to check whether it is possible for a PROMELA specification to not terminate correctly?
!
What is an alternating bit protocol?
!
How can you model the alternating bit protocol in PROMELA?
!
