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 14
  • 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.
  • Item
    Formal Validation of Software for Nano Satellite Missions
    (Universidad Abierta Interamericana. Facultad de Tecnología Informática, 2023-6-30) Asteasuain, Fernando
    Space research industry has become one of the most successful domains in the last years. In particular, the development of nano satellites has emerged as a stunning field since its low costs of production. The software in charge of the satellite functioning must be carefully verified to check that system fulfills the expected behavior. In this work we provide a full, complete and declarative framework to formally validate software for nano satellite missions, including behavioral synthesis which is a distinguishable contribution in this field. When validating the satellite behavior we include requirements from different sources: on board computer, IoT protocols, operating system and mission properties. Our framework is based on the declarative and graphical language FVS (Feather Weight Visual Scenarios).
  • Item
    Formalizing operating systems for nano satellites on board computers
    (AJEA : Actas de Jornadas y Eventos Académicos de UTN, 2022-12-23) Asteasuain, Fernando
    In this work we provide a formal verification of the FreeRTOS operating system. Even most, a controller for the system is found. FreeRTOS is one of the most used operating systems for On Board Computers (OBC) in nano satellites such as CubeSats. Exploring, verifying and understating the potential and limitations of OBC operating systems is crucial for the growth of one of the most promising domains in the modern world: the space research industry. FreeRTOS’s formal verification is achieved employing the Feather Weight Visual Scenarios (FVS) framework, which has been previously applied to verify Internet of Things (IoT) protocols.
  • Item
    A parallel tableau algorithm for BIG DATA verification
    (Universidad Nacional de La Matanza, 2020-10) Asteasuain, Fernando ; Rodríguez Caldeira, Luciana
    BIG DATA systems are becoming more and more present in our everyday life generating data and information that needs to be explored and analyzed. In this sense, formal verification tools and techniques must provide solutions to face with these new challenges since they been pointed out as one of the most needed software engineering activities to consolidate BIG DATA modern systems. In this work we present a parallel implementation of a tableau algorithm aiming to improve the performance of our formal verication scheme. The pursued objective behind this transformation is to adapt our framework to deal with BIG DATA systems.
  • 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.