Verificación de propiedades temporales en PPML
Product Process Modeling Languaje(PPML) es un lenguaje formal para modelar Procesos de Negocios que posee una semántica basada en sistemas de transición de estados temporizados. El lenguaje posee elementos que lo hacen apropiado para la especificación formal de procesos de negocios con restricciones...
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Objeto de conferencia |
| Lenguaje: | Español |
| Publicado: |
2008
|
| Materias: | |
| Acceso en línea: | http://sedici.unlp.edu.ar/handle/10915/21962 |
| Aporte de: |
| id |
I19-R120-10915-21962 |
|---|---|
| record_format |
dspace |
| institution |
Universidad Nacional de La Plata |
| institution_str |
I-19 |
| repository_str |
R-120 |
| collection |
SEDICI (UNLP) |
| language |
Español |
| topic |
Ciencias Informáticas Formal methods métodos formales autómatas temporizados Model checking procesos de negocios business processes |
| spellingShingle |
Ciencias Informáticas Formal methods métodos formales autómatas temporizados Model checking procesos de negocios business processes Regis, Germán Aguirre, Nazareno Matías Verificación de propiedades temporales en PPML |
| topic_facet |
Ciencias Informáticas Formal methods métodos formales autómatas temporizados Model checking procesos de negocios business processes |
| description |
Product Process Modeling Languaje(PPML) es un lenguaje formal para modelar Procesos de Negocios que posee una semántica basada en sistemas de transición de estados temporizados. El lenguaje posee elementos que lo hacen apropiado para la especificación formal de procesos de negocios con restricciones temporales, concurrencia, etc. Sin embargo, no existe actualmente ninguna herramienta de soporte al lenguaje; en particular, el lenguaje carece de herramientas de verificación de propiedades temporales asociadas a las especificaciones. En este trabajo proponemos, en primer lugar, una codificación de la semántica de PPML en autómatas temporizados, a través de una traducción de PPML al lenguaje UPPAAL. En segundo lugar, aprovechamos esta traducción, que ha sido automatizada en un prototipo, para realizar verificación de propiedades CTL (branching time) de especificaciones PPML, utilizando la herramienta asociada a UPPAAL. |
| format |
Objeto de conferencia Objeto de conferencia |
| author |
Regis, Germán Aguirre, Nazareno Matías |
| author_facet |
Regis, Germán Aguirre, Nazareno Matías |
| author_sort |
Regis, Germán |
| title |
Verificación de propiedades temporales en PPML |
| title_short |
Verificación de propiedades temporales en PPML |
| title_full |
Verificación de propiedades temporales en PPML |
| title_fullStr |
Verificación de propiedades temporales en PPML |
| title_full_unstemmed |
Verificación de propiedades temporales en PPML |
| title_sort |
verificación de propiedades temporales en ppml |
| publishDate |
2008 |
| url |
http://sedici.unlp.edu.ar/handle/10915/21962 |
| work_keys_str_mv |
AT regisgerman verificaciondepropiedadestemporalesenppml AT aguirrenazarenomatias verificaciondepropiedadestemporalesenppml |
| bdutipo_str |
Repositorios |
| _version_ |
1764820465216389124 |