Refinement-Based Hierarchical Modeling and Correctness Verification of Cross-Organization Collaborative Emergency Response Processes

When an emergency occurs, one of the important challenges is how to form an effective and timely response. An emergency disposal plan is usually organized as a series of emergency response processes manipulated by one emergency command center and several subordinate emergency organizations. Moreover, these subordinate organizations are usually geographically dispersed and need to collaborate with each other. In this case, designing and verifying such cross-organizational collaborative emergency response processes are complicated and time-consuming. To address this problem, we propose a hierarchical modeling and correctness verification approach. A general framework for hierarchical modeling and correctness verification of such processes is first introduced. Then, a top-level model and two kinds of bottom-level models (complex and simple bottom-level ones) are proposed to model such processes and collaboration patterns from different abstraction levels. Next, Petri net refinement operation is adopted to refine the top-level model by using its corresponding bottom-level models to obtain the refined model. Finally, the correctness of the refined model is verified based on reachability graph. A typical running case of cross-organization collaborative fire emergency response processes is given to validate our proposed method.