1. EMS

1) Configuration

• 3 Ambulances
• A, B in 911
• C in Hospital A
• 5 Places
• 4 House: A, B, C, D, E
• 1 School
• 8 Patients
• 4 Patients at each House
• 4 Patients at School
• 3 Hospital
• A: 1 Restroom, 1 Surgery, 3 Doctor
• B: 1 Restroom, 1 Surgery, 3 Doctor
• C: 1 Restroom, 1 Surgery, 2 Doctor
• 1 911
• 1 CS

2. Operational Requirements

• Patients at each location inform CS of their own emergency situation.
• CS informs 911 and Hospitals of the situations with respect to type of energencies at the locations.
• Each Amb moves to the locations and transport the patients as informed.
• Each Amb is directed by its proper authrity from 911 or Hospital.
• each Amb informs its target Hospital in order for the doctors at the hospital to be ready to handle the patients at its arrival.

3. Operation Specification: δ-calculus

4. SAVE : ITL Specification

5. SAVE : ITS Specification

6. EM Generation

7. Simulation

8. GTS

9. Secure Requirements

• HBP Patient to be transported to Hospital A:
• R1: (P_HBP1 :CALL((HA_HBP) ̅)→(SurgeryA:get P_HBP1)
• R2: (P_HBP2 :CALL((HB_HBP) ̅)→(SurgeryA:get P_HBP2)
• R3: (P_HBP3 :CALL((SC_HBP) ̅)→(SurgeryA:get P_HBP3)
• HD Patient to be transported to Hospital B:
• R4: (P_HD1 :CALL((HC_HD) ̅)→(SurgeryB:get P_HD1)
• R5: (P_HD2 :CALL((HD_HD) ̅)→(SurgeryB:get P_HD2)
• R6: (P_HD3 :CALL((SC_HD) ̅)→(SurgeryB:get P_HD3)
• FP patient to be transported to Hospital C:
• R7: (P_FP1 :CALL((SC_FP1) ̅)→(SurgeryC:get P_FP1)
• R8: (P_FP2 :CALL((SC_FP2) ̅)→(SurgeryC:get P_FP2)
• Doctor should prepare for treatment before patients are arrived:
• R9: (DoctorA1:in SurgeryA)<(SurgeryA:get P_HBP1)
• R10: (DoctorA2:in SurgeryA)<(SurgeryA:get P_HBP2)
• R11: (DoctorA3:in SurgeryA)<(SurgeryA:get P_HBP3)
• R12: (DoctorB1:in SurgeryB)<(SurgeryA:get P_HD1)
• R13: (DoctorB2:in SurgeryB)<(SurgeryA:get P_HD2)
• R14: (DoctorB3:in SurgeryB)<(SurgeryA:get P_HD3)
• R15: (DoctorC1:in SurgeryC)<(SurgeryA:get P_FP1)
• R16: (DoctorC2:in SurgeryC)<(SurgeryA:get P_FP2)