{"id":38570,"date":"1998-11-09T00:00:00","date_gmt":"1998-11-09T00:00:00","guid":{"rendered":"https:\/\/www.deberes.net\/tesis\/sin-categoria\/observadores-lineales-un-lenguaje-de-especificacion-de-propiedades-para-verificacion-de-protocolos\/"},"modified":"1998-11-09T00:00:00","modified_gmt":"1998-11-09T00:00:00","slug":"observadores-lineales-un-lenguaje-de-especificacion-de-propiedades-para-verificacion-de-protocolos","status":"publish","type":"post","link":"https:\/\/www.deberes.net\/tesis\/matematicas\/observadores-lineales-un-lenguaje-de-especificacion-de-propiedades-para-verificacion-de-protocolos\/","title":{"rendered":"Observadores lineales: un lenguaje de especificacion de propiedades para verificacion de protocolos."},"content":{"rendered":"<h2>Tesis doctoral de <strong> Pedro Merino Gomez <\/strong><\/h2>\n<p>La verificaci\u00f3n de protocolos es una actividad fundamental para localizar errores de dise\u00f1o y para garantizar que un sistema distribuido tenga el funcionamiento deseado. La automatizaci\u00f3n de esta tarea supone comparar una especificaci\u00f3n del comportamiento esperado frente a otra especificaci\u00f3n que se propone como un dise\u00f1o para el sistema. Aunque la verificaci\u00f3n autom\u00e1tica es una t\u00e9cnica relativamente reciente, existe ya una gran variedad de lenguajes para la descripci\u00f3n de estos dos componentes, as\u00ed como diversos criterios para decidir si el dise\u00f1o satisface la especificaci\u00f3n. En este trabajo se propone un nuevo lenguaje para describir el funcionamiento deseado de los protocolos.  este lenguaje de especificaci\u00f3n de propiedades, que se denomina observadores lineales, puede considerarse como una versi\u00f3n ejecutable de un fragmento de l\u00f3gica lineal. El nuevo formalismo permite especificar propiedades en las que es importante el n\u00famero de veces que ocurren los eventos, como pueden ser las propiedades que incluyen par\u00e1metros de calidad de servicio (cds), estrategias de planificaci\u00f3n o n\u00fameros de secuencia. Adem\u00e1s, el lenguaje incorpora mecanismos para especificar y analizar sistemas con configuraciones din\u00e1micas. su base l\u00f3gica facilita tanto su uso en un marco de programaci\u00f3n declarativa, como la aplicaci\u00f3n de t\u00e9cnicas propias de la l\u00f3gica lineal para el an\u00e1lisis y la transformaci\u00f3n de la propia especificaci\u00f3n de la propiedad.  el algoritmo de verificaci\u00f3n propuesto consiste en realizar el an\u00e1lisis al mismo tiempo que se genera el espacio de estados del protocolo, e incluye m\u00e9todos de optimizaci\u00f3n existentes para reducir las necesidades de memoria y tiempo. Como novedad se presenta un m\u00e9todo de poda del \u00e1rbol de estados, que se basa en t\u00e9cnicas de programaci\u00f3n entera para determinar si es posible o no satisfacer la propiedad en funci\u00f3n del an\u00e1lisis ya realizado.  para demostrar la utilidad p<\/p>\n<p>&nbsp;<\/p>\n<h3>Datos acad\u00e9micos de la tesis doctoral \u00ab<strong>Observadores lineales: un lenguaje de especificacion de propiedades para verificacion de protocolos.<\/strong>\u00ab<\/h3>\n<ul>\n<li><strong>T\u00edtulo de la tesis:<\/strong>\u00a0 Observadores lineales: un lenguaje de especificacion de propiedades para verificacion de protocolos. <\/li>\n<li><strong>Autor:<\/strong>\u00a0 Pedro Merino Gomez <\/li>\n<li><strong>Universidad:<\/strong>\u00a0 M\u00e1laga<\/li>\n<li><strong>Fecha de lectura de la tesis:<\/strong>\u00a0 11\/09\/1998<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n<h3>Direcci\u00f3n y tribunal<\/h3>\n<ul>\n<li><strong>Director de la tesis<\/strong>\n<ul>\n<li>Jos\u00e9 Mar\u00eda Troya Linero<\/li>\n<\/ul>\n<\/li>\n<li><strong>Tribunal<\/strong>\n<ul>\n<li>Presidente del tribunal: Carlos Delgado kloos <\/li>\n<li>\u00c1lvaro Suarez sarmiento (vocal)<\/li>\n<li>Juan  Jos\u00e9 Moreno navarro (vocal)<\/li>\n<li>arturo Azkorra salo\u00f1a (vocal)<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Tesis doctoral de Pedro Merino Gomez La verificaci\u00f3n de protocolos es una actividad fundamental para localizar errores de dise\u00f1o y [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"site-sidebar-layout":"default","site-content-layout":"","ast-site-content-layout":"","site-content-style":"default","site-sidebar-style":"default","ast-global-header-display":"","ast-banner-title-visibility":"","ast-main-header-display":"","ast-hfb-above-header-display":"","ast-hfb-below-header-display":"","ast-hfb-mobile-header-display":"","site-post-title":"","ast-breadcrumbs-content":"","ast-featured-img":"","footer-sml-layout":"","theme-transparent-header-meta":"","adv-header-id-meta":"","stick-header-meta":"","header-above-stick-meta":"","header-main-stick-meta":"","header-below-stick-meta":"","astra-migrate-meta-layouts":"default","ast-page-background-enabled":"default","ast-page-background-meta":{"desktop":{"background-color":"var(--ast-global-color-4)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"tablet":{"background-color":"","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"mobile":{"background-color":"","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""}},"ast-content-background-meta":{"desktop":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"tablet":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"mobile":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""}},"footnotes":""},"categories":[6313,1890,6474,3747,7834,126],"tags":[15946,100058,30894,4814,16231,32622],"class_list":["post-38570","post","type-post","status-publish","format-standard","hentry","category-aplicaciones-de-la-logica","category-ciencia-de-los-ordenadores","category-lenguajes-de-programacion","category-logica","category-malaga","category-matematicas","tag-alvaro-suarez-sarmiento","tag-arturo-azkorra-salona","tag-carlos-delgado-kloos","tag-jose-maria-troya-linero","tag-juan-jose-moreno-navarro","tag-pedro-merino-gomez"],"_links":{"self":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/38570","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/comments?post=38570"}],"version-history":[{"count":0,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/38570\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/media?parent=38570"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/categories?post=38570"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/tags?post=38570"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}