A Framework for Abstract Interpretation of Timed Concurrent Constraint Programs

Moreno Falaschi 1 Carlos Olarte 2 Catuscia Palamidessi 2
2 COMETE - Concurrency, Mobility and Transactions
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : Timed Concurrent Constraint Programming (tcc) is a declarative model for concurrency offering a logic for specifying reactive systems, i.e. systems that continuously interact with the environment. The universal tcc formalism (utcc) is an extension of tcc with the ability to express mobility. Here mobility is understood as communication of private names as typically done for mobile systems and security protocols. In this paper we consider the denotational semantics for tcc, and we extend it to a "collecting" semantics for utcc based on closure operators over sequences of constraints. Relying on this semantics, we formalize the first general framework for data flow analyses of tcc and utcc programs by abstract interpretation techniques. The concrete and abstract semantics we propose are compositional, thus allowing us to reduce the complexity of data flow analyses. We show that our method is sound and parametric w.r.t. the abstract domain. Thus, different analyses can be performed by instantiating the framework. We illustrate how it is possible to reuse abstract domains previously defined for logic programming, e.g., to perform a groundness analysis for tcc programs. We show the applicability of this analysis in the context of reactive systems. Furthermore, we make also use of the abstract semantics to exhibit a secrecy flaw in a security protocol. We have developed a prototypical implementation of our methodology and we have implemented the abstract domain for security to perform automatically the secrecy analysis.
Type de document :
Article dans une revue
Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, ACM, 2009, Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programming, pp.207-218. 〈10.1145/1599410.1599436〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00426608
Contributeur : Catuscia Palamidessi <>
Soumis le : mardi 27 octobre 2009 - 01:15:01
Dernière modification le : jeudi 11 janvier 2018 - 06:22:13
Document(s) archivé(s) le : mardi 16 octobre 2012 - 12:45:30

Fichier

ppdp21-olarte.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Moreno Falaschi, Carlos Olarte, Catuscia Palamidessi. A Framework for Abstract Interpretation of Timed Concurrent Constraint Programs. Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, ACM, 2009, Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programming, pp.207-218. 〈10.1145/1599410.1599436〉. 〈inria-00426608〉

Partager

Métriques

Consultations de la notice

435

Téléchargements de fichiers

170