A verification algorithm for Declarative Concurrent Programming

Abstract : A verification method for distributed systems based on decoupling forward and backward behaviour is proposed. This method uses an event structure based algorithm that, given a CCS process, constructs its causal compression relative to a choice of observable actions. Verifying the original process equipped with distributed backtracking on non-observable actions, is equivalent to verifying its relative compression which in general is much smaller. We call this method Declarative Concurrent Programming (DCP). DCP technique compares well with direct bisimulation based methods. Benchmarks for the classic dining philosophers problem show that causal compression is rather efficient both time- and space-wise. State of the art verification tools can successfully handle more than 15 agents, whereas they can handle no more than 5 following the traditional direct method; an altogether spectacular improvement, since in this example the specification size is exponential in the number of agents.
Type de document :
Rapport
[Research Report] 2006
Liste complète des métadonnées

Littérature citée [1 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00081218
Contributeur : Jean Krivine <>
Soumis le : jeudi 22 juin 2006 - 15:15:56
Dernière modification le : vendredi 25 mai 2018 - 12:02:03
Document(s) archivé(s) le : lundi 5 avril 2010 - 23:14:02

Fichiers

Identifiants

Collections

Citation

Jean Krivine. A verification algorithm for Declarative Concurrent Programming. [Research Report] 2006. 〈inria-00081218〉

Partager

Métriques

Consultations de la notice

125

Téléchargements de fichiers

130