Reference no: EM132523808

Part : Modelling aconcurrent system using Finite State Processes (FSP) and using Label Transition System Analyser (LTSA) for model animation and property checking

Scenario: Two warring neighbours are separated by a field with wild berries. They agree to permit each other to enter the field to pick berries, but also need to ensure that only one of them is ever in the field at a time. After negotiation, they agree to the following protocol. When one neighbour wants to enter the field, he raises a flag. If he sees his neighbour's flag, he does not enter but lowers his flag and tries again. If he does not see his neighbor's flag, he enters the field and picks berries. He lowers his flag after leaving the field. Model this algorithm for two neighbours, NEIGHBOUR1 and NEIGHBOUR2. Specify the required safety property for the fieldand check that it does indeed ensuremutually exclusive access.Specify the required progress properties for the neighbours such that they both get topick berries given a fair scheduling strategy. Are there any adverse circumstances inwhich neighbors would not make progress? Whatif the neighbors are greedy?

(a) Propose an FSP specification modelling this scenario and explain your modelling choices.
(b) Check the properties mentioned and explain the results.
(c) Consider using a turn indicator (which can take the values 1 or 2) to avoid deadlock and provide an enhancedFSP specification for this scenario: if a neighbor sees his neighbour's flag and it is his neighbour's turn, he may not enter, but must try again later. Check that it does indeed avoid deadlock and satisfy the properties.

Part 3:Implementing a concurrent systemin Java.

Consider a generalisation of thea bove scenario, with N neighbours that want to access the field with wild berries and provide an implementation in Java that ensures mutual exclusion, avoids deadlock and offers a fair scheduling.

(a) Propose a Java implementation: it is not necessary to use a low-level algorithm like Paterson's, you can use any of the Java concurrency facilities.
(b) Provide a simulation program animating the system (with N>2 neighbours) and showing who is currently picking the berries, who is waiting etc.
(c) Argument (in plain English)how your Java implementation is satisfying each of the requested properties (mutual exclusion, lack of deadlock, fairness)or enhance the system with a GUI interfacein order to show graphically the concurrent execution.

The coding and fsp should be pasted into a word document but please also provide the below items too:
For these questions please also provide the lts files with the FSP processes and also the source code files for the java implementation. The learning material is also provided for support.

Attachment:- Modelling aconcurrent system.zip