Fault Localization and Explanation for Concurrent Programs

When:
01/05/2018 – 02/05/2018 all-day
2018-05-01T02:00:00+02:00
2018-05-02T02:00:00+02:00

Annonce en lien avec l’Action/le Réseau : aucun

Laboratoire/Entreprise : INRIA Grenoble – LIG
Durée : 3 years
Contact : vincent.leroy@univ-grenoble-alpes.fr
Date limite de publication : 2018-04-31

Contexte :
Recent computing trends promote the development of hardware and software applications that are intrinsically parallel, distributed, and concurrent. Designing and developing such systems has always been a tedious and error-prone task, and the ever increasing system complexity is making matters even worse. Although we are still far from proposing techniques and tools avoiding the existence of bugs in a system under development, we know how to automatically chase and find bugs that would be very difficult, if not impossible, to detect manually.

Model checking [1] is an established technique for automatically verifying that a model, e.g., a Labelled Transition System (LTS), obtained from higher-level program languages such as process algebra satisfies a given temporal property, e.g., the absence of deadlocks. When the model violates the property, the model checker returns a counterexample, which is a sequence of actions leading to a state where the property is not satisfied. Understanding this counterexample for debugging the specification is a complicated task for several reasons: (i) the counterexample can contain hundreds (even thousands) of actions, (ii) the debugging task is mostly achieved manually (satisfactory automatic debugging techniques do not yet exist), (iii) the counterexample does not explicitly highlight the source of the bug that is hidden in the model, and (iv) the counterexample describes only one occurrence of the bug and does not give a global view of the problem with all its occurrences.

Sujet :
https://jobs.inria.fr/public/classic/fr/offres/2018-00510

The objective of this PhD Thesis is to propose and develop new solutions for understanding and summarizing the origin of bugs detected by model checking techniques. To do so, we would like first to find adequate models for representing not only the semantics of the corresponding concurrent program (LTS) but also the structure of the program. This latter information is particularly useful once the source of the bug has been identified in the model and we want to show to the developer where it occurs in the corresponding program.

Second, we plan to provide analysis techniques combining model checking and data mining techniques in order to identify what parts of the model caused the bug. We will start from the notion of choices proposed in [2] where the model moves from a correct to an incorrect behaviour. These choices turned out to be very relevant from a debugging perspective because they identify portions of the code that may be the source of the bug. To favour usability of our approach, we will revisit graph mining and visualization to propose new visualization techniques by highlighting these choices in the models.

Finally, we will use the information computed in the aforementioned steps for building an abstracted and summarized explanation of the origin of the bug. To do so, we plan to reuse notions such as the concepts of sufficient and necessary behaviour, the distance to the bug or the probability of the bug occurrence from a specific position in the program.

Two complementary ideas will be study during this PhD Thesis. First, we will try to propose debugging techniques for counterexamples produced in the context of equivalence checking techniques where two programs are compared with respect to an equivalence notion, and counterexamples show all differences between these two programs. Second, we will see whether our techniques could go one step further by not only detecting the source of the bug but also by proposing a solution to automatically repair the bug and obtain a correct program.

Complementary information:

. Bibliography
[1] Principles of Model Checking. Christel Baier and Joost-Pieter
Katoen. MIT Press, 2008
[2] Gianluca Barbon, Vincent Leroy, Gwen Salaün:
Debugging of Concurrent Systems Using Counterexample Analysis. FSEN 2017: 20-34

. Supervisors
Gwen Salaun is full professor at Université Grenoble Alpes and member of the CONVECS team.
Gregor Goessler is Inria researcher and head of the SPADES team.
Vincent Leroy is associate professor at Université Grenoble Alpes.

. Keywords
Debugging, Model Checking, Temporal Logic, Counterexample, Bug Localization, Concurrent Programs, Behavioural Models, Data Visualization, Equivalence Checking, Code Repair.

Profil du candidat :
. Education: MSc/Master 2 research in Computer Science

Formation et compétences requises :
. Knowledge of formal methods (concurrency theory) and verification
. Knowledge of data mining and data visualization is a plus
. Candidates who enjoy programming would be appreciated, as the work will include software development
. Good command of English, French is a plus

Adresse d’emploi :
Ville : Montbonnot
Centre Inria : CRI Grenoble – Rhône-Alpes

Document attaché :