{"id":76235,"date":"2018-03-09T23:21:35","date_gmt":"2018-03-09T23:21:35","guid":{"rendered":"https:\/\/www.deberes.net\/tesis\/sin-categoria\/abstract-interpretation-techniques-for-the-verification-of-timed-systems\/"},"modified":"2018-03-09T23:21:35","modified_gmt":"2018-03-09T23:21:35","slug":"abstract-interpretation-techniques-for-the-verification-of-timed-systems","status":"publish","type":"post","link":"https:\/\/www.deberes.net\/tesis\/matematicas\/abstract-interpretation-techniques-for-the-verification-of-timed-systems\/","title":{"rendered":"Abstract interpretation techniques for the verification of timed systems"},"content":{"rendered":"<h2>Tesis doctoral de <strong> Robert Clariso Viladrosa <\/strong><\/h2>\n<p>En muchos sistemas, la correcci\u00f3n se puede decidir comparando las respuestas a eventos del entorno con las descritas en la especificaci\u00f3n. En otros dominios, la correcci\u00f3n no s\u00f3lo depende de qu\u00e9 respuestas se produzcan, sino tambi\u00e9n de cuando. La especificaci\u00f3n de estos sistemas, llamados sistemas temporizados, contiene informaci\u00f3n temporal como los retardos de las acciones internas y sucesos del entorno. Este concepto se puede generalizar en sistemas temporizados param\u00e9tricos, donde parte de la informaci\u00f3n temporal en la especificaci\u00f3n es un par\u00e1metro del sistema. Verificar un sistema con par\u00e1metros consiste en determinar el conjunto de valores aceptables para estos par\u00e1metros que garantizan un funcionamiento correcto. Sin embargo, muchas versiones de este problema de verificaci\u00f3n son computacionalmente costosas o incluso indecidibles.  una clase importante de sistemas temporizados son los circuitos temporizados, un estilo de dise\u00f1o orientado a construir circuitos de alta velocidad. un circuito temporizado consigue un buen rendimiento, pero su correcci\u00f3n s\u00f3lo esta garantizada si los retardos de sus puertas y cables satisfacen un conjunto de restricciones de tiempo. Por otro lado, los dise\u00f1adores de un circuito temporizado tienen alg\u00fan control sobre esos retardos. Formalizar el circuito c\u00f3mo un sistema temporizado param\u00e9trico permite retrasar la elecci\u00f3n de esos retardos hasta despu\u00e9s de verificar. Entonces, los retardos pueden seleccionarse acorde con las restricciones impuestas por la verificaci\u00f3n, evitando decisiones conservadores a priori. Una buena elecci\u00f3n de retardos puede mejorar la eficiencia de un circuito, p.Ej., Reduciendo su latencia.  esta tesis estudia la verificaci\u00f3n de sistemas temporizados param\u00e9tricos, con atenci\u00f3n especial al dominio de los circuitos temporizados. Los m\u00e9todos propuestos se basan en la teor\u00eda de interpretaci\u00f3n abstracta, un m\u00e9todo general para el an\u00e1lisis est\u00e1tico usad<\/p>\n<p>&nbsp;<\/p>\n<h3>Datos acad\u00e9micos de la tesis doctoral \u00ab<strong>Abstract interpretation techniques for the verification of timed systems<\/strong>\u00ab<\/h3>\n<ul>\n<li><strong>T\u00edtulo de la tesis:<\/strong>\u00a0 Abstract interpretation techniques for the verification of timed systems <\/li>\n<li><strong>Autor:<\/strong>\u00a0 Robert Clariso Viladrosa <\/li>\n<li><strong>Universidad:<\/strong>\u00a0 Polit\u00e9cnica de catalunya<\/li>\n<li><strong>Fecha de lectura de la tesis:<\/strong>\u00a0 19\/09\/2005<\/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>Jordi Cortadella Fortuny<\/li>\n<\/ul>\n<\/li>\n<li><strong>Tribunal<\/strong>\n<ul>\n<li>Presidente del tribunal: robert lukas mario Nieuwenhuis <\/li>\n<li>nicolas Halbwachs (vocal)<\/li>\n<li>enrique Pastor llorens (vocal)<\/li>\n<li>abelardo Pardo (vocal)<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Tesis doctoral de Robert Clariso Viladrosa En muchos sistemas, la correcci\u00f3n se puede decidir comparando las respuestas a eventos del [&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":[1890,332,15977,45251,13880,126,15596,8967,2535],"tags":[67834,164538,47502,164537,164536,6477],"class_list":["post-76235","post","type-post","status-publish","format-standard","hentry","category-ciencia-de-los-ordenadores","category-ciencias-tecnologicas","category-diseno-con-ayuda-de-ordenador","category-fiabilidad-de-los-ordenadores","category-informatica","category-matematicas","category-politecnica-de-catalunya","category-sistemas-en-tiempo-real","category-tecnologia-de-los-ordenadores","tag-abelardo-pardo","tag-enrique-pastor-llorens","tag-jordi-cortadella-fortuny","tag-nicolas-halbwachs","tag-robert-clariso-viladrosa","tag-robert-lukas-mario-nieuwenhuis"],"_links":{"self":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/76235","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=76235"}],"version-history":[{"count":0,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/76235\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/media?parent=76235"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/categories?post=76235"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/tags?post=76235"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}