Improving the verification capabilities of ComMA : Master Thesis

Designing and maintaining robust interfaces for software components of component-based systems is a challenging task. To address this issue, TNO-ESI and Philips have employed model-driven engineering techniques by creating ComMA (Component Modelling and Analysis Suite), a framework that has been successfully used in the industry. This framework offers a toolset that aims to improve the methodology of updating and developing software interfaces by allowing users to define interface and component specifications, from which several artifacts can be generated, such as test clients, runtime monitors, simulators, as well as visualizations and documentation. Before using such specifications as input for a generation task, certain properties need to be verified in order to check that a model is consistent with regard to its expected behavior. Recently, an integrated model checking approach has been developed to support lightweight verification. This enables the verification of several properties on interface models but only on a bounded part of the behavior. This project aims to integrate novel state-of-the-art model checking techniques within the ComMA framework in order to verify more types of properties on larger, more complex specifications in a scalable manner. A literature study was conducted, which focused on techniques for tackling the state space explosion problem, such as symbolic approaches and reduction techniques, as well as various standalone model checkers, their strategies, and possible integration with ComMA. Upon conducting a feasibility study, ITS-tools was chosen as the most appropriate model checker to be used as a verification back-end, for the problem context. A comprehensive conceptual model-to-model mapping has been developed to facilitate the translation of ComMA models into the input formalism of ITS-tools, namely the Guarded Action Language (GAL). This mapping has been specifically designed to cater to both interface and component models. Compared to the current verification methodology, the new solution’s benefits and limitations were evaluated using industrial examples. Additionally, a case study demonstrates how verifying properties on component models is now possible, which is currently not supported. The chosen methodology allows for
the scalable verification of reachability, CTL, and LTL properties on interface and component models. These models can include multiple communicating interfaces and sub-components, as well as higher-order rules on the communication protocol known as functional constraints.