Colored Petri Net (CPN) is a graphical modeling language for simulation and modeling and for verification of discrete event systems. CPN allows developers to define a model in the form of reusable components. A model component is an independent element, which is specified using a formalized description, can conform to a certain component standard, has a well-defined interface, and encapsulates certain behavior. Modern components can help the developer reuse existing models according to their requirement as it reduces the cost and time of development. Composability is the capability to select and integrate various components to fulfill user requirements. Composability provides the means to achieve reusability where "reuse" is the ability of a simulation component to be reclaimed for various applications. We propose a verification framework for developers to select and assemble CPN-based components and verify their composability. The goal of this paper is to provide a pattern which helps developer in making models of concurrent systems. We present a case study of a restaurant model as proof of concept. A verified composition affirms reuse of model components in a meaningful manner by satisfying given requirement specifications.

Hajj is one of the largest mass gatherings where Muslims from all over the world gather in Makah each year for pilgrimage. A mass assembly of such scale bears a huge risk of disaster either natural or man-made. In the past few years, thousands of casualties have occurred while performing different Hajj rituals, especially during the Circumambulation of Kaba (Tawaf) due to stampede or chaos. During such calamitous situations, an appropriate evacuation strategy can help resolve the problem and mitigate further risk of causalities. It is however a daunting research problem to identify an optimal course of action based on several constraints. Modeling and analyzing such a problem of real-time and spatially explicit complexity requires a microscale crowd simulation and analysis framework. Which not only allows the modeler to express the spatial dimensions and features of the environment in real scale, but also provides modalities to capture complex crowd behaviors. In this paper, we propose an Agent-based Crowd Simulation & Analysis framework that incorporates the use of Anylogic Pedestrian library and integrates/interoperate Anylogic Simulation environment with the external modules for optimization and analysis. Hence provides a runtime environment for analyzing complex situations, e.g., emergency evacuation strategies. The key features of the proposed framework include: (i) Ability to model large crowd in a spatially explicit environment at real-scale; (ii) Simulation of complex crowd behavior such as emergency evacuation; (iii) Interoperability of optimization and analysis modules with simulation runtime for evaluating evacuation strategies. We present a case study of Hajj scenario as a proof of concept and a test bed for identifying and evaluating optimal strategies for crowd evacuation