Reference no: EM133070205

Question 1) Discuss the importance and the role of model checking as a complement to the traditional testing.

Question 2) Explain why security protocols are a good example of a domain where model checking techniques may be applied successfully.

Question 3) Consider the following transition system depicted in Figure 1, with all the states, transitions and state variables. There are four propositional variables p, q, r and s. All of them are false in the initial state s0, p and s are true in the state s1, q is true in the state s2, q and r are true in the state s3, and so on. Express the following properties in CTL and state whether they hold in the transition system. If a property does not hold then show a counter example.

(i) Always, in the next state q is false.

(ii) There is a possibility that the system never reach a state where r is true

(iii) Always, r is false until q is true

Figure 1. An example transition system

Question 4) What is busy-waiting in multi-threading programming? Discuss when it can be useful in improving the performance of a multi-threading application.

Question 5) Consider the mutual exclusion protocol for two processes shown below:
//Shared variables boolean c1 = false, c2 = false;
int turn = 1;
Process P1: Process P2:
init1; init2;
while(true){ while(true){
//entry protocol //entry protocol
turn = 2; c1 = true; turn = 1; c2 = true; while(c2 && turn ==2){ } while(c1 && turn == 1) { }
crit1; crit2;
//exit protocol //exit protocol
c1 = false; c2 = false;
rem1; rem2;
} }

where init1 and init2 are non-critical initialisations, crit1 and crit2 are critical sections and rem1 and rem2 are non-critical remainders of the programs. Does the protocol satisfy the properties of Mutual Exclusion, Absence of deadlock, and Eventual Entry? If not, give an example trace that results in the property being violated and fix the algorithm using only standard C-like instructions as in the original algorithm so that it satisfies all the properties.

Question 6) Consider the following two processes that share a common variable X and a semaphore S:
// Shared variable int X =2;
binary semaphore S = 1;
Process P1: Process P2:
//initialisation code //initialisation code int Y; int Z;
P(S); P(S);

P11: Y = 2*X; P21: Z = X+1;
P12: X = Y; P22: X = Z;
V(S); V(S);
//other code //other code

The line numbers P11, P12 and P21, P22 have been added to the left of each statement. How many different values of X are possible after both processes finish executing? What are those values? Explain your answer showing all the possible execution traces.

Question 7) Consider the following transition relation and write the corresponding NuSMV code.

Question 8) State for each Linear-time Temporal Logic (LTL) formula whether it is legal or not (p and q are propositional variables).
(i) Gp
(ii) AGp
(iii) EG(p->Fq)
(iv) (pUq)
(v) GFp

Question 9) Consider the following transition diagram and state whether the CTL formula AFAG p and the LTL formula FGp hold or not. Justify your answer.

Attachment:- Exam Paper Template.rar