{"id":8881,"date":"1995-01-01T00:00:00","date_gmt":"1995-01-01T00:00:00","guid":{"rendered":"https:\/\/www.deberes.net\/tesis\/1995\/01\/01\/transformacion-y-verificacion-con-lotos\/"},"modified":"1995-01-01T00:00:00","modified_gmt":"1995-01-01T00:00:00","slug":"transformacion-y-verificacion-con-lotos","status":"publish","type":"post","link":"https:\/\/www.deberes.net\/tesis\/logica\/transformacion-y-verificacion-con-lotos\/","title":{"rendered":"Transformacion y verificacion con lotos"},"content":{"rendered":"<h2>Tesis doctoral de <strong> Jos\u00e9 Juan Pazos Arias <\/strong><\/h2>\n<p>El trabajo de la tesis es una contribucion al dise\u00f1o y desarrollo de sistemas con el lenguaje de especificacion formal lotos. Lotos facilita el dise\u00f1o de sistemas mediante refinamientos sucesivos: el sistema se construye de forma incremental como una secuencia de pasos dirigida a obtener un producto final que satisfaga los requisitos expresados inicialmente por el usuario o cliente.  el objetivo del trabajo de tesis se centro en el dise\u00f1o de una herramienta que diera soporte a este proceso de dise\u00f1o, es decir, automatizara todas las tareas rutinarias. En este proceso de dise\u00f1o es conveniente disponer de un mecanismo que permita asegurar que los efectos de un refinamiento son unicamente los deseados.  la logica temporal es un formalismo muy adecuado para la especificacion de las propiedades de un sistema. Dentro del trabajo de tesis, utilizamos la logica temporal para definir la semantica de programas lotos, obteniendo las siguientes ventajas:  * verificacion de propiedades de programas lotos. Este tipo de verificacion ofrece una buen mecanismo de guia del proceso de dise\u00f1o.  * sintesis de programas lotos a partir de la propiedad que queremos que satisfaga.  como resultado practico del trabajo realizado, se ha desarrollado un entorno que da soporte al desarrollo por refinamientos sucesivos de un sistema con lotos y que ofrece de forma integrada las facilidades de verificacion y de sintesis comentadas.<\/p>\n<p>&nbsp;<\/p>\n<h3>Datos acad\u00e9micos de la tesis doctoral \u00ab<strong>Transformacion y verificacion con lotos<\/strong>\u00ab<\/h3>\n<ul>\n<li><strong>T\u00edtulo de la tesis:<\/strong>\u00a0 Transformacion y verificacion con lotos <\/li>\n<li><strong>Autor:<\/strong>\u00a0 Jos\u00e9 Juan Pazos Arias <\/li>\n<li><strong>Universidad:<\/strong>\u00a0 Polit\u00e9cnica de Madrid<\/li>\n<li><strong>Fecha de lectura de la tesis:<\/strong>\u00a0 01\/01\/1995<\/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>Carlos Delgado Kloos<\/li>\n<\/ul>\n<\/li>\n<li><strong>Tribunal<\/strong>\n<ul>\n<li>Presidente del tribunal: Gonzalo Le\u00f3n Serrano <\/li>\n<li>Angel Velazquez Iturbe (vocal)<\/li>\n<li>Pere Botella L\u00f3pez (vocal)<\/li>\n<li> Santos Suarez Jos\u00e9 Manuel (vocal)<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Tesis doctoral de Jos\u00e9 Juan Pazos Arias El trabajo de la tesis es una contribucion al dise\u00f1o y desarrollo 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":[3747,3748,16008,30772],"tags":[30895,30894,16198,30893,15853,30590],"class_list":["post-8881","post","type-post","status-publish","format-standard","hentry","category-logica","category-logica-deductiva","category-politecnica-de-madrid","category-teoria-de-lenguajes-formales","tag-angel-velazquez-iturbe","tag-carlos-delgado-kloos","tag-gonzalo-leon-serrano","tag-jose-juan-pazos-arias","tag-pere-botella-lopez","tag-santos-suarez-jose-manuel"],"_links":{"self":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/8881","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=8881"}],"version-history":[{"count":0,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/8881\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/media?parent=8881"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/categories?post=8881"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/tags?post=8881"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}