Goal of the Project

The increasing use of computerised systems in all aspects of
our lives gives an increasing importance on the need for them to function
correctly. The presence of such systems in safety-critical applications,
coupled with their increasing complexity,makes the conventional method of
checking inadequate. In fact this method checks if a system behaves as
required by testing it on a representative set of scenarios. Moreover the
functional correctness and performability analysis of such systems must be
performed during their conception phases, then testing and measuring are
inadaptable. A branch of computer science which aims to resolve this problem
is *formal verification*.
The formal verification techniques which can be automated as
*model checking *are of particular
interest. First thing to do in order to verify the correctness and safetiness
of a real-life system using model checking, is to construct a model to
represent it. This model describes the set of all possible states that the
system can be in and the transitions which can occur between them. A model
checker then automatically checks through a systematic analysis of the model,
whether or not each of the specified properties is satisfied.

Model checking has been popular and successfully used in
industry. A restriction of the model checking paradigm comes from the fact
that the results of verification depend on the accuracy of the model which has
been constructed for analysis. Since verification techniques have become more
efficient and more prevalent, many people have sought to extend the
range of models and specification formalisms to whichmodel checking can be
applied. A good example is the field of *probabilistic model checking*.
Indeed the behaviour of many real-life processes is inherently stochastic.
Therefore, different formalisms in which the underlying system has been
modelled by Markovian models has been proposed. CSL for Continuous Time Markov
Chains(CTMC) [1], PCTL for Discrete Time Markov Chains (PCTL) [10] and Markov
Decision Processes [5]. Furthermore these formalisms are extended with cost
and reward models. Indeed, formal verification using model checking and
performance and dependability evaluation have a lot of things in common.
Markovian models have been largely used in performance, dependability,
availability and reliability analysis of computer and communication systems.
In order to specify the models of real systems which become more and more
large and sophisticated, high-level specification techniques as stochastic
Petri nets, stochastic process algebra, stochastic automata networks, etc.
have been proposed. Therefore it is possible to construct very large and
complex models by using a high-level specification technique. Once the model
is constructed, it is analyzed to evaluate the performability, availability
measures which are defined by steady-state or transient-state probabilities.
The possibility to express complex measures of interest can be provided by
formalisms which are extension of formal logics: Branching-time logics as
Computational Tree Logic (CTL) let us to express state-based properties and
properties over paths [10], Continuous Stochastic Logic (CSL) [1] which allows
to specify probabilistic measures over paths for CTMCs as well as standard
transient-state and steady-state measures in a compact and unambiguous way.

Stochastic model checking can be performed by numerical or statistical methods. In [19, 17], authors propose a statistical approach based on Monte Carlo simulation and statistical hypothesis testing for CSL model checking. To perform model checking by numerical analysis we need to compute transient-state or steady-state distribution of the underlying Markov chains. The numerical model checking has been studied extensively and numerous algorithms have been devised. These have been implemented in different model checkers. It is well-known that despite the considerable works in the domain, the numerical Markovian analysis still remains a problem. This problem known as the state space explosion : the state space size increases exponentially with parameter sizes of the model. Many of works have been done and are under study to overcome this problem by applyingmodel driven methods as decomposition, bounding methods, matrix geometric, stockage techniques, etc.

The reason that non-probabilistic model checking has been so successful in the real worlds is that an important amount of work has been done to develop efficient implementation techniques for it. One of the most successful approaches is symbolic model checking. For instance, Binary Decision Diagrams (BDD) are a data structure exploiting the regularity of model description via high level formalism leading in an compact representation of large models. Efficient manipulation algorithms have been developed under this data structure and its extension multi-terminal binary decision diagrams (MTBDD).