Sidebar

Main

Internal

Trace:

Differences

This shows you the differences between two versions of the page.

--- alvis:modelling_and_verification [2013/11/09 22:09]
marcin
+++ — (current)
@@ Line 1: / Line 1: @@
-====== Modelling and verification process ======
-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.
-{{ :alvis:alvis-process.png?nolink |Fig. 1}}
-Another approach to Alvis model verification relies on using CADP toolbox. CADP offers a wide set of functionalities, ranging from step-by-step simulation to massively parallel model-checking. An Alvis LTS graph can be converted into BCG (Binary Coded Graphs) format which is one of acceptable input formats for CADP Toolbox.  Then the **CADP evaluator** is used to check whether the model satisfies requirements given as regular alternation-free μ-calculus formulae.