Publication

Automatic Fault Localization for BIP

Simon Bliudze, Qiang Wang
2015
Conference Papers

Résumé

This paper presents a novel idea of automatic fault localization by exploiting counterexamples generated by a model checker. The key insight is that, if a candidate statement is faulty, it is possible to modify (i.e. correct) this statement so that the counterexample is eliminated. We have implemented the proposed fault localization algorithm for component-based systems modelled in the BIP (Behaviour, Interaction and Priority) language, and conducted the first experimental evaluation on a set of benchmarks with injected faults, showing that our approach is promising and capable of quickly and precisely localizing faults.

Source officielle

https://infoscience.epfl.ch/entities/publication/43e6adc5-769c-4a14-8b9c-b81608d0e2d9

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Simon Bliudze, Qiang Wang
2015
Conference Papers

Résumé

Source officielle

https://infoscience.epfl.ch/entities/publication/43e6adc5-769c-4a14-8b9c-b81608d0e2d9

À propos de ce résultat

Concepts associés (8)

Autoland

Autoland désigne, en aviation, un système qui automatise la procédure d'atterrissage d'un avion tout en restant sous la supervision de l'équipage. Un tel procédé permet l'atterrissage dans des conditions météorologiques difficiles. Les systèmes d'autoland ont été conçus pour permettre un atterrissage lors d'une visibilité trop faible pour permettre un atterrissage à vue, bien qu'ils soient opérables quel que soit le niveau de visibilité.

Système d'atterrissage aux instruments

Le système d'atterrissage aux instruments ou ILS (acronyme de l'anglais instrument landing system) est un moyen de radio-navigation utilisé pour l'approche de précision d'aéronefs en régime de vol aux instruments. La procédure correspondante est appelée approche ILS. thumb|Indicateur : (de gauche à droite) trop à droite, bien centré, trop à gauche Il comprend deux éléments : un localizer (LOC) qui fournit l'écart de l'avion par rapport à l'axe de la piste ; un glide path qui fournit l'écart de l'avion par rapport à la pente nominale d'approche (le plus souvent 3 degrés).

Vérification de modèles

thumb|308x308px|Principe du model checking. En informatique, la vérification de modèles, ou model checking en anglais, est le problème suivant : vérifier si le modèle d'un système (souvent informatique ou électronique) satisfait une propriété. Par exemple, on souhaite vérifier qu'un programme ne se bloque pas, qu'une variable n'est jamais nulle, etc. Généralement, la propriété est écrite dans un langage, souvent en logique temporelle. La vérification est généralement faite de manière automatique.

Afficher plus

Publications associées (1)

Verification of Component-based Systems via Predicate Abstraction and Simultaneous Set Reduction

Simon Bliudze, Qiang Wang

This paper presents a novel safety property verification approach for component-based systems modelled in BIP (Behaviour, Interaction and Priority), encompassing multiparty synchronisation with data transfer and priority. Our contributions consist of: (1 ...

Springer2015