Análisis de sistemas críticos en teoría de tipos

Para el análisis de sistemas reactivos y de tiempo real se destacan dos enfoques formales: la verificación de modelos y el análisis deductivo basado en asistentes de pruebas. El primero se caracteriza por ser completamente automatizable pero presenta dificultades al tratar sistemas con un gran númer...

Descripción completa

Guardado en:

Detalles Bibliográficos
Autor principal:	Luna, Carlos Daniel
Formato:	Objeto de conferencia
Lenguaje:	Español
Publicado:	2004
Materias:	Ciencias Informáticas ARTIFICIAL INTELLIGENCE Especificación y Análisis de Sistemas de Tiempo Real Intelligent agents Autómatas (Grafos) Temporizados Lógicas TCTL y CTL Verificación de Modelos Teoría de Tipos y Coq, Verificación-Demostración de Corrección
Acceso en línea:	http://sedici.unlp.edu.ar/handle/10915/22520
Aporte de:	SEDICI (UNLP) de Universidad Nacional de La Plata

id	I19-R120-10915-22520
record_format	dspace
institution	Universidad Nacional de La Plata
institution_str	I-19
repository_str	R-120
collection	SEDICI (UNLP)
language	Español
topic	Ciencias Informáticas ARTIFICIAL INTELLIGENCE Especificación y Análisis de Sistemas de Tiempo Real Intelligent agents Autómatas (Grafos) Temporizados Lógicas TCTL y CTL Verificación de Modelos Teoría de Tipos y Coq, Verificación-Demostración de Corrección
spellingShingle	Ciencias Informáticas ARTIFICIAL INTELLIGENCE Especificación y Análisis de Sistemas de Tiempo Real Intelligent agents Autómatas (Grafos) Temporizados Lógicas TCTL y CTL Verificación de Modelos Teoría de Tipos y Coq, Verificación-Demostración de Corrección Luna, Carlos Daniel Análisis de sistemas críticos en teoría de tipos
topic_facet	Ciencias Informáticas ARTIFICIAL INTELLIGENCE Especificación y Análisis de Sistemas de Tiempo Real Intelligent agents Autómatas (Grafos) Temporizados Lógicas TCTL y CTL Verificación de Modelos Teoría de Tipos y Coq, Verificación-Demostración de Corrección
description	Para el análisis de sistemas reactivos y de tiempo real se destacan dos enfoques formales: la verificación de modelos y el análisis deductivo basado en asistentes de pruebas. El primero se caracteriza por ser completamente automatizable pero presenta dificultades al tratar sistemas con un gran número de estados o que tienen parámetros no acotados. El segundo permite tratar con sistemas arbitrarios pero requiere la interacción del usuario. Este trabajo presenta formalizaciones en teoría de tipos de grafos temporizados para modelar sistemas reactivos y de tiempo real, y formalizaciones de las lógicas CTL y TCTL para razonar sobre estas clases de sistemas críticos. Asimismo, el artículo explora una metodología que permite compatibilizar el uso de un verificador de modelos como Kronos y el asistente de pruebas Coq en el análisis de sistemas reactivos y de tiempo real.
format	Objeto de conferencia Objeto de conferencia
author	Luna, Carlos Daniel
author_facet	Luna, Carlos Daniel
author_sort	Luna, Carlos Daniel
title	Análisis de sistemas críticos en teoría de tipos
title_short	Análisis de sistemas críticos en teoría de tipos
title_full	Análisis de sistemas críticos en teoría de tipos
title_fullStr	Análisis de sistemas críticos en teoría de tipos
title_full_unstemmed	Análisis de sistemas críticos en teoría de tipos
title_sort	análisis de sistemas críticos en teoría de tipos
publishDate	2004
url	http://sedici.unlp.edu.ar/handle/10915/22520
work_keys_str_mv	AT lunacarlosdaniel analisisdesistemascriticosenteoriadetipos
bdutipo_str	Repositorios
_version_	1764820465894817793

Análisis de sistemas críticos en teoría de tipos

Ejemplares similares