{"id":97197,"date":"2018-03-11T10:17:41","date_gmt":"2018-03-11T10:17:41","guid":{"rendered":"https:\/\/www.deberes.net\/tesis\/sin-categoria\/tecnicas-para-el-analisis-automatico-de-software-descrito-en-lenguajes-de-programacion\/"},"modified":"2018-03-11T10:17:41","modified_gmt":"2018-03-11T10:17:41","slug":"tecnicas-para-el-analisis-automatico-de-software-descrito-en-lenguajes-de-programacion","status":"publish","type":"post","link":"https:\/\/www.deberes.net\/tesis\/malaga\/tecnicas-para-el-analisis-automatico-de-software-descrito-en-lenguajes-de-programacion\/","title":{"rendered":"Tecnicas para el analisis automatico de software descrito en lenguajes de programacion"},"content":{"rendered":"<h2>Tesis doctoral de <strong> David Sanan Baena <\/strong><\/h2>\n<p>La verificaci\u00f3n de modelos o model checking es un m\u00e9todo formal que explora de forma exhaustiva el espacio de estados del modelo de un sistema, especificado en alguna t\u00e9cnica de descripci\u00f3n formal, para comprobar la correcci\u00f3n de \u00e9ste respecto a una serie de propiedades como puede ser an\u00e1lisis de alcanzabilidad, ausencia de interbloqueos, o verificaci\u00f3n de propiedades temporales. La verificaci\u00f3n de propiedades de un programa escrito en un lenguaje de programaci\u00f3n determinado requer\u00eda la creaci\u00f3n manual de un modelo, descrito en la t\u00e9cnica de descripci\u00f3n formal utilizada por la herramienta de an\u00e1lisis. De un tiempo a esta parte han surgido herramientas que realizan la verificaci\u00f3n del c\u00f3digo de forma autom\u00e1tica sin necesidad de realizar manualmente la obtenci\u00f3n del modelo. No obstante, la verificaci\u00f3n de sistemas de software directamente desde el c\u00f3digo fuente lleva consigo una serie de problemas como pueden ser la llamadas externas al lenguaje, la gesti\u00f3n de memoria din\u00e1mica o la verificaci\u00f3n de propiedades en las estructuras de datos presentes en el programa. En esta tesis detallamos una metodolog\u00eda para la verificaci\u00f3n autom\u00e1tica de sistemas descritos en lenguajes de programaci\u00f3n que hacen uso de apis bien definidos y de memoria din\u00e1mica. Dentro de la verificaci\u00f3n de funciones externas nuestra metodolog\u00eda se basa en proporcionar un formalismo del comportamiento de las funciones del api usado por el sistema. De esta forma, se puede verificar la correcci\u00f3n de \u00e9ste respecto a ese api bien definido. Respecto al uso de la memoria din\u00e1mica, en esta tesis proporcionamos un modelo de memoria basado en la divisi\u00f3n del espacio en dos \u00e1reas diferenciadas: el heap y el store global y una l\u00f3gica de dos niveles, temporal y espacial para la verificaci\u00f3n de propiedades sobre estructuras de datos din\u00e1micas. Adem\u00e1s, proporcionamos la implementaci\u00f3n de estas metodolog\u00eda en dos sistemas muy conocidos en el campo de la verificaci\u00f3n: spin y cadp.<\/p>\n<p>&nbsp;<\/p>\n<h3>Datos acad\u00e9micos de la tesis doctoral \u00ab<strong>Tecnicas para el analisis automatico de software descrito en lenguajes de programacion<\/strong>\u00ab<\/h3>\n<ul>\n<li><strong>T\u00edtulo de la tesis:<\/strong>\u00a0 Tecnicas para el analisis automatico de software descrito en lenguajes de programacion <\/li>\n<li><strong>Autor:<\/strong>\u00a0 David Sanan Baena <\/li>\n<li><strong>Universidad:<\/strong>\u00a0 M\u00e1laga<\/li>\n<li><strong>Fecha de lectura de la tesis:<\/strong>\u00a0 13\/11\/2009<\/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>Mar\u00eda  Del Mar Gallardo Melgarejo<\/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>stefania Gnesi (vocal)<\/li>\n<li>valentin Valero ruiz (vocal)<\/li>\n<li>Mar\u00eda Alpuente frasnedo (vocal)<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Tesis doctoral de David Sanan Baena La verificaci\u00f3n de modelos o model checking es un m\u00e9todo formal que explora de [&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":[13880,24723,7834],"tags":[199281,4814,6479,77041,199282,54644],"class_list":["post-97197","post","type-post","status-publish","format-standard","hentry","category-informatica","category-logica-modal","category-malaga","tag-david-sanan-baena","tag-jose-maria-troya-linero","tag-maria-alpuente-frasnedo","tag-maria-del-mar-gallardo-melgarejo","tag-stefania-gnesi","tag-valentin-valero-ruiz"],"_links":{"self":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/97197","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=97197"}],"version-history":[{"count":0,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/97197\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/media?parent=97197"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/categories?post=97197"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/tags?post=97197"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}