Hispanopedia WikiTAPAAL es una herramienta para el modelado, simulación y verificación de redes de Petri de arco temporizado desarrollada en el Departamento de Ciencias de la Computación de la Universidad de Aalborg en Dinamarca y está disponible para las plataformas Linux, Windows y Mac OS X. [ 1 ]
La red de Petri de arcos temporizados (TAPN) es una extensión temporal del modelo clásico de red de Petri (un modelo gráfico de computación distribuida de uso común, introducido por Carl Adam Petri en su tesis doctoral en 1962). La extensión temporal considerada en TAPN permite un tratamiento explícito del tiempo real, que se asocia con los tokens de la red (cada token tiene su propia antigüedad). Los arcos que conectan lugares con transiciones se etiquetan mediante intervalos de tiempo que restringen la antigüedad de los tokens que pueden utilizarse para activar la transición correspondiente. En la herramienta TAPAAL se implementa una extensión adicional de este modelo con invariantes de antigüedad, arcos de transporte (que son más expresivos que, por ejemplo, los arcos de lectura considerados anteriormente) y arcos inhibidores.
La herramienta TAPAAL ofrece un editor gráfico para dibujar modelos TAPN, un simulador para experimentar con las redes diseñadas y un entorno de verificación que responde automáticamente a consultas lógicas formuladas en un subconjunto de la lógica CTL (esencialmente fórmulas EF, EG, AF, AG sin anidamiento). También permite al usuario comprobar si una red dada está k-acotada para un número k dado. TAPAAL está equipado con sus propios motores de verificación distribuidos junto con TAPAAL (uno para tiempo continuo [ 2 ] y otro para tiempo discreto [ 3 ] ). Opcionalmente, el usuario puede traducir automáticamente los modelos TAPAAL a UPPAAL y utilizar el motor de verificación de UPPAAL .
Enlaces externos
- Sitio web de TAPAAL, descarga
- Unidad DES, Departamento de Informática, Universidad de Aalborg, Dinamarca
- TAPAAL: editor, simulador y verificador de redes de Petri de arco cronometrado por J. Byg, KY Jørgensen y J. Srba, ATVA'09, Springer
- Una traducción eficiente de redes de Petri de arco temporizado a redes de autómatas temporizados por J. Byg, KY Jørgensen y J. Srba, ICFEM'09, Springer
- Un marco para relacionar sistemas de transición temporizada y preservar la verificación de modelos TCTL por L. Jacobsen, M. Jacobsen, MH Møller y J. Srba, EPEW'10, Springer
- Verificación de redes de Petri de arco temporizado por L. Jacobsen, M. Jacobsen, MH Møller y J. Srba, SOFSEM'11, Springer
Referencias
- ^ Alejandro David; Lasse Jacobsen; Morten Jacobsen; Kenneth Yrke Jorgensen; Mikael H. Møller; Jiří Srba (2012). "TAPAAL 2.0: entorno de desarrollo integrado para redes de Petri de arco temporizado". Herramientas y Algoritmos para la Construcción y Análisis de Sistemas . LNCS. vol. 7214. págs. 492– 497. doi : 10.1007/978-3-642-28756-5_36 . ISBN 978-3-642-28755-8.
- ^ Alexandre David; Lasse Jacobsen; Morten Jacobsen; Jiří Srba (2012). "Un algoritmo de alcanzabilidad hacia adelante para redes de Petri de arco temporizado acotado". Actas electrónicas en informática teórica . 102 : 141–155 . arXiv : 1211.6194 . doi : 10.4204/EPTCS.102.12 . S2CID 15499812 .
- ^ M. Andersen, H.G. Larsen, J. Srba, M.G. Sørensen, J.H. Taankvist (2012). "Verificación de propiedades de vivacidad en redes de Petri cerradas de arco temporizado". Métodos matemáticos y de ingeniería en ciencias de la computación . LNCS. Vol. 7721. pp. 69–81 . doi : 10.1007/978-3-642-36046-6_8 . ISBN 978-3-642-36044-2.
- Verificadores de modelos
- Métodos formales esbozos