The scheme of the modelling and verification process with Alvis is shown in Fig. 1. From the users point of view, the process starts from designing a model using prototype modelling environment called Alvis Editor. The designed model is stored using XML file format. Then it is translated into Haskell source code and its Haskell representation is used to generate the LTS graph. The Haskell functional language has been chosen as middle-stage representation of an Alvis model because Haskell is also used as a part of Alvis language i.e. Alvis uses Haskell to define parameters, data types and data manipulation functions. Haskell has been also used to implement the LTS graph generation algorithm. Such an LTS graph is stored as a Haskell list. A designer has access to such a source code, so user-defined Haskell functions (called filtering functions) that search an LTS graph for some states or parts of the graph that meet given requirements can be included into the model. The source code is compiled with GHC compiler. The results of received program execution are the LTS graph for the given model and the report of the model verification with filtering functions.