english Icono del idioma   español Icono del idioma  

Please use this identifier to cite or link to this item: https://hdl.handle.net/20.500.12008/2916 How to cite
Title: Especificación y análisis de sistemas de tiempo real en teoría de tipos. Caso de estudio : the railroad crossing example
Authors: Luna, Carlos
Obtained title: Magíster en Informática
University or service that grants the title: Universidad de la República (Uruguay). Facultad de Ingeniería. Instituto de Computación – PEDECIBA
Tutor: Cornes, Cristina
Echague, Juan
Type: Tesis de maestría
Keywords: ANALISIS DE SISTEMAS EN TIEMPO REAL, AUTOMATAS TEMPORIZADOS, TCTL, CTL, VERIFICACION DE MODELOS, TEORIA DE TIPOS, REAL TIME SYSTEMS, MODEL, TYPE THEORY
Issue Date: 2000
Abstract: Para el análisis de sistemas reactivos y de tiempo real dos importantes enfoques formales se destacan: la verificación de modelos, o model checking, y el análisis deductivo basado en asistentes de pruebas. El primero se caracteriza por la automaticidad pero presenta dificultades al tratar con sistemas que involucran un gran número de estados o donde se tienen parámetros variables, no acotados. El segundo permite tratar con sistemas que involucran un gran número de estados o donde se tienen parámetros variables, no acotados. El segundo permite tratar con sistemas arbitrarios pero requiere la interacción del usuario. Este trabajo explora una metodología de trabajo que permita compatibilizar el uso de un verificador de modelos como Kromos y el asistente de pruebas Coq en el análisis de sistemas de tiempo real. Para ello formalizamos grafos (autómatas) temporizados y la lógica TCTL (y CTL) en el cálculo de construcciones inductivas y co-inductivas de Coq, a fin de disponer de lenguajes de especificación y análisis comunes a ambas herramientas. Los grafos permiten describir los sistemas, mientras que la lógica se usa para especificar los requerimientos temporales. Una parte importante del trabajo está dedicada a estudiar cómo razonar deductivamente en Coq sobre esta clase de sistemas -la utilidad de tipos inductivos y la necesidad de tipos co-inductivos- asumiendo inicialmente un modelo de tiempo discreto. Un especial énfasis es puesto en el análisis de un caso de estudio, considerado como benchmark en diferentes trabajos: el control de un paso a nivel de tren ("the railroad corssing example"). Este problema es utilizado para evaluar y validar algunas de las formalizaciones propuestas.
Publisher: UR. FI-INCO,
Citation: LUNA, C. "Especificación y análisis de sistemas de tiempo real en teoría de tipos. Caso de estudio : the railroad crossing example". Tesis de maestría, Universidad de la República (Uruguay). Facultad de Ingeniería. Instituto de Computación – PEDECIBA, 2000.
License: Licencia Creative Commons Atribución – No Comercial – Sin Derivadas (CC BY-NC-ND 4.0)
Appears in Collections:Tesis de posgrado - Instituto de Computación

Files in This Item:
File Description SizeFormat  
tesis-cluna.pdf915,4 kBAdobe PDFView/Open


This item is licensed under a Creative Commons License Creative Commons