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

• Main Author: Olarte, Carlos
• Language: ENG
• Published: Ecole Polytechnique X 2009
• Subjects: [INFO:INFO_MO] Computer Science/Modeling and Simulation; Programmation Concurrent par Contraintes; sécurité; sémantiques
• Online Access: http://tel.archives-ouvertes.fr/tel-00430446; http://tel.archives-ouvertes.fr/docs/00/43/04/46/PDF/thesis.pdf

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.