Utilización de herramientas basadas en Métodos Formales para el desarrollo de sistemas de comercio electrónico

Abstract

El comercio electrónico es, sin lugar a dudas uno de los campos de la informática aplicada de mayor actualidad y previsible crecimiento en los próximos años. El mismo exige la producción de un software con garantías de seguridad que facilite la confianza de los potenciales usuarios, y con ello su rentabilidad. El comercio electrónico es un ejemplo de software distribuido. A su vez, los sistemas distribuidos se pueden ver como una evolución de los sistemas concurrentes. Es bien sabido que la programación concurrente exige un cierto soporte formal si se quiere garantizar el buen funcionamiento de los sistemas, pues en otro caso, la explosión combinatoria de posibles ejecuciones que genera el no-determinismo, hace totalmente imposible capturar ‘a ojo’ todas las posibles alternativas. El trabajo aquí desarrollado trata sobre el estudio y el diseño de sistemas distribuidos y sistemas basados en agentes móviles. Este documento esta estructurado en consecuencia con esta idea, claramente diferenciado en dos bloques, un primer bloque dedicado a los sistemas distribuidos, y un segundo bloque destinado a los sistemas basados en agentes móviles. El primer bloque consta de una primera parte de estudio sobre los métodos formales, y en concreto en el lenguaje CCS y sus variantes y como segunda parte del bloque el uso de herramientas formales, que usaremos sobre un ejemplo más o menos complejo. Análogamente el segundo bloque también consta de una primera parte de estudio y una segunda de aplicación práctica, en la cual detallaremos mediante cálculo de ambientes, un protocolo de intercambio de claves privadas.

[ABSTRACT] e-comerce is one of the most topical subjects of information tecnologies and probably it will grow in the future. We need the production of realiable software with security guarantees which inspire constumer confidence and market profits. e-comerce is an example of distributed software. And distributed software could be seen as an evaluation of concurrent systems. We know thet concurrent software needs a formal support in order to grant a proper operation. On the other hand we could have too many potential different processes which are generated by the non-determiniss of the system. This project is about the study and design of distributed systems and system based in mobility agents. The structure of these documents follows this idea. We distinguish between the two blocks. The first of them is about distributed systems and the second one is about systems based in mobility ambients. The first block has two parts, a first part ot theorical subjects about formal methods and specificly about CCS and their variations. And a second part about formal utilities, which we employ in orden to run and test an example made by ours. The second block also has two parts, very similar to the first block. The first part is about the theorical subject of Ambient Calculus and the second one is about a security protocol which we described using Ambient Calculus.