Explorando verificación formal paralela para sistemas de BIG-DATA

• Autores: Fernando Asteasuain, Luciana Rodríguez
• Localización: Ciencia y tecnología, ISSN 1850-0870, ISSN-e 2344-9217, Nº. 21, 2021
• Idioma: español
• DOI: 10.18682/cyt.vi21.4549
• Títulos paralelos:
  • Exploring parallel formal verification of BIG-DATA systems
• Enlaces
  • Texto completo (pdf)
• Resumen
  • español

    La Ingeniería de Software viene adaptando sus herramientas, métodos y técnicas para enfrentar los desafíos de los denominados sistemas de BIG-DATA. En particular, el área de verificación formal ha sido señalada como unas de las áreas de las que se requiere inmediatas contribuciones. En este trabajo se presentan aspectos claves buscando adaptar al lenguaje FVS como un lenguaje de verificación formal para BIG DATA. Por un lado se presenta una demostración formal de la correctitud del esquema paralelo de FVS. Por otro, se presenta una desafiante validación empírica del enfoque propuesto utilizando un protocolo relevante a nivel industrial con un balanceador de carga y comparando varias implementaciones.

  • English

    Software Engineering is trying to adapt its tools, mechanisms and techniques to cope with the challenges involved when developing BIG DATA software systems.

    In particular, formal verification in one of the areas that more urgently is required to step in. In this work we introduce two crucial aspects aiming to adapt FVS to cope with BIG Data requirements. For one side, FVS’s parallel algorithm is proved to be sound and correct. For the other side, we developed a compelling empirical validation of our approach, employing a communication protocol relevant in the industrial world within a context of parallel systems, introducing a load-balancer process and comparing several implementations.

• Referencias bibliográficas
  • Asteasuain, F., & Braberman, V. (2017). Declaratively building behavior by means of scenario clauses. Requirements Engineering, 22(2),...
  • Asteasuain, F., & Rodriguez Caldeira L (2020). A Parallel Tableau Algorithm for BIG DATA Verification. CACIC 2020.
  • Bellettini, C., Camilli, M., Capra, L., & Monga, M. (2016). Distributed CTL model checking using MapReduce: theory and practice. Concurrency...
  • Boukala, M. C., & Petrucci, L. (2012). Distributed model-checking and counterexample search for CTL logic. International Journal of Critical...
  • Brassesco,M.V. 2017. Síntesis concurrente de controladores para juegos definidos con objetivos de generalized reactivity(1). Tesis de Licenciatura.,...
  • Brim, L., Yorav, K., & Žídková, J. (2005). Assumption-based distribution of CTL model checking. International Journal on Software Tools...
  • Camilli, M. (2014, May). Formal verification problems in a big data world: towards a mighty synergy. In Companion Proceedings of the 36th...
  • Clarke, E. M., Klieber, W., Nováček, M., & Zuliani, P. (2011, September). Model checking and the state explosion problem. In LASER Summer...
  • Ding, J., Zhang, D., & Hu, X. H. (2016, June). A framework for ensuring the quality of a big data service. In 2016 IEEE International...
  • Hummel, O., Eichelberger, H., Giloj, A., Werle, D., & Schmid, K. (2018, August). A collection of software engineering challenges for big...
  • Kumar, V. D., & Alencar, P. (2016, December). Software engineering for big data projects: Domains, methodologies and gaps. In 2016 IEEE...
  • Laigner, R., Kalinowski, M., Lifschitz, S., Monteiro, R. S., & de Oliveira, D. (2018, August). A systematic mapping of software engineering...
  • Otero, C. E., & Peter, A. (2014). Research directions for engineering big data analytics software. IEEE Intelligent Systems, 30(1), 13-19.
  • Segura, S., Fraser, G., Sanchez, A. B., & Ruiz-Cortés, A. (2016). A survey on metamorphic testing. IEEE Transactions on software engineering,...
  • Shafi, A., Carpenter, B., & Baker, M. (2009). Nested parallelism for multi-core HPC systems using Java. Journal of Parallel and Distributed...
  • Vardi, M. Y. (2001, April). Branching vs. linear time: Final showdown. In International conference on tools and algorithms for the construction...
  • Vega-Gisbert, O., Roman, J. E., & Squyres, J. M. (2016). Design and implementation of Java bindings in Open MPI. Parallel Computing, 59,...