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


ems3_itl.png



5. SAVE : ITS Specification


ems3_its2.png


ems3_its1.png



6. EM Generation


ems3_ex.png



7. Simulation


ems3_sim.png



8. GTS


ems3_gts.png



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)
10. Verification: GTS Logic

logic.png


EMS-GTS-BO.png