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 15
  • 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.
  • 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.