A Framework for Automatic Construction of Abstract Promela Models

One of the current trends in model checking for the verification of concurrent systems is to reduce the state space produced by the model, and one of the more promising ways to achieve this objective is to support some kind of automatic construction of more abstract models. This paper presents a proposal in this direction. The main contribution of the paper is the definition of a semantics framework which allows us to relate different models of the system, each one with a particular abstraction level. Automatic source-to-source transformation is supported by this formal basis. The method is applied to Promela models.