Declarative Diagnosis of Temporal Concurrent Constraint Programs

Moreno Falaschi 1 Carlos Olarte 2, 3 Catuscia Palamidessi 2 Frank Valencia 3, 2
2 COMETE - Concurrency, Mobility and Transactions
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : We present a framework for the declarative diagnosis of nondeterministic timed concurrent constraint programs. We present a denotational semantics based on a (continuous) immediate consequence operator, TD, which models the process behaviour associated with a program D given in terms of sequences of constraints. Then, we show that, given the intended specification of D, it is possible to check the correctness of D by a single step of TD. In order to develop an effective debugging method, we approximate the denotational semantics of D. We formalize this method by abstract interpretation techniques, and we derive a finitely terminating abstract diagnosis method, which can be used statically. We define an abstract domain which allows us to approximate the infinite sequences by a finite ‘cut'. As a further development we show how to use a specific linear temporal logic for deriving automatically the debugging sequences. Our debugging framework does not require the user to either provide error symptoms in advance or answer questions concerning program correctness. Our method is compositional, that may allow to master the complexity of the debugging methodology.
Type de document :
Communication dans un congrès
Verónica Dahl and Ilkka Niemelä. 23rd International Conference in Logic Programming (ICLP'07), Sep 2007, Porto, Portugal. Springer, 4670, pp.271--285, 2007, 〈10.1007/978-3-540-74610-2_19〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00201065
Contributeur : Catuscia Palamidessi <>
Soumis le : samedi 22 décembre 2007 - 23:21:24
Dernière modification le : jeudi 10 mai 2018 - 02:06:30
Document(s) archivé(s) le : mardi 13 avril 2010 - 15:20:25

Fichier

iclp07.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Moreno Falaschi, Carlos Olarte, Catuscia Palamidessi, Frank Valencia. Declarative Diagnosis of Temporal Concurrent Constraint Programs. Verónica Dahl and Ilkka Niemelä. 23rd International Conference in Logic Programming (ICLP'07), Sep 2007, Porto, Portugal. Springer, 4670, pp.271--285, 2007, 〈10.1007/978-3-540-74610-2_19〉. 〈inria-00201065〉

Partager

Métriques

Consultations de la notice

415

Téléchargements de fichiers

99