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...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Regis, Germán, Aguirre, Nazareno Matías
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