Informes técnicos de investigación DSIC-MiST

Colección de documentos de trabajo, informes técnicos y otro material de investigación realizado por los investigadores del Departamento de Sistemas Informáticos y Computación (DSIC). Grupo: Tecnología Software Multiparadigma de la Universitat Politècnica de València en el desarrollo de sus investigaciones.

URI permanente para esta colecciónhttps://riunet.upv.es/handle/10251/8357

Examinar

Envíos recientes

Mostrando 1 - 1 de 1
  • Miniatura
    Item type: Informe , Access status: Abierto ,
    A Semantics to Generate the Context-sensitive Synchronized Control-Flow Graph (extended)
    (Universitat Politècnica de València, 2010-06-07) Tamarit Muñoz, Salvador; Silva, Josep; Llorens Agost, María Luisa; Oliver Villarroya, Javier; Escuela Técnica Superior de Ingeniería de Telecomunicación; Departamento de Sistemas Informáticos y Computación; Escuela Técnica Superior de Ingeniería Informática; Instituto Universitario Valenciano de Investigación en Inteligencia Artificial
    The CSP language allows the specification and verification of complex concurrent systems. Many analyses for CSP exist that have been successfully applied in different industrial projects. However, the cost of the analyses performed is usually very high, and sometimes prohibitive, due to the complexity imposed by the non-deterministic execution order of processes and to the restrictions imposed on this order by synchronizations. In this work, we define a data structure that allows us to statically simplify a specification before the analyses. This simplification can dras- tically reduce the time needed by many CSP analyses. We also introduce an algorithm able to automatically generate this data structure from a CSP specification. The algorithm has been proved correct and its implementation for the CSP's animator ProB is publicly available.