Submission Date: 23/Oct/2022 (no extensions)

Submission Format: 1 file called <your-upi>.tgz containing the following:

a.) A promela file, including the LTL formulas for Q1.

b.) A python script encoding a working SMT formulation for Q2.

c.) A pdf file/report explaining the results obtained from SPIN/SMT solvers for Q1 and Q2.

NOTE: Your code should be well commented

Q1.) This question  relates to your understanding of model-checking LTL properties on concurrent processes.

Part-A

Model Petersons mutual exclusion algorithm as described below in Promela.

The basic idea behind Peterson’s n-process mutual exclusion algorithm is

that each process passes through n−1 stages before entering the critical section (cs). These stages are designed to block one process per stage so that after n−1 stages     only one process will be eligible to enter the critical section (which we consider      as stage n). The algorithm uses two integer arrays step and pos of sizes n − 1           and n respectively: pos is an array of 1-writer multi-reader variables and step is       an array of multi-writer multi-reader variables. The value at step[j] indicates the      latest process at stepj, and pos[i] indicates the latest stage that the process i is         passing through. (Peterson uses Q for pos, and TURN for step.) The array pos          is initialized to 0. The process id’s, pids, are assumed to be integers between 1         and n. The code segment for process i is given in Figure 1.

Figure – 1

Part-B

Represent the following properties in LTL and verify them against at least 2 processes from above.

Property- 1 (Safety property): Multiple processes cannot enter the ciritical section together.                Property-2 (Liveness property): If a process is waiting, eventually it will enter the critical section.    Property-3 (Liveness property): Any process not in the critical section will eventually enter the critical section.