Symbolic Verification of Parallel Programs

I. Vernier

IBP-Masi 1995/03: Rapport de Recherche Masi / Masi research reports
12 pages - Février/February 1995 - Document en anglais.

PostScript : 335 Ko /Kb

Titre / Title: Symbolic Verification of Parallel Programs

Résumé : Nous proposons une solution partielle au problème de la vérification de propriétés de programmes parallèles avec un nombre fini mais non déterminé de processus. Nous considérons une sous-classe des programmes représentés par les réseaux de Petri. L'originalité de notre méthode est de construire un graphe symbolique. Les noeuds du graphe sont des prédicats qui représentent des ensembles d'états. Les propriétés exprimées par des formules de la logique temporelle arborescente CTL-X sont vérifiées sur ce graphe. Notre méthode de vérification présente des cas d'échec. Ce n'est pas surprenant car le problème est indécidable en général. Si aucun échec n'est rencontré, le graphe symbolique représente tous les états accessibles et les exécutions des programmes instanciés par un nombre de processus supérieur à une borne. L'algorithme de construction du graphe calcule cette borne.

Abstract : We propose a solution to solve part of the problem of the verification of properties of programs with a finite but unknown number of processes. We consider a subclass of parallel programs modeled with Petri nets. The originality of our method is to build a symbolic graph. The nodes of the graph are predicates that represent sets of states. Properties expressed in the branching temporal logic CTL-X are verified on this graph. Our verification method presents failure cases. This is not surprising because the problem is undecidable in the general case. If no failure cases are encountered, the symbolic graph represents all the reachable states and sequences of actions of programs instantiated with a number of processes greater than a bound. The building algorithm computes this bound.

Publications internes Masi 1995 / Masi research reports 1995