Universal Temporal Concurrent Constraint Programming - PASTEL - Thèses en ligne de ParisTech Accéder directement au contenu
Thèse Année : 2009

Universal Temporal Concurrent Constraint Programming

Programmation Concurrent par Contraintes pour Vérifier un Protocole de Sécurité

Carlos Olarte
  • Fonction : Auteur
  • PersonId : 845696

Résumé

Concurrent Constraint Programming (CCP) is a formalism for concurrency in which agents (processes) interact with one another by telling (adding) and asking (reading) information represented as constraints in a shared medium (the store). Temporal Concurrent Constraint Programming (tcc) extends CCP by allowing agents to be constrained by time conditions. This dissertation studies temporal CCP as a model of concurrency for mobile, timed reactive systems. The study is conducted by developing a process calculus called utcc, Universal Temporal CCP. The thesis is that utcc is a model for concurrency where behavioral and declarative reasoning techniques coexist coherently, thus allowing for the specification and verification of mobile reactive systems in emergent application areas. The utcc calculus generalizes tcc, a temporal CCP model of reactive synchronous programming, with the ability to express mobility. Here mobility is understood as communication of private names as typically done for mobile systems and security protocols. The utcc calculus introduces parametric ask operations called abstractions that behave as persistent parametric asks during a time-interval but may disappear afterwards. The applicability of the calculus is shown in several domains of Computer Science. Namely, decidability of Pnueli's First-order Temporal Logic, closure-operator semantic characterization of security protocols, semantics of a Service-Oriented Computing language, and modeling of Dynamic Multimedia-Interaction systems.
La Programmation Concurrente par Contraintes (CCP) est un modèle mathématique pour la spécification de systèmes concurrents où les agents (processus) ajoutent de l'information ou interrogent si certains faits peuvent être déduits. Dans ce modèle, l'information est représentée par un ensemble de contraintes. La Programmation Temporelle Concourante par Contraintes (tcc) est un extension de CCP où l'exécution des processus a lieu dans des intervalles de temps. Ce mémoire étudie tcc en tant que modèle concurrent pour les systèmes mobiles et développe le calcul de processus utcc, Universal Temporal CCP. La thèse proposée est qu'utcc est un modèle concurrent où les techniques comportementales et déclaratives peuvent être utilisées pour la spécification et la vérification des systèmes concurrents. La calcul utcc généralise tcc en permettant la possibilité de spécifier la mobilité. Ici le terme mobilité est compris comme la possibilité de communiquer des variables ou des canaux locaux comme dans le cas du pi-calcul. Utcc introduit un opérateur "ask" paramétrique que nous appelons "abstraction". Cet opérateur est persistent pendant un intervalle de temps et il disparaît au moment de passer à l'intervalle de temps suivant. Nous présentons l'utilisation d'utcc dans plusieurs domaines: Nous prouvons l'incomplétude de la logique temporelle de Pnueli, nous modélisons et vérifions des protocoles de sécurité et des systèmes dynamique d'interaction multimédia et nous donnons une sémantique déclarative à un langage pour le web-services.
Fichier principal
Vignette du fichier
thesis.pdf (1.48 Mo) Télécharger le fichier
Loading...

Dates et versions

tel-00430446 , version 1 (06-11-2009)

Identifiants

  • HAL Id : tel-00430446 , version 1

Citer

Carlos Olarte. Universal Temporal Concurrent Constraint Programming. Modeling and Simulation. Ecole Polytechnique X, 2009. English. ⟨NNT : ⟩. ⟨tel-00430446⟩
444 Consultations
1489 Téléchargements

Partager

Gmail Facebook X LinkedIn More