{"id":55675,"date":"2018-03-09T22:43:23","date_gmt":"2018-03-09T22:43:23","guid":{"rendered":"https:\/\/www.deberes.net\/tesis\/sin-categoria\/from-sofware-architecture-to-formal-verification-of-a-distributed-system\/"},"modified":"2018-03-09T22:43:23","modified_gmt":"2018-03-09T22:43:23","slug":"from-sofware-architecture-to-formal-verification-of-a-distributed-system","status":"publish","type":"post","link":"https:\/\/www.deberes.net\/tesis\/teoria-de-la-programacion\/from-sofware-architecture-to-formal-verification-of-a-distributed-system\/","title":{"rendered":"From sofware architecture to formal verification of a distributed system"},"content":{"rendered":"<h2>Tesis doctoral de <strong>  Sanchez Penas Juan  Jose <\/strong><\/h2>\n<p>La tesis estudia como ir desde la arquitectura software a la verificaci\u00f3n formal de un sistema distribuido. Como motivaci\u00f3n y caso de estudio de la investigaci\u00f3n, usamos un servidor de video bajo demanda desarrollado por nuestro grupo de investigaci\u00f3n. La arquitectura software de dicho sistema es muy flexible y compleja, y mejores herramientas son necesarias para mejorar la calidad del sistema. La tesis estudia como usar m\u00e9todos formales para eso. Usando diversas herramientas del \u00e1rea, proponemos un m\u00e9todo innovador para extraer de forma autom\u00e1tica informaci\u00f3n sobre rendimiento. Como entrada, usamos el c\u00f3digo fuente y la configuraci\u00f3n del sistema, como salida, informaci\u00f3n sobre rendimiento y cuellos de botella. Se demuestra el m\u00e9todo con el servidor de video y se generaliza para otras herramientas y sistemas.<\/p>\n<p>&nbsp;<\/p>\n<h3>Datos acad\u00e9micos de la tesis doctoral \u00ab<strong>From sofware architecture to formal verification of a distributed system<\/strong>\u00ab<\/h3>\n<ul>\n<li><strong>T\u00edtulo de la tesis:<\/strong>\u00a0 From sofware architecture to formal verification of a distributed system <\/li>\n<li><strong>Autor:<\/strong>\u00a0  Sanchez Penas Juan  Jose <\/li>\n<li><strong>Universidad:<\/strong>\u00a0 A coru\u00f1a<\/li>\n<li><strong>Fecha de lectura de la tesis:<\/strong>\u00a0 24\/11\/2006<\/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>Thomas Arts<\/li>\n<\/ul>\n<\/li>\n<li><strong>Tribunal<\/strong>\n<ul>\n<li>Presidente del tribunal:  Freire nistal Jos\u00e9 Luis <\/li>\n<li>lars-ake Fredlund (vocal)<\/li>\n<li>john Demrick (vocal)<\/li>\n<li>ricardo Pe\u00f1a mari (vocal)<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Tesis doctoral de Sanchez Penas Juan Jose La tesis estudia como ir desde la arquitectura software a la verificaci\u00f3n formal [&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":[18576,13880,6474,6473,30772],"tags":[10525,123000,122999,16545,122997,122998],"class_list":["post-55675","post","type-post","status-publish","format-standard","hentry","category-a-coruna","category-informatica","category-lenguajes-de-programacion","category-teoria-de-la-programacion","category-teoria-de-lenguajes-formales","tag-freire-nistal-jose-luis","tag-john-demrick","tag-lars-ake-fredlund","tag-ricardo-pena-mari","tag-sanchez-penas-juan-jose","tag-thomas-arts"],"_links":{"self":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/55675","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=55675"}],"version-history":[{"count":0,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/55675\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/media?parent=55675"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/categories?post=55675"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/tags?post=55675"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}