Framework para el Desarrollo de Software mediante Modularización Avanzada. 2da. Etapa

Permanent URI for this collection

https://repositorio.uai.edu.ar/handle/123456789/295

Browse

Recent Submissions

Now showing 1 - 5 of 21
  • Item
    Notas sobre complejidad computacional
    (Universidad Abierta Interamericana. Facultad de Tecnología Informática, 2024-12) Rosenfeld, Ricardo Fabian
    Dos aspectos centrales del proyecto en curso del CAETI, de creacion de un ambiente de desarrollo de software basado en conceptos avanzados de modularizacion y sintesis de comportamiento, son la correctitud y la eficiencia. En relación al primer aspecto, en artículos anteriores describimos la verificación axiomática de programas. En este artículo nos enfocamos en la eficiencia, presentando una serie de notas que cubren sucintamente temas relevantes de la complejidad computacional, área de la teoría de la computación que estudia la dificultad inherente de los problemas. Se tratan los paradigmas determinístico, probabilístico y cuántico, incluyendo elementos vinculados con la criptografía, las pruebas y la desaleatorización de los algoritmos. El material integra los contenidos de la asignatura Métodos Formales en la Ingeniería de Software, que se dicta en el Doctorado en Informática de la Facultad de Tecnología Informática de la UAI.
  • Item
    A Sound and Correct Formalism to Specify, Verify and Synthesize Behavior in BIG DATA Systems
    (Springer, 2022-5-20) Asteasuain, Fernando ; Rodriguez Caldeira, Luciana
    In this work we consolidate our behavioral specification frame work based on the Feather Weight Visual Scenarios (FVS) language as a powerful tool to specify, verify and synthesize behavior for BIG DATA systems. We formally demonstrate that our approach is sound and cor rect end to end, including the latest extensions such as fluents and par tial specifications. In addition, our empirical validation is strengthen by adding new and complex case studies and incorporating, besides execu tion time, space exploration as a factor in the comparison with other approaches. We believe that the contributions introduced in this work aim to point up FVS as a solid tool to formally verify behavior in BIG DATA systems.
  • Item
    Formally Verifying Data Science Systems with a Sound and Correct Formalism
    (Springer, 2024-6-23) Asteasuain, Fernando
    The state explosion problem arises as one of the most problematic issues to be faced against when trying to formally validate Data Science Software Systems. This challenge imposes the synergy and combination of tools. Taking this into consideration in this work we present a robust theoretical feature of our behavioral framework VG-FVS: we formally prove that our approach relies on a sound, complete and correct formalism. VG-FVS is a brand new new version of our framework FVS (Feather weight Visual Scenarios), which is specially developed to address the state explosion problem by integrating FVS with MaRDiGraS, a generic library which eases the state space exploration using a MAP-REDUCE software architecture.
  • Item
    New Horizons for Metamorphic Relationships in Formal Verification
    (Springer, 2023-5-27) Asteasuain, Fernando
    In this work we broadened the impact of the so called Metamorphic relationships (MR’s) in the formal verification phase. We showed the potential of our behavioral framework called FVS (Feather Weight Visual Scenarios) to successfully denote metamorphic properties in diverse, complex and meaningful domains such as UAV’s flying missions and operating systems for On Board Computers (OBC) for nano satellites. We employed MR’s to validate behavior in a BIG-DATA context, where possible a large amount of data and information seen as traces must be verified but also a novel way to relate different goals and UAV’s configurations in the context of the dynamic adaption of AUV’s missions due to changes in the requirements. In addition, we explored complementary behavior as a possible source for obtaining MR’s.
  • Item
    Addressing the State Explosion Problem for Big Data Systems Formal Verication
    (Universidad Nacional de Luján, 2023-10-12) Asteasuain, Fernando
    The formal verification of BIG DATA systems remains as a challenging task to be addressed since a very large and complex state space describing the behavior of the system must be explored and verified. In particular, the state explosion problem arises as one of the most problematic issues to be faced against. Some approaches have leveraged on some architectural patterns used in BIG DATA system development, especially those focused on the MAP-REDUCE architecture. Taking this into consideration in this work we present VG-FVS, a new version of our framework FVS (Feather weight Visual Scenarios), which is specially developed to address the state explosion problem. This is achieved by integrating FVS with MaRDiGraS, a generic library which eases the state space exploration using a MAP-REDUCE software architecture. Empirical validation analyzing BIG DATA systems was carried on, showing promising results for our approach.