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 17
  • 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.
  • Item
    Making Self-Adaptive Systems More Verifiable
    (edUTecNe, 2023-11) Asteasuain, Fernando
    Property Adaptation patterns were proposed as a technique to empower the application of formal verification mechanisms to detect and modify behavior in Self-Adaptive Systems. In this work the graphical and declarative language FVS (Feather weight Visual Scenarios) is proposed as a flexible and expressive formalism to specify all the adaption patterns. FVS distinguishable features allow performing the verification process in Self-Adaptive systems in a simple and straightforward manner. This work provides a full specification of the Adaptation patterns in FVS.
  • Item
    Verificación de Programas Distribuidos
    (Universidad Abierta Interamericana. Facultad de Tecnología Informática, 2023-12) Rosenfeld, Ricardo Fabian
    Este artículo completa nuestra serie de cuatro artículos sobre la verificación axiomática de programas, que planteamos en el marco del proyecto del CAETI para construir un ambiente de soporte al desarrollo de software. En particular, concluimos el análisis de los programas concurrentes iniciado en la publicación anterior, considerando ahora la familia de los programas distribuidos, caracterizados por contar con procesos con variables disjuntas y que se comunican mediante mensajes. Como siempre, destacamos el principio de utilizar las axiomáticas como guías para la obtención de programas correctos por construcción, y la observación de que las nociones fundamentales de predicado invariante y función variante constituyen la base metodológica en todos los paradigmas de programación.