Verificación de extensiones de Redes de Petri con precios, tiempo y múltiples instancias

Las redes de Petri son un lenguaje formal muy adecuado para la modelizacíon, ańalisis y verificacíon de sistemas concurrentes con infinitos estados. En particular, son muy apropiadas para estudiar las propiedades de seguridad de dichos sistemas, dadas sus buenas propiedades de decidibilidad. Sin embargo, en muchas ocasiones las redes de Petri carecen de la expresividad necesaria para representar algunas caracteŕısticas fundamentales de los sistemas que se manejan hoy en d́ıa, como el manejo de tiempo real, costes reales, o la presencia de varios procesos con un ńumero no acotado de estados ejecut́andose en paralelo. En la literatura se han definido y estudiado algunas extensiones de las redes de Petri para la representaci ́on de las caracteŕısticas anteriores. Por ejemplo, las “Redes de Petri Temporizadas” [83, 10](TPN) incluyen el manejo de tiempo real y las ν-redes de Petri [78](ν-PN) son capaces de representar un ńumero no acotado de procesos con infinitos estados ejecut́andose concurrentemente. En esta tesis definimos varias extensiones que réunen estas dos caracteŕısticas y estudiamos sus propiedades de decidibilidad. En primer lugar definimos las “ν-Redes de Petri Temporizadas”, que réunen las caracteŕısticas expresivas de las TPN y las ν-PN. Este nuevo modelo es capaz de representar sistemas con un ńumero no acotado de procesos o instancias, donde cada proceso es representado por un nombre diferente, y tiene un ńumero no acotado de relojes reales. En este modelo un reloj de una instancia debe satisfacer ciertas condiciones (pertenecer a un intervalo dado) para formar parte en el disparo de una transicíon. Desafortunadamente, demostramos que la verificacíon de propiedades de seguridad es indecidible para este modelo...

Verificación de algoritmos y estructuras de datos en Dafny

La verificación formal de un programa es la demostración de que este funciona de acuerdo a una descripción del comportamiento esperado en toda posible ejecución. La especificación de lo deseado puede utilizar técnicas diversas y entrar en mayor o menor detalle, pero para ganarse el título de formal esta ha de ser matemáticamente rigurosa. El estudio y ejercicio manual de alguna de esas técnicas forma parte del currículo común a los estudios de grado de la Facultad de Informática y del itinerario de Ciencias de la Computación de la Facultad de Ciencias Matemáticas de la Universidad Complutense de Madrid, como es el caso de la verificación con pre- y postcondiciones o lógica de Hoare. En el presente trabajo se explora la automatización de estos métodos mediante el lenguaje y verificador Dafny, con el que se especifican y verifican algoritmos y estructuras de datos de diversa complejidad. Dafny es un lenguaje de programación diseñado para integrar la especificación y permitir la verificación automática de sus programas, con la ayuda del programador y de un demostrador de teoremas en la sombra. Dafny es un proyecto en desarrollo activo aunque suficientemente maduro, que genera programas ejecutables.

La participación social en la protección y gestión de los bienes agrarios inscritos en la lista del patrimonio mundial : ejemplos de buenas prácticas y estrategias de futuro

La participación de las personas y las comunidades que viven en lugares inscritos en la Lista del Patrimonio Mundial (o que se ven directamente afectadas por la inscripción) en la toma de decisiones respecto a su identificación, protección y gestión, es uno de los principales retos que debe afrontar la Convención de Patrimonio Mundial para alcanzar su anhelada credibilidad. Esta participación real y activa, exigible en todos los tipos de bienes culturales y naturales (independientemente de su categoría de protección), es especialmente necesaria en el caso de los pertenecientes al Patrimonio agrario. En primer lugar porque la gestión de los sitios y paisajes agrarios debe respetar las técnicas de manejo tradicionales y basarse en los derechos y conocimientos de las comunidades locales, imprescindibles para asegurar la supervivencia e integridad de sus valores tangibles e intangibles. Y en segundo lugar porque la continuidadv de estos espacios depende íntegramente de las actividades – y por lo tanto de las personas- que les han dado forma y sin las cuales se convertirían en lugares inertes y faltos de sustancia y autenticidad. Partiendo de estas premisas,este estudio analiza y compara los principios de la Carta de Baeza sobre el Patrimonio agrario y los planes de gestión de los bienes agrarios inscritos en la Lista del Patrimonio Mundial para identificar ejemplos de buenas prácticas en la materia y proponer estrategias que mejoren el reconocimiento y la participación de los agricultores, ganaderos y silvicultores en su protección, manejo y promoción.

Impacto de la inscripción de la ciudad maya de Palenque en la lista del patrimonio mundial de la Unesco.

La zona arqueológica de Palenque en Chiapas, México fue inscrita en la Lista del Patrimonio Mundial de la UNESCO en 1987. Desde entonces no se ha hecho una evaluación del impacto que ha tenido esta inscripción dentro de las comunidades circundantes al entorno protegido. El autor pretende abordar cuáles han sido los efectos que dicha inscripción entre la población local. Para ello se muestra el estado de la cuestión, su tendencia actual y las acciones que los diferentes agentes implicados están llevando a cabo para preservar el valor universal excepcional del sitio, su autenticidad e integridad. El tema es pertinente al cumplirse veinte años del levantamiento armado del Ejercito Zapatista de Liberación Nacional (EZLN) en el Estado de Chiapas. Este movimiento contribuyó al empoderamiento de las comunidades indígenas presentes en la zona arqueológica, las cuales han aprovechado este y otros sitios patrimoniales como un elemento para mejorar sus condiciones de vida. De este modo se produce una abierta confrontación a la autoridad del Instituto Nacional de Antropología e Historia (INAH), organismo del gobierno federal facultado para la gestión del sitio. Estudiar el caso de Palenque es por demás oportuno pues los gobiernos local, estatal y federal han comenzado a invertir en infraestructuras tendientes a incrementar los ingresos generados por el turismo. En los respectivos planes de ejecución se destaca el rol de la zona arqueológica como el atractivo principal y el detonador del desarrollo económico de la región. Tengamos en cuenta que esta ha sido una zona históricamente marcada por la pobreza, la marginación y la exclusión social, problemas a los que recientemente se han agregado la inseguridad pública, la migración ilegal y el deterioro ambiental.

Análisis de terminación para una plataforma de verificación de programas

De entre una serie de métodos estudiados acerca de la terminación de algoritmos, tales como Size-Change Termination o Isabelle, elegimos el método de RANK como instrumento para desarrollar nuestro propio programa de detección de terminación sobre el lenguaje de la IR. Esta decisión se basa en el coste polinómico de este método (frente a costes en PSPACE como el Size-Change Termination)y la posibilidad de obtener una herramienta asociada al mismo que además nos da la posibilidad de conocer un tiempo de ejecución aproximado. La herramienta asociada a RANK es compleja y va de la mano de una segunda herramienta (ASPIC). Hemos estudiado varios ejemplos, tales como el Mergesort o el Quicksort, para explicar la utilización de estas dos herramientas y a su vez ponernos en situación de los diferentes problemas que nos podemos encontrar a la hora de estudiar un programa. Partiendo del proceso que hemos usado para construir los automátas de los ejemplos anteriores, hemos diseñado e implementado en Java un algoritmo para transformar programas en el lenguaje de la IR al formato de entrada de RANK. Los resultados han sido satisfactorios, puesto que con los autómatas generados somos capaces de detectar de forma automatizada la terminación de, entre otros, los algoritmos recursivos antes mencionados.

Problemática de la verificación del principio de empresa en funcionamiento en la auditoria externa

La aplicación del principio de empresa en funcionamiento es un tema que inspira mucho respeto y su evaluación supone una gran responsabilidad por parte del auditor externo pues conlleva un alto grado de dificultad el poder medir, valorar y opinar sobre el negocio en marcha de la empresa analizada. Por otro lado, el entorno de escepticismo creado hacia la profesión auditora, debido a los escándalos financieros y a las crisis empresariales surgidas en los últimos años ha generado una serie de inquietudes que derivan en dos cuestiones: • ¿Las normas de auditoría contienen suficientes herramientas para medir las situaciones de insolvencia? • ¿Pueden ser útiles las herramientas de predicción de insolvencia para evaluar el principio de empresas en funcionamiento? La búsqueda de respuestas a estas preguntas, nos ha motivado a profundizar en el estudio del marco normativo existente que es el que aplica el profesional de la auditoría. Por ese motivo el objeto del presente trabajo de investigación es analizar el grado de calidad en la aplicación del principio de empresa en funcionamiento por parte del auditor externo en España en el actual contexto de crisis económica, e intentar evaluar si el uso de herramientas como los predictores de insolvencia podrían ayudar al auditor reforzando las evidencias...