Reference no: EM132485872

CTEC5723 - High Assurance System Design - De Montfort University

Learning outcome 1: Describe and evaluate fundamental formal methods concepts

Learning outcome 2: Analyse and critically review the role of formal methods in the software life cycle

Learning outcome 3: Critically evaluate the role of tools and methods supporting formal software development

Exercise 1

You are given the following vending machine specifications:

Machine N can dispense the following type of snacks: chocolate bar, packet of crisps or bag of sweets. N has 3 buttons for selecting the type of snack and 2 buttons for selecting the number of snacks: 1 or 2.

Payment can only by contactless card. The customer first selects the type of snack and then selects the number of snacks. If the number of snacks is available then the customer presents the contactless card to the card reader. If payment is approved then N will dispense the selected item and wait for the next customer. N can run out of a particular type of snack, in this case a warning will be issued to the customer that another item can be selected. The customer can either select another type of snack or choose not to have a snack. If number of snacks selected is not available then N will only dispense the available number of snacks.

Machine M is a updated version of machine N. The unhealthy chocolate bar has been replaced by the healthy cereal bar and the healthy option bag of popcorn has been added. M has therefore 4 buttons for selecting the type of snack. The operation of M is the same as N.

Machine P can dispense the the following type of healthy drinks: fruit juice, water or skimmed milk. P has currently 3 buttons for selecting the type of drink. Payment can only by contactless card. The customer first selects the type of drink and then presents the contactless card to the card reader. If payment is approved then P will dispense the selected item and wait for the next customer. P can run out of a particular drink, in this case a warning will be issued to the customer that another item should be selected. The customer will only be presented with the no drink option if P runs out of all drinks.

You are required to

Q1: Produce a model of each of the following machines together with an appropriate set of documentations which includes: the specification of the models, the models themselves, design decisions and their simulation and test cases (using JFLAP):

i) Machine N for dispensing a number of snacks.
ii) Machine M for dispensing a number of snacks.
iii) Machine P for dispensing a drink.
iv) A combined P-N machine in which a number of snacks are dispensed after the drink. Note: payment for machine P is separate from machine N.
v) A combined P-M machine in which a number of snacks are dispensed after the drink. Note: payment for machine P is separate from machine M.
vi) A combined M-P machine in which a drink is dispensed after a number of snacks. Note: payment for machine M is separate from machine P.

Q2: Explore the notion of equivalence between FSMs in general.

Investigate the condition(s) that need to be satisfied for the combined P-N machine produced in iv) and the combined P-M machine produced in v), to be equivalent.

Exercise 2

Q1: Describe informally the languages accepted by the finite state machines shown below.

i)

ii)

b)The following machine is deterministic finite state machine over the input alphabet {0; 1}

i) Construct the minimisation tree for this machine.

ii) Deduce the minimal deterministic finite state machine equivalent to this machine. Note: you should also remove unreachable states if any.

c) Given the following language.
L = {w ∈ {0; 1; 2; 3; 4; 5; 6; 7; 8; 9}+ : w is a multiple of 1000 }

i) Construct a deterministic finite state machine accepting L.
ii) Give a regular expression for the language L.

d) Draw state diagrams for nondeterministic finite machines accepting these languages.
i) (ba)* + aa*

ii) 1*(01*)*1*

e) Consider the "-transition nondeterministic finite state machine shown below.

i) Construct a nondeterministic finite state machine equivalent to this machine.
ii) Transform the machine obtained in i) into an equivalent deterministic finite state machine.

Exercise 3.

Assessment Indicators:

a) Critically analyse the limitations of finite state machines (FSM) in modelling reactive systems and discuss how these limitations are overcome in Statecharts. (Max 500 words)

b) The following is an informal description of the entry and exit system of a bio laboratory (AREA-42). AREA-42 consists of two rooms, the green room where staff put on their bio-hazard suites, and the red room where all the experiments will take place. Staff can enter and exit the green and red rooms via the two orange corridors.

The AREA-42 entry/exit system (see figure) consists of four doors D0, D1, D2 and D3 and two infrared sensors IR0 and IR1.
Initially door D0 is open, door D1 is closed, door D2 is open and door D3 is closed.

The procedure for exiting the green room and entering the red room is as follows:
• Enter the left orange corridor via door D0.
• If infrared sensor IR0 detects somebody then door D0 will close.
• If D0 is closed then door D1 will open.
If infrared sensor IR0 does not detect somebody then door D1 will close.
If door D1 is closed then the left corridor is decontaminated. This procedure takes 30 seconds.

If the decontamination procedure has completed then the door D0 will open.

The procedure for exiting the red room and entering the green room is as follows:
• Enter the right orange corridor via door D2.
• If infrared sensor IR1 detects somebody then door D2 will close.
If D2 is closed then the right corridor is decontaminated. This procedure takes 1 minute.
If the decontamination procedure has completed then the door D3 will open.
If infrared sensor IR1 does not detect somebody then door D3 will close.
• If door D3 is closed then door D2 will open.

Be aware of the following
The two decontamination procedures are different in that the left one is lethal to humans. The right one is human friendly.

As experiments in the red room are potential dangerous doors D2 and D3 should not be open at the same time. Similarly doors D0 and D1.

Specify the above AREA-42 system using Statecharts.

Check your answer by simulating that a staff member first enters the left orange corridor and then enters the red room. After a while the staff members returns to the green room via the right orange corridor.