Towards the verification of RAISE specifications through Model Checking

Abstract

Ensuring the correctness of a given software component has become a crucial aspect in Software Engineering and the Model Checking technique provides a fully automated way to achieve this goal. In particular, the usage of Model Checking in formal languages has been reinforced in the last decades because the specifications themselves provide an abstraction of the problem under study (whether created by abstraction from the software or by hand) and the properties validated at the specification level can be warrantied to be preserved until implementation. In this paper we focus on the main issues for adding Model Checking functionalities to the RAISE specification language and present the most important characteristics of our current approach for doing so. An outline of the main issues and problems faced in the process and possible ways to solve them are also presented.