{"id":82995,"date":"2018-03-10T00:07:03","date_gmt":"2018-03-10T00:07:03","guid":{"rendered":"https:\/\/www.deberes.net\/tesis\/sin-categoria\/diseno-y-verificacion-de-sistemas-distribuidos-mediante-la-aplicacion-combinada-de-metodos-formales\/"},"modified":"2018-03-10T00:07:03","modified_gmt":"2018-03-10T00:07:03","slug":"diseno-y-verificacion-de-sistemas-distribuidos-mediante-la-aplicacion-combinada-de-metodos-formales","status":"publish","type":"post","link":"https:\/\/www.deberes.net\/tesis\/logica\/diseno-y-verificacion-de-sistemas-distribuidos-mediante-la-aplicacion-combinada-de-metodos-formales\/","title":{"rendered":"Dise\u00f1o y verificacion de sistemas distribuidos mediante la aplicaci\u00f3n combinada de metodos formales"},"content":{"rendered":"<h2>Tesis doctoral de <strong> Alberto Gil Solla <\/strong><\/h2>\n<p>Esta tesis doctoral se centra en la aplicaci\u00f3n de las tecnicas formales al dise\u00f1o y verificacion de sistemas distribuidos, concretamente a la fase inicial de captura de los requisitos de usuario. El trabajo define un procedimiento metodologico para obtener la arquitectura inicial en forma de sistema de transiciones simbolico. Para ello, define la logica temporal ltcs y un algoritmo de model checking para la verificacion de las propiedades que se desea que cumpla el sistema. En caso de no cumplirse una propiedad, en la tesis se propone una variante de model checking con registros de informaci\u00f3n para identificar posibles modificaciones del sistema que deriven en el cumplimiento de la citada propiedad. El modelo resultante es automaticamente traducido a una especificacion elotos que sirve como punto de partida para un proceso de refinamientos.<\/p>\n<p>&nbsp;<\/p>\n<h3>Datos acad\u00e9micos de la tesis doctoral \u00ab<strong>Dise\u00f1o y verificacion de sistemas distribuidos mediante la aplicaci\u00f3n combinada de metodos formales<\/strong>\u00ab<\/h3>\n<ul>\n<li><strong>T\u00edtulo de la tesis:<\/strong>\u00a0 Dise\u00f1o y verificacion de sistemas distribuidos mediante la aplicaci\u00f3n combinada de metodos formales <\/li>\n<li><strong>Autor:<\/strong>\u00a0 Alberto Gil Solla <\/li>\n<li><strong>Universidad:<\/strong>\u00a0 Vigo<\/li>\n<li><strong>Fecha de lectura de la tesis:<\/strong>\u00a0 18\/01\/2000<\/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 Juan Pazos Arias<\/li>\n<\/ul>\n<\/li>\n<li><strong>Tribunal<\/strong>\n<ul>\n<li>Presidente del tribunal: Carlos Delgado kloos <\/li>\n<li>Luis Sanchez fernandez (vocal)<\/li>\n<li>pere Botella l\u00f3pez (vocal)<\/li>\n<li> Lopez garcia candido Antonio (vocal)<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Tesis doctoral de Alberto Gil Solla Esta tesis doctoral se centra en la aplicaci\u00f3n de las tecnicas formales al dise\u00f1o [&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":[3747,3748,30772,18657],"tags":[122380,30894,30893,30796,26736,15853],"class_list":["post-82995","post","type-post","status-publish","format-standard","hentry","category-logica","category-logica-deductiva","category-teoria-de-lenguajes-formales","category-vigo","tag-alberto-gil-solla","tag-carlos-delgado-kloos","tag-jose-juan-pazos-arias","tag-lopez-garcia-candido-antonio","tag-luis-sanchez-fernandez","tag-pere-botella-lopez"],"_links":{"self":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/82995","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=82995"}],"version-history":[{"count":0,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/82995\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/media?parent=82995"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/categories?post=82995"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/tags?post=82995"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}