Alumno: Daniel Romero
Titulo Thesis: Rewriting-based Verification  and  Debugging of Web Systems

Resum

El increment de la complexitat dels sistemes Web ha donat lloc al desenvolupament de sofisticades metodologies formals per a verificar i corregir la informació i els programes a la Web.
En general, comprovar si un sistema Web es comporta correctament en respecte a la intenció original del programador així com verificar la seua consistència i correcció no son tasques trivials. La prova d'açò es la quantitat d'estudis que existixen a la lliteratura al respecte d'estes comprovacions.

A la tesis, abordem dos problemes interessants de verificació de sistemes Web. Específicament, la reparació semiautomàtica de sistemes Web i la verificació de sistemes Web dinàmics.

En primer lloc, ampliem un marc previ de verificació Web afegint una tècnica per a la reparació de sistemes Web. Proposem una metodologia de reparació bàsica junt amb distintes estratègies que permeten  optimitzar el nombre d'accions que deuen ser executades per reparar una web donada.
A més, presentem un millora del marc de verificació Web, basada en interpretació abstracta, que millora en gran mida la eficiència i la escalabilitat de la tècnica original.

En segon lloc, presentem un marc lògic de re-escritura per l'especifica-ció i 'model-checking' de aplicacions Web dinàmiques. El nostre marc, mos permet simular la navegació d'un usuari i avaluar els scripts Web dins de la aplicació Web, així com verificar importants propietats com per eixample d'abastabilitat i consistència.
Quan una propietat es refutada, es mostra un contra-eixample amb la traça errònea. Aquesta informació pot ser analitzada amb la finalitat de depurar l'aplicació Web que esta sent analitzada. Per aquest propòsit, desenvolupem una nova tècnica d'slicing cap enrere sobre les traces donades. Aquesta tècnica consisteix en buscar cap enrere, sobre la traça d'execució, els símbols rellevants del terme (o estat) en el qual estem interessats.