Scaling up Model-checking

Abstract

A typical formal development method includes specification of the functionality, formal analysis of the specification and finally code generation on to a platform. Often formal analysis is done using model-checking and scalability of model-checking is an area of concern. In this paper we describe our work on integrating two specific tools – Statemate and SAL, to scale up model-checking. More specifically we highlight the benefits, in terms of scalability, that can be obtained by exploiting peculiar usage patterns in the specifications under consideration. The paper briefly introduces the tools and their respective notations, describes a translation strategy as a means to integrate the notations, and presents how we achieved improved scalability of verification using SAL by exploiting peculiar usage of language constructs in the Statecharts of interest. We also present the results of using our tool on some randomly selected Statecharts demonstrating the scalability of our approach.