Comprobador de modelos Uppaal

UPPAAL es un entorno de herramientas integrado para el modelado , la validación y la verificación de sistemas en tiempo real modelados como redes de autómatas temporizados , ampliados con tipos de datos (enteros acotados, matrices, etc.).

Se ha utilizado en al menos 17 estudios de caso desde su lanzamiento en 1995, incluyendo en Lego Mindstorms , para el protocolo de audio de Philips y en controladores de cajas de engranajes para Mecel . ^{[ 1 ]}

Esta herramienta ha sido desarrollada en colaboración entre el grupo de Diseño y Análisis de Sistemas en Tiempo Real de la Universidad de Uppsala , Suecia , y el grupo de Investigación Básica en Ciencias de la Computación de la Universidad de Aalborg , Dinamarca .

Están disponibles las siguientes extensiones:

• Cora para el análisis de alcanzabilidad óptima en términos de costo.
• Tron para probar sistemas en tiempo real en línea (pruebas de conformidad de caja negra).
• Portada archivada el 17/01/2021 en Wayback Machine para la generación de pruebas fuera de línea con cobertura óptima.
• Síntesis de controladores basada en Tiga para juegos con tiempo limitado.
• Puerto para sistemas temporizados basados ​​en componentes, que aprovecha las técnicas de reducción de orden parcial.
• Pro para análisis de alcanzabilidad probabilística. (Descontinuado)
• SMC para la verificación de modelos estadísticos.

• Sitio web académico de UPPAAL
• Sitio web comercial de UPPAAL
• Grupo de Diseño y Análisis de Sistemas en Tiempo Real
• Unidad DEIS, Departamento de Ciencias de la Computación en AAU