PAT (Process Analysis Toolkit) es un marco autónomo [1] para componer, simular y razonar sistemas concurrentes en tiempo real y otros dominios posibles. Viene con interfaces fáciles de usar, editor de modelos destacado y simulador animado. Lo más importante es que PAT implementa varias técnicas de verificación de modelos que atienden diferentes propiedades, como la ausencia de bloqueo , la ausencia de divergencia , la accesibilidad, las propiedades LTL con supuestos de equidad , la verificación de refinamiento y la verificación del modelo probabilístico. Para lograr un buen rendimiento, se implementan técnicas avanzadas de optimización en PAT, por ejemplo , reducción parcial de pedidos ,reducción de simetría , abstracción de contador de proceso. [2] Hasta ahora, PAT tiene 1350 usuarios registrados de 302 organizaciones en 41 países y regiones.
Desarrollador (es) | Universidad Nacional de Singapur |
---|---|
Versión inicial | 2008 |
Lanzamiento estable | 3.5.1 / 13 de agosto de 2013 |
Escrito en | C# |
Sistema operativo | Microsoft Windows ; Linux , Unix , Mac OS X con Mono |
Plataforma | .Net 3.0 |
Disponible en | Inglés Chino (simplificado) Chino (tradicional) Japonés Alemán Vietnamita |
Tipo | Comprobación de modelo |
Sitio web | http://pat.comp.nus.edu.sg/ |
Referencias
- ^ Yang Liu, Jun Sun y Jin Song Dong. (2011), An Extensible Architecture for Building Multi-Domain Model Checker . ISSRE 2011
- ^ J. Sun, Y. Liu, A. Roychoudhury, S. Liu y JS Dong. (2009), Verificación de modelos justos con abstracción del contador de procesos . FM '09 Actas del 2º Congreso Mundial de Métodos Formales . doi : 10.1007 / 978-3-642-05089-3_9