Verification of asynchronous systems by abstraction/refinement of concurrency

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.