RT Generic T1 Utilización de herramientas basadas enMétodos Formales para el desarrollo desistemas de comercio electrónico A1 Lorido Sánchez, Luis A1 Palazuelo Bretón, Luis A1 Romero Córdoba, Sergio A1 Serna Gil, José Luis AB El comercio electrónico es, sin lugar a dudas uno de los campos de la informáticaaplicada de mayor actualidad y previsible crecimiento en los próximos años. El mismoexige la producción de un software con garantías de seguridad que facilite la confianzade los potenciales usuarios, y con ello su rentabilidad.El comercio electrónico es un ejemplo de software distribuido. A su vez, los sistemasdistribuidos se pueden ver como una evolución de los sistemas concurrentes. Es biensabido que la programación concurrente exige un cierto soporte formal si se quieregarantizar el buen funcionamiento de los sistemas, pues en otro caso, la explosióncombinatoria de posibles ejecuciones que genera el no-determinismo, hace totalmenteimposible capturar ‘a ojo’ todas las posibles alternativas.El trabajo aquí desarrollado trata sobre el estudio y el diseño de sistemas distribuidos ysistemas basados en agentes móviles. Este documento esta estructurado en consecuenciacon esta idea, claramente diferenciado en dos bloques, un primer bloque dedicado a lossistemas distribuidos, y un segundo bloque destinado a los sistemas basados en agentesmóviles. El primer bloque consta de una primera parte de estudio sobre los métodosformales, y en concreto en el lenguaje CCS y sus variantes y como segunda parte delbloque el uso de herramientas formales, que usaremos sobre un ejemplo más o menoscomplejo. Análogamente el segundo bloque también consta de una primera parte deestudio y una segunda de aplicación práctica, en la cual detallaremos mediante cálculode ambientes, un protocolo de intercambio de claves privadas.[ABSTRACT]e-comerce is one of the most topical subjects of information tecnologies andprobably it will grow in the future. We need the production of realiable software withsecurity guarantees which inspire constumer confidence and market profits.e-comerce is an example of distributed software. And distributed software couldbe seen as an evaluation of concurrent systems. We know thet concurrent softwareneeds a formal support in order to grant a proper operation. On the other hand we couldhave too many potential different processes which are generated by the non-determinissof the system.This project is about the study and design of distributed systems and systembased in mobility agents. The structure of these documents follows this idea.We distinguish between the two blocks. The first of them is about distributedsystems and the second one is about systems based in mobility ambients.The first block has two parts, a first part ot theorical subjects about formalmethods and specificly about CCS and their variations. And a second part about formalutilities, 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 partis about the theorical subject of Ambient Calculus and the second one is about a securityprotocol which we described using Ambient Calculus. YR 2003 FD 2003 LK https://hdl.handle.net/20.500.14352/61148 UL https://hdl.handle.net/20.500.14352/61148 LA spa NO "Trabajo de la asignatura Sistemas Informáticos (Facultad de Informática, Curso 2002/2003)" DS Docta Complutense RD 2 may 2024