Executive Summary : | Model checking is an automated software verification technique which is widely used to establish the correctness, safety, reliability and dependability of complex software and hardware systems. Model checking involves capturing the qualitative or quantitative behavior of a complex system using a graph-based mathematical model and checking if it satisfies a formally described qualitative or quantitative property. These mathematical models can be broadly classified into two categories, namely, state-labeled and action-labeled models. Action-labeled models, e.g., labeled transition systems, action-labeled discrete-time/continuous-time Markov chains are more commonly used as semantic model for amongst others qualitative and quantitative variants of process algebras, and Petri nets. To compare the behavior of action-labeled models, several linear-time and branching-time equivalences have been proposed. In contrast, state-of-the-art model checkers, e.g. nuSMV, PRISM, and Storm can be used to efficiently verify qualitative and quantitative properties, e.g., linear temporal logic, computation tree logic, probabilistic computation tree logic, and continuous stochastic logic formulae interpreted over qualitative/quantitative state-labeled models, e.g. Kripke structures, state-labeled discrete-time/continuous-time Markov chains. Although both these categories of models are regarded to be on an equal footing, no progress has been made in the past to propose a unified framework of model and logic transformation functions/embeddings, and use it to develop tools which enables one to utilize the state-of-the-art minimization and formal verification machinery implemented in one domain for model minimization and analysis in the other domain. In other words, a uniform framework which can bridge the gap between these two important qualitative (quantitative, respectively) design and verification communities has not been proposed previously. The two main objectives of this project are as follows: 1) propose a uniform framework of model embeddings and logic embeddings which would enable one to analyze, minimize and verify process algebraic models using state-of-the-art state-based model checking tools and vice versa, 2) to use this theoretical framework to design, develop and implement a user-friendly, free to use, open-source prototypical toolset called GALTOSM, which will connect the modeling and verification machinery from the action-labeled and state-labeled domains. This tool would also us to connect several widely used model checkers, e.g. nuSMV and PRISM with mCRL2 and CADP, respectively. |