Verifying Dynamic Semantic Composability of BOM-Based Composed Models Using Colored Petri Nets

Model reuse is a promising and appealing convention for effective development of simulation systems as it offers reduction in development cost and time. Various methodological advances in this area have given rise to the development of different component reusability frameworks such as BOM (Base Object Model). But lack of component matching and weak support for compos ability verification and validation, in these frameworks, makes it difficult to achieve effective and meaningful reuse. In this paper we focus on Compos ability verification and propose a process to verify BOM based composed model at dynamic semantic level. We suggest an extension to the BOM components, to capture behavior at a greater detail. Then we transform the extended BOM into our proposed Colored Petri Nets (CPN) based component model so that the components can be composed and executed at an abstract level. Subsequently we advocate to use CPN tools and analysis techniques to verify that the model satisfy given requirements. We classify the properties of a system among different groups and express the model´s requirements by selecting some of the properties from these groups to form requirement specification. Also we present an example of a Field Artillery model, in which we select a set of properties as requirement specification, and explain how CPN state-space analysis technique is used to verify the required properties. Our experience confirms that CPN tools provide strong support for verification of composed models.