A Verification Framework for Component-Based Modeling and Simulation Putting the pieces together

TL;DR

This thesis presents a comprehensive verification framework for component-based modeling, focusing on verifying composability across various system types using multiple formal analysis techniques, especially targeting dynamic-semantic composability.

Contribution

It introduces a multi-level verification framework and applies three distinct formal methods to verify dynamic-semantic composability in concurrent systems.

Findings

Effective verification of dynamic-semantic composability achieved

Petri Nets and CPN-based analysis confirm model correctness

Framework supports structural and behavioral analysis of complex systems

Abstract

In this thesis a comprehensive verification framework is proposed to contend with some important issues in composability verification and a verification process is suggested to verify composability of different kinds of systems models, such as reactive, real-time and probabilistic systems. With an assumption that all these systems are concurrent in nature in which different composed components interact with each other simultaneously, the requirements for the extensive techniques for the structural and behavioral analysis becomes increasingly challenging. The proposed verification framework provides methods, techniques and tool support for verifying composability at its different levels. These levels are defined as foundations of consistent model composability. Each level is discussed in detail and an approach is presented to verify composability at that level. In particular we focus on the Dynamic-Semantic Composability level due to its significance in the overall composability correctness and also due to the level of difficulty it poses in the process. In order to verify composability at this level we investigate the application of three different approaches namely (i) Petri Nets based Algebraic Analysis (ii) Colored Petri Nets (CPN) based State-space Analysis and (iii) Communicating Sequential Processes based Model Checking. All three approaches attack the problem of verifying dynamic-semantic composability in different ways however they all share the same aim i.e., to confirm the correctness of a composed model with respect to its requirement specifications.