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 19
  • 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.
  • Item
    Verificación de Programas Paralelos
    (Universidad Abierta Interamericana. Facultad de Tecnología Informática, 2023-6-30) Rosenfeld, Ricardo Fabian
    En este tercer artículo de la serie que venimos presentando sobre la verificación axiomática de programas (en su variante de la Lógica de Hoare), tarea emprendida en el marco del proyecto del CAETI de construcción de un ambiente para asistir en el desarrollo de software, comenzamos a tratar el paradigma concurrente, para el que más se justifica el empleo de un método de prueba riguroso. Trabajamos con el modelo de los programas paralelos, programas concurrentes con procesos que comparten variables y se comunican a través de ellas (a pesar de la problemática común, por razones de espacio dejamos para el cuarto y último artículo el modelo de los programas distribuidos, programas concurrentes cuyos procesos son disjuntos y se comunican por medio de mensajes). Como en las publicaciones anteriores, remarcamos la idea de utilizar las axiomáticas descriptas como guías para obtener programas correctos por construcción. Destacamos además que las nociones fundamentales de la verificación axiomática observadas cuando analizamos los programas secuenciales, principalmente los predicados invariantes y las funciones variantes. se preservan en el contexto concurrente, a pesar de tener que considerarse una mayor variedad de clases de programas, propiedades y aspectos (metodológicos, semánticos, metateóricos).
  • Item
    A flexible and expressive formalism to specify metamorphic properties for BIG DATA systems validation
    (Universidad Nacional de La Rioja - EUDELAR, 2023-1) Asteasuain, Fernando
    BIG DATA systems represent a huge challenge for software engineering validations tasks since they have been classified as "non testable". Metamorphic Relationships (MR) have been proposed as a technique to overcome this problem. These relationships establish interactions between data that can be used to validate the expected behavior of the system. However, the process of exploring and defining MRs is a very arduous one, and an expressive and flexible specification language is needed to denote them. In this work we show how the Feather Weight Visual Scenarios (FVS) framework can be seen as an appealing tool to specify MRs. We exploit FVS features to model complex MR interactions and analysis, allowing the possibility to perform non trivial operations between MRs such as refinement and consistency checking. FVS is shown in action by introducing a proof of concept example focused on a machine learning system over biology cell images.