{\rtf1\ansi\ansicpg1252\cocoartf1038\cocoasubrtf350
{\fonttbl\f0\fswiss\fcharset0 Helvetica;}
{\colortbl;\red255\green255\blue255;}
\paperw11900\paperh16840\margl1440\margr1440\vieww9000\viewh8400\viewkind0
\pard\tx566\tx1133\tx1700\tx2267\tx2834\tx3401\tx3968\tx4535\tx5102\tx5669\tx6236\tx6803\ql\qnatural\pardirnatural

\f0\fs24 \cf0 Des dels or\'edgens del maquinari i el programari fins a l'\'e8poca actual, la complexitat dels sistemes de c\'e0lcul ha suposat un problema al com inform\'e0tics, enginyers i programadors han hagut d'enfrontar-se. Com a resultat d'aquest esfor\'e7 han sorgit i madurat importants \'e0rees d'investigaci\'f3. En aquesta tesi abordem algunes de les l\'ednies d'investigaci\'f3 actuals relacionada amb l'an\'e0lisi i la verificaci\'f3 de sistemes de computaci\'f3 complexos utilitzant m\'e8todes formals i llenguatges de domini espec\'edfic. Per a proporcionar models i eines per a l'an\'e0lisi i la verificaci\'f3 de sistemes de computaci\'f3 complexos utilitzem llenguatges de domini espec\'edfic. \
\
En aquesta tesi ens centrem en els sistemes distribu\'efts, amb un especial inter\'e8s pels sistemes Web i els sistemes biol\'f2gics. La primera part de la tesi est\'e0 dedicada a aspectes de seguretat i t\'e8cniques relacionades, concretament la certificaci\'f3 del programari. En primer lloc estudiem sistemes de control d'acc\'e9s a recursos i proposem un llenguatge per a especificar pol\'edtiques de control d'acc\'e9s que estan fortament associades a bases de coneixement i que proporcionen una descripci\'f3 sensible a la sem\'e0ntica dels recursos o elements als quals s'accedeix. Tamb\'e9 hem desenvolupat un marc nou de treball per a la Code-Carrying Theory, una metodologia per a la certificaci\'f3 del programari l'objectiu de la qual \'e9s assegurar l'enviament segur de codi en un entorn distribu\'eft. El nostre marc de treball est\'e0 basat en un sistema de transformaci\'f3 de teories de reescriptura mitjan\'e7ant operacions de plegat/desplegat. La segona part d'aquesta tesi es concentra en l'an\'e0lisi i la verificaci\'f3 de sistemes Web i sistemes biol\'f2gics. Proposem un llenguatge per al filtrat d'informaci\'f3 que permet la recuperaci\'f3 d'informacions en grans magatzems  de dades. Aquest llenguatge utilitza informaci\'f3 sem\'e0ntica obtinguda a partir d'ontologies remotes per a refinar el proc\'e9s de filtrat. Tamb\'e9 estudiem m\'e8todes de validaci\'f3 per a comprovar la consist\'e8ncia de continguts web pel que fa a propietats sint\'e0ctiques i sem\'e0ntiques. Una altra de les nostres contribucions \'e9s la proposta d'un llenguatge que permet definir i comprovar autom\'e0ticament restriccions sem\'e0ntiques i sint\'e0ctiques en el contingut est\'e0tic d'un sistema Web. Finalment, tamb\'e9 considerem els sistemes biol\'f2gics i ens centrem en un formalisme basat en l\'f2gica de reescriptura per al modelatge i l'an\'e0lisi d'aspectes quantitatius dels processos biol\'f2gics. \
\
Per a avaluar l'efectivitat de totes les metodologies proposades, hem prestat especial atenci\'f3 al desenvolupament de prototips que s'han implementat utilitzant llenguatges basats en regles.}