Entorno de herramientas integrado
UPPAAL es un entorno de herramientas integrado para modelar , validar y verificar sistemas en tiempo real modelados como redes de autómatas temporizados , extendidos con tipos de datos (enteros acotados, matrices, etc.).
Se ha utilizado en al menos 17 estudios de caso desde su lanzamiento en 1995, incluso en Lego Mindstorms , para el protocolo de audio de Philips y en controladores de caja de cambios para Mecel . [1]
La 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 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 accesibilidad de costo óptimo.
- Tron para pruebas de sistemas en tiempo real ON-line (pruebas de conformidad de caja negra).
- Cobertura para generación de pruebas fuera de línea óptima para COVERerage.
- Tiga para síntesis de controlador basada en juegos temporizados.
- Puerto para sistemas temporizados basados en componentes, que explota técnicas de reducción de orden parcial.
- Pro para análisis de accesibilidad PRObabilístico. (Descontinuado)
- SMC para verificación de modelos estadísticos.
Referencias
Enlaces externos
- 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 Informáticas de la AAU
