Coordinación de servicios Webde las aplicaciones a los modelos formales

Abstract

The goal of the thesis was the application of formal methods in software engineering in order to increase the reliability of real software systems. In particular, a Web Coordination Service has been analyzed. This service is a component in several working distributed systems in the context of Location Based Services. The coordination service is based on JavaSpaces (an implementation of the Linda coordination model) and provides a set of services to communicate and synchronize heterogeneous applications distributed over the Internet. Given a real-life system, a formal model was been obtained in order to study its properties and prove that the pattern-matching process implemented in the coordination service complies with the semantics rules of Linda. Moreover, the service enables other more complex matching processes. Then, the Linda model has been extended with operations where multiple tuples are involved. These new operations supply some transactional capabilities to the coordination model. Finally, a "semi-formal" analysis of a RETE-based algorithm for the multiple reading operation was performed.