UPPAAL

UPPAAL es un entorno integrado de herramientas para el modelado, la validación y verificación de los sistemas de tiempo real modeladas como redes de autómatas cronometrada, extendido con tipos de datos (enteros delimitadas, matrices, etc.).
UPPAAL CORA es una rama de UPPAAL Costo óptima Accesibilidad Anslysis desarrollado por el equipo UPPAAL como parte de los proyectos de VHS y Ametist. Mientras UPPAAL apoya el modelo de cheques de los autómatas cronometrada, UPPAAL CORA utiliza una extensión de autómata temporizado llamada LPTA. LPTA le permite anotar el modelo con la noción de costo.
Este puede ser el costo de la demora en ciertas situaciones o el costo de acciones particulares. UPPAAL CORA luego encuentra rutas óptimas condiciones a juego de gol.
UPPAAL CORA se ha utilizado en una serie de estudios de caso. Algunos de ellos se describen en la página de estudio de caso de este sitio. Si usted viene con usos interesantes, por favor póngase en contacto con nosotros. Estamos interesados ​​en escuchar lo que haces!
Debido a las diferentes estructuras de datos internas, UPPAAL CORA actualmente consiste en dos versiones diferentes:
Una versión para el caso simplificado de análisis de la accesibilidad óptima tiempo.
Una versión para la lengua llena de LPTA.
Como UPPAAL, UPPAAL CORA es gratuito para uso sin fines de lucro, por ejemplo, para la evaluación, la investigación y la enseñanza.
Aquí están algunas características clave de "UPPAAL":
Robusto
 
· El lenguaje de modelado de UPPAAL CORA es robusto a cambios en el problema de modelado. Esto significa que su inversión en el modelado no se pierde cuando el problema cambia, ya que es fácil adaptar el modelo existente.
 
Rápido
 
· Aunque la tecnología es bastante nueva, experimental y muy diferente de las técnicas utilizadas en la investigación operativa tradicional, UPPAAL CORA es competitivo en una serie de estudios de caso.
 
Compatible
 
· El lenguaje de UPPAAL CORA es un superconjunto de UPPAAL. Cualquier modelo UPPAAL válida es también un modelo UPPAAL CORA válida. Esto hace que sea fácil y cómodo de reutilizar y adaptar sus modelos existentes para Uppaal CORA.
 
Corriente
 
· UPPAAL CORA se basa en la versión más reciente desarrollo interno de UPPAAL, que contiene las últimas mejoras de rendimiento y de lenguaje. Sin embargo, es una herramienta experimental y carece de muchas de las características de verificación de UPPAAL.
Limitaciones:
UPPAAL CORA con soporte completo LPTA tiene una serie de limitaciones. Estas limitaciones no son fundamentales, pero son el resultado de la utilización de las nuevas estructuras de datos internos con un conjunto de características actualmente limitado. Con el tiempo, se resolverán estas limitaciones.
- No extrapolación, por lo tanto, la terminación no se garantiza a no ser usted garantiza que:
· El sistema es acíclico.
· Todos los relojes están delimitadas por invariantes.
- Sólo accesibilidad simple:
· Sin verificación liveness
· Sin verificación de estancamiento
- Uso limitado de guía:
· Soporte para la clasificación (costo restante +) se implementa (mejor primera búsqueda)
· Apoyo a la variable de heurística es implementado, pero la expresión no puede hacer referencia a la variable costo.
¿Qué hay de nuevo en esta versión:
· Esta versión corrige errores de choque y una pérdida de memoria.