UPPAAL es un entorno de herramientas integrado para el modelado , validación y verificación de sistemas en tiempo real modelados como redes de autómatas temporizados , extendidos con tipos de datos (enteros acotados, matrices, etc.).
Desarrollador (es) | Universidad de Uppsala Universidad de Aalborg |
---|---|
Versión inicial | 1995 |
Lanzamiento estable | 4.0.14 / 20 de mayo de 2014 |
Versión de vista previa | 4.1.22 / 28 de marzo de 2019 |
Escrito en | C ++ y GUI en Java |
Sistema operativo | Linux Mac OS X Microsoft Windows |
Disponible en | Inglés danés japonés chino lituano |
Tipo | Comprobación de modelo |
Licencia | Licencias comerciales Licencias académicas |
Sitio web | http://www.uppaal.org/ http://www.uppaal.com/ |
Se ha utilizado en al menos 17 casos de estudio 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 la Investigación Básica en Ciencias de la Computación en la Universidad de Aalborg , Dinamarca .
Están disponibles las siguientes extensiones:
- Cora para el análisis de accesibilidad óptima a los costos.
- Tron para pruebas de sistemas en tiempo real en línea (pruebas de conformidad de caja negra).
- Cobertura para generación de pruebas fuera de línea óptima para COBERTURA.
- Tiga para síntesis de controladores basada en TImed GAmes.
- Puerto para sistemas cronometrados basados en componentes, aprovechando técnicas de reducción de pedidos parciales.
- Pro para el análisis de accesibilidad PRObabilístico. (Interrumpido)
- SMC para la verificación de modelos estadísticos.
Referencias
enlaces externos
- Sitio web académico UPPAAL
- Web comercial UPPAAL
- Grupo de Diseño y Análisis de Sistemas en Tiempo Real
- Unidad DEIS, Departamento de Ciencias de la Computación en AAU