Advisors: I. Walukiewicz, G. Sutre and F. Herbreteau
Location: LaBRI - UMR CNRS 5800, Bordeaux, FRANCE
Keywords: model-checking, infinite-state systems, abstraction/refinment, CEGAR, partial-order methods, unfoldings
A longer presentation of the subject is available here (in french)
Subject:
Formal methods, in particular model-checking, are frequently
integrated in critical softwares development cycles, since certainties
on the software's quality and security that they ensure is precious.
However, using model-checking first requires a huge modeling work by
an expert, with a main difficulty: choosing an adequated model
granularity for being able to verify the model.
The CEGAR (Counter Example Guided Abstraction Refinement) approach has
particularly been introduced to automatically build a model (for
instance, directly from a C source code, making easier the expert's
job) which is refined incrementally such that it only contains the
informations that are necessary for model-checking the validity of the
specification.
Usually, abstraction only concerns the data that are manipulated by
the system. But, for systems of asynchronous components, the
excessive model size mainly originates in the fact that
concurrency is not handled well during model-checking. Partial-order
methods, in particular unfolding, have been introduced for preserving
and exploiting concurrency, resulting in smaller models, and tractable
and efficient verification.
Asynchronous systems (like GALS) are naturally heavily
concurrent. However, most of the time, when modeling, one can still
assume a lot more concurrency (resulting in smaller unfoldings and
more efficient model-checking) while still preserving the (in)validity
of the specification. The goal of this work is to reinforce the impact
of the unfolding technique by combining it with a CEGAR approach
handling the concurrency relation between the components. This
includes the definition of abstractions and refinements, as well as
the implementation and experimentation of the whole approach.