{"id":20891,"date":"2018-03-09T09:10:26","date_gmt":"2018-03-09T09:10:26","guid":{"rendered":"https:\/\/www.deberes.net\/tesis\/sin-categoria\/desde-especificaciones-logicas-de-intervalos-a-automatas-de-propiedad-una-construccion-tableau-para-su-aplicacion-en-comprobacion-de-modelos-on-the-fly\/"},"modified":"2018-03-09T09:10:26","modified_gmt":"2018-03-09T09:10:26","slug":"desde-especificaciones-logicas-de-intervalos-a-automatas-de-propiedad-una-construccion-tableau-para-su-aplicacion-en-comprobacion-de-modelos-on-the-fly","status":"publish","type":"post","link":"https:\/\/www.deberes.net\/tesis\/matematicas\/desde-especificaciones-logicas-de-intervalos-a-automatas-de-propiedad-una-construccion-tableau-para-su-aplicacion-en-comprobacion-de-modelos-on-the-fly\/","title":{"rendered":"Desde especificaciones l\u00f3gicas de intervalos a aut\u00f3matas de propiedad: una construcci\u00f3n tableau para su aplicaci\u00f3n en comprobaci\u00f3n de modelos on-the-fly"},"content":{"rendered":"<h2>Tesis doctoral de <strong>  Hornos Barranco Miguel Juan <\/strong><\/h2>\n<p>Este trabajo constituye el punto de partida para la verificaci\u00f3n autom\u00e1tica de sistemas mediante comprobaci\u00f3n de modelos on-the-fly, especificando los requisitos o propiedades temporales que el sistema debe cumplir con f\u00f3rmulas de una l\u00f3gica de intervalos, que nos permite razonar a nivel de intervalos de tiempo en lugar de instantes.  las l\u00f3gicas temporales de intervalos permiten especificar formalmente los requisitos o propiedades temporales de sistemas complejos, como son los sistemas reactivos, en general, y los concurrentes, en particular, en cuyo estudio y an\u00e1lisis se centra nuestro inter\u00e9s. La ventaja de este tipo de l\u00f3gicas, frente a las l\u00f3gicas temporales tradicionales, es que permiten establecer de forma sucinta el contexto temporal en el que ciertos requisitos deben aplicarse, haciendo posible una especificaci\u00f3n m\u00e1s concisa y comprensible de las propiedades a verificar, especialmente de aqu\u00e9llas m\u00e1s complejas.  uno de los objetivos actuales de la comunidad cient\u00edfica consiste en intentar que las t\u00e9cnicas de especificaci\u00f3n formal sean m\u00e1s f\u00e1ciles de entender para un grupo cada vez m\u00e1s amplio de personas que tienen responsabilidad en el proceso de desarrollo de software. Una posible manera de alcanzar dicho objetivo ser\u00eda adoptar un lenguaje de descripci\u00f3n basado en una l\u00f3gica temporal que soporte una representaci\u00f3n gr\u00e1fica sem\u00e1nticamente equivalente a las de sus f\u00f3rmulas textuales.  hemos adoptado la l\u00f3gica temporal de intervalos denomindada future interval logic (fil), ya que esta l\u00f3gica cuenta con una representaci\u00f3n gr\u00e1fica muy natural e intuitiva, que hace que las especificaciones sean m\u00e1s f\u00e1ciles de desarrollar y de comprender, incluso para aquellas personas involucradas en el desarrollo de software que no tengan una buena formaci\u00f3n matem\u00e1tico-l\u00f3gica.  por tanto, constituye la base sobre la que se pueden construir herramientas software amigables para el razonamiento formal acerca de las<\/p>\n<p>&nbsp;<\/p>\n<h3>Datos acad\u00e9micos de la tesis doctoral \u00ab<strong>Desde especificaciones l\u00f3gicas de intervalos a aut\u00f3matas de propiedad: una construcci\u00f3n tableau para su aplicaci\u00f3n en comprobaci\u00f3n de modelos on-the-fly<\/strong>\u00ab<\/h3>\n<ul>\n<li><strong>T\u00edtulo de la tesis:<\/strong>\u00a0 Desde especificaciones l\u00f3gicas de intervalos a aut\u00f3matas de propiedad: una construcci\u00f3n tableau para su aplicaci\u00f3n en comprobaci\u00f3n de modelos on-the-fly <\/li>\n<li><strong>Autor:<\/strong>\u00a0  Hornos Barranco Miguel Juan <\/li>\n<li><strong>Universidad:<\/strong>\u00a0 Granada<\/li>\n<li><strong>Fecha de lectura de la tesis:<\/strong>\u00a0 19\/12\/2002<\/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> Capel Tu\u00f1\u00f3n Manuel Isidoro<\/li>\n<\/ul>\n<\/li>\n<li><strong>Tribunal<\/strong>\n<ul>\n<li>Presidente del tribunal: Jos\u00e9 Mar\u00eda Troya linero <\/li>\n<li>Fernando Cuartero g\u00f3mez (vocal)<\/li>\n<li>Mar\u00eda Alpuente frasnedo (vocal)<\/li>\n<li>pedro Merino gomez (vocal)<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Tesis doctoral de Hornos Barranco Miguel Juan Este trabajo constituye el punto de partida para la verificaci\u00f3n autom\u00e1tica de sistemas [&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":[1890,18534,3747,3748,24723,126,6566,15624],"tags":[63341,5510,63340,4814,6479,32622],"class_list":["post-20891","post","type-post","status-publish","format-standard","hentry","category-ciencia-de-los-ordenadores","category-lenguajes-formales","category-logica","category-logica-deductiva","category-logica-modal","category-matematicas","category-sistemas-formales","category-software","tag-capel-tunon-manuel-isidoro","tag-fernando-cuartero-gomez","tag-hornos-barranco-miguel-juan","tag-jose-maria-troya-linero","tag-maria-alpuente-frasnedo","tag-pedro-merino-gomez"],"_links":{"self":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/20891","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=20891"}],"version-history":[{"count":0,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/20891\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/media?parent=20891"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/categories?post=20891"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/tags?post=20891"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}