{"id":23112,"date":"2018-03-09T09:13:33","date_gmt":"2018-03-09T09:13:33","guid":{"rendered":"https:\/\/www.deberes.net\/tesis\/sin-categoria\/model-checking-of-the-concurrent-constraint-paradigm\/"},"modified":"2018-03-09T09:13:33","modified_gmt":"2018-03-09T09:13:33","slug":"model-checking-of-the-concurrent-constraint-paradigm","status":"publish","type":"post","link":"https:\/\/www.deberes.net\/tesis\/politecnica-de-valencia\/model-checking-of-the-concurrent-constraint-paradigm\/","title":{"rendered":"Model checking of the concurrent constraint paradigm"},"content":{"rendered":"<h2>Tesis doctoral de <strong> Alicia Villanueva Garc\u00eda <\/strong><\/h2>\n<p>En muchas aplicaciones reales la verificaci\u00f3n formal de propiedades temporales es imprescindible. En la bibliograf\u00eda podemos encontrar muchos casos de estudio en los que parec\u00edan c\u00f3mo las t\u00e9cnicas de verificaci\u00f3n formal han permitido detectar errores en sistemas que parec\u00edan correctos.  el model cheching es una t\u00e9cnica de verificaci\u00f3n auton\u00f3mica que, dado un modelo del sistema y una f\u00f3rmula temporal, comprueba si el modelo satisface la f\u00f3rmula. El problema principal del model checking es la explosi\u00f3n de estados.  en esta tesis se usa el paradigma concurrent constraint (cc) para especificar sistemas reactivos y sistemas h\u00edbridos. Se consideran tres lenguajes temporales que han sido definidos a partir del paradigma cc: el lenguaje tcc, el lenguaje tccp y el lenguaje hcc. Los dos primeros pueden modelar sistemas reactivos gracias a que han definidos sobre una noci\u00f3n de tiempo discreto, mientras que el tercer lenguaje es capaz de modelar sistemas h\u00edbridos ya que usa una noci\u00f3n de tiempo continuo.  sabemos que una adecuada sem\u00e1ntica denotacional permite realizar an\u00e1lisis muy interesantes de lenguajes. Cuando fue introducido el lenguaje tcc se defini\u00f3 su sem\u00e1ntica operacional y su sem\u00e1ntica denotacional, sin embargo estas dos sem\u00e1ntcias a veces no coinciden. En esta tesis se ha definido una sem\u00e1tncia denotacional fully abstract (con respecto a la sem\u00e1ntica operacional) para el modelo de programaci\u00f3n tcc. Adem\u00e1s mostramos un ejemplo de c\u00f3mo se puede usar esta nueva sem\u00e1ntica denotacional para analizar la expresividad del operador de tcc que modela los conceptos de timeout y preemption. Se ha demostrado que la introducci\u00f3n de dicho constructor hace el lenguaje tcc m\u00e1s potente que el paradigma cc.  el resultado m\u00e1s importante de esta tesis es la definici\u00f3n de un algoritmo de model checking para el lenguaje tccp. La idea es la de explortar las caracter\u00edsticas del paradigma cc para resolver (en parte) el problema<\/p>\n<p>&nbsp;<\/p>\n<h3>Datos acad\u00e9micos de la tesis doctoral \u00ab<strong>Model checking of the concurrent constraint paradigm<\/strong>\u00ab<\/h3>\n<ul>\n<li><strong>T\u00edtulo de la tesis:<\/strong>\u00a0 Model checking of the concurrent constraint paradigm <\/li>\n<li><strong>Autor:<\/strong>\u00a0 Alicia Villanueva Garc\u00eda <\/li>\n<li><strong>Universidad:<\/strong>\u00a0 Polit\u00e9cnica de Valencia<\/li>\n<li><strong>Fecha de lectura de la tesis:<\/strong>\u00a0 24\/05\/2003<\/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>Mar\u00eda Alpuente Frasnedo<\/li>\n<\/ul>\n<\/li>\n<li><strong>Tribunal<\/strong>\n<ul>\n<li>Presidente del tribunal: furio Honsell <\/li>\n<li>marco Cadoli (vocal)<\/li>\n<li>claude Kirchner (vocal)<\/li>\n<li>jacques Jaray (vocal)<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Tesis doctoral de Alicia Villanueva Garc\u00eda En muchas aplicaciones reales la verificaci\u00f3n formal de propiedades temporales es imprescindible. En la [&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":[16820],"tags":[68704,68707,68705,68708,68706,6479],"class_list":["post-23112","post","type-post","status-publish","format-standard","hentry","category-politecnica-de-valencia","tag-alicia-villanueva-garcia","tag-claude-kirchner","tag-furio-honsell","tag-jacques-jaray","tag-marco-cadoli","tag-maria-alpuente-frasnedo"],"_links":{"self":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/23112","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=23112"}],"version-history":[{"count":0,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/23112\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/media?parent=23112"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/categories?post=23112"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/tags?post=23112"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}