Composability Verification of Complex Systems Using Colored Petri Nets

Abstract

The discipline of component-based modeling and simulation offers promising gains including reduction in development cost, time, and system complexity. This paradigm is becoming quite profitable as it promotes the use and reuse of modular components for adequate development of complex simulations. Achieving effective and meaningful model reuse through the composition of components still remains a daunting challenge. “Composability”, an integral part of this challenge, is the capability to select and assemble model components in various combinations to satisfy specific user requirements. Different researches in this area have given rise to the development of different component reusability frameworks. However, lack of support for composability verification makes it difficult to achieve effective and meaningful reuse. For this reason there is a need for an adequate framework to verify and validate composability of composed models and ensure the satisfaction of desired system properties. In this thesis we propose the use of Colored Petri Nets for component oriented model development, model composition and the verification of composed models using state-space analysis technique. We present a case study of an elevator model as a proof of concept. Our case study explains the proposed process of developing and composing CPN based model components, and verifying the composed model using state-space analysis. A verified composition asserts meaningful reuse of model components by satisfying given requirement specifications.