{"id":94289,"date":"2018-03-11T10:13:56","date_gmt":"2018-03-11T10:13:56","guid":{"rendered":"https:\/\/www.deberes.net\/tesis\/sin-categoria\/tecnicas-de-verificacion-funcional-de-sistemas-digitales\/"},"modified":"2018-03-11T10:13:56","modified_gmt":"2018-03-11T10:13:56","slug":"tecnicas-de-verificacion-funcional-de-sistemas-digitales","status":"publish","type":"post","link":"https:\/\/www.deberes.net\/tesis\/campos-anillos-y-algebras\/tecnicas-de-verificacion-funcional-de-sistemas-digitales\/","title":{"rendered":"T\u00e9cnicas de verificaci\u00f3n funcional de sistemas digitales"},"content":{"rendered":"<h2>Tesis doctoral de <strong> I\u00f1igo Ugarte Olano <\/strong><\/h2>\n<p>En la tesis se desarrollan varias t\u00e9cnicas de verificaci\u00f3n de sistemas digitales a nivel funcional. Las t\u00e9cnicas parten de un modelo funcional que permite describir sistemas atemporales con tipos de datos y construcciones de control complejas. La metodolog\u00eda de modelado est\u00e1 basada en sistemas de inecuaciones de tipo polinomial.  la primera \u00e1rea de investigaci\u00f3n explora t\u00e9cnicas est\u00e1ticas de generaci\u00f3n de vectores de entrada en procesos de verificaci\u00f3n basados en aserciones. El objetivo de las t\u00e9cnicas desarrolladas es encontrar patrones de entrada que no cumplan las aserciones que modelan el funcionamiento del sistema o las restricciones de entrada\/salida.  la primera t\u00e9cnica desarrollada esta basada en an\u00e1lisis de intervalos modificado (modia) que mejora en eficiencia a las t\u00e9cnicas de an\u00e1lisis de intervalos tradicionales. La segunda t\u00e9cnica explora la utilizaci\u00f3n de herramientas de optimizaci\u00f3n no-lineal frente a t\u00e9cnicas que utilizan herramientas de optimizaci\u00f3n lineal. La principal ventaja es que trabajan en el dominio real (mayor rapidez de convergencia)  y permiten manejar operadores no lineales (multiplicaci\u00f3n) sin necesidad de aplicar transformaciones para convertirla en un conjunto de operadores lineales.  la segunda \u00e1rea de investigaci\u00f3n se centra en la verificaci\u00f3n basada en simulaci\u00f3n. La primera aportaci\u00f3n se centra en conocer la capacidad de detecci\u00f3n de fallos de las m\u00e9tricas tradicionales de cobertura (c\u00f3digo, saltos, bloque). Y la segunda, en mejorar el conjunto de vectores de prueba para la verificaci\u00f3n de sistemas complejos. la primera parte provee a las m\u00e9tricas de cobertura utilizadas en simulaci\u00f3n de un significado formal. El trabajo proporciona ecuaciones que permiten cuantificar la calidad de las m\u00e9tricas de cobertura de camino, de bloque y de sentencias. La principal conclusi\u00f3n es que dichas las m\u00e9tricas proporcionan una capacidad alta de detecci\u00f3n de errores si los rangos de entrada son suficientemente grandes. Con respecto a las sentencias de control, la principal conclusi\u00f3n es que la cobertura de errores de dicha m\u00e9trica es baja (aproximadamente un 50%). Otra conclusi\u00f3n es la evaluaci\u00f3n de la complejidad de la verificaci\u00f3n exhaustiva de sistemas descritos a nivel funcional. Esta complejidad depende del grado de los polinomios (complejidad de la descripci\u00f3n) y del n\u00famero de entradas, por lo que transformaciones que incrementan estos valores (por ejemplo, la conversi\u00f3n de entradas de tipo entero a un vector de bits) pueden tener un impacto negativo sobre la complejidad de la verificaci\u00f3n.  la segunda parte de esta \u00e1rea es la mejora de la generaci\u00f3n autom\u00e1tica de vectores para simulaciones aleatorias. Los puntos clave son, por un lado, aprovechar la informaci\u00f3n que se obtiene de la propia simulaci\u00f3n, y por otro lado, definir vectores capaces de ejecutar los dos caminos de las sentencias condicionales (100% de cobertura de saltos). en resumen, esta tesis ha abordado dos l\u00edneas de trabajo, definiendo 4 t\u00e9cnicas de verificaci\u00f3n semi-formal y dando lugar a 16 publicaciones en congresos internacionales y una revista.<\/p>\n<p>&nbsp;<\/p>\n<h3>Datos acad\u00e9micos de la tesis doctoral \u00ab<strong>T\u00e9cnicas de verificaci\u00f3n funcional de sistemas digitales<\/strong>\u00ab<\/h3>\n<ul>\n<li><strong>T\u00edtulo de la tesis:<\/strong>\u00a0 T\u00e9cnicas de verificaci\u00f3n funcional de sistemas digitales <\/li>\n<li><strong>Autor:<\/strong>\u00a0 I\u00f1igo Ugarte Olano <\/li>\n<li><strong>Universidad:<\/strong>\u00a0 Cantabria<\/li>\n<li><strong>Fecha de lectura de la tesis:<\/strong>\u00a0 22\/06\/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>Pablo Pedro Sanchez Espeso<\/li>\n<\/ul>\n<\/li>\n<li><strong>Tribunal<\/strong>\n<ul>\n<li>Presidente del tribunal: teresa Riesgo alcaide <\/li>\n<li>seraf\u00edn Olcoz yanguas (vocal)<\/li>\n<li>jordi Carrabina bordoll (vocal)<\/li>\n<li>Jos\u00e9 Luis Martin gonzalez (vocal)<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Tesis doctoral de I\u00f1igo Ugarte Olano En la tesis se desarrollan varias t\u00e9cnicas de verificaci\u00f3n de sistemas digitales a nivel [&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":[4335,10518,37728,10522,8166],"tags":[194404,16649,46304,194405,194406,43236],"class_list":["post-94289","post","type-post","status-publish","format-standard","hentry","category-campos-anillos-y-algebras","category-cantabria","category-diseno-microelectronico","category-polinomios","category-programacion-no-lineal","tag-inigo-ugarte-olano","tag-jordi-carrabina-bordoll","tag-jose-luis-martin-gonzalez","tag-pablo-pedro-sanchez-espeso","tag-serafin-olcoz-yanguas","tag-teresa-riesgo-alcaide"],"_links":{"self":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/94289","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=94289"}],"version-history":[{"count":0,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/94289\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/media?parent=94289"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/categories?post=94289"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/tags?post=94289"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}