SAVE/ADOxx
글 수 8
2016.06.29 15:17:03 (*.70.193.131)
5975
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)
10. Verification: GTS Logic