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

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

  • 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
    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
    An expressive and enriched specification language to synthezise behavior in BIG DATA systems
    (Universidad Nacional de Salta, 2021) Asteasuain, Fernando ; Rodríguez Caldeira, Luciana
    In this work we extend our behavioral speci_cation and controller synthesis framework FVS to deal with BIG DATA requirements. For one side, we enriched FVS expressive power by exhibiting how our language can handle uents and partial speci_cations. For the other side, we combined FVS with a parallel model checker in order to automatically obtain a controller given the behavior speci_cation. In this way, FVS can be presented as an attractive tool to formally verify and synthesize behavior for BIG DATA systems. Our approach is compared to other well known parallel tool analyzing a complex big data system.
  • Item
    Controller synthesis for IoT protocols verification
    (Universidad Tecnológica Nacional, 2021-11) Asteasuain, Fernando
    Almost every modern device or artifact can now send and/or receive information and data. This hyper connected modern era is commonly denominated Internet of Things (IoT). Software Engineering tools and techniques must be adapted to manage the new challenges and requirements that the emergent paradigm of IoT imposes, especially regarding to communications, interactions and protocols between those artifacts. In this work we focus on a very well known formal technique called Controller Synthesis, which features interesting characteristics to formally verify IoT systems. In particular, we specified and synthesized the behavior of a key protocol for IoT, the MQQT protocol, employing the FVS formal verification framework.
  • Item
    Declarative specification and verification of modern software architecture patterns
    (Universidad Tecnológica Nacional. Facultad Regional San Francisco, 2021-3) Asteasuain, Fernando ; Machuca, Martín Miguel
    In this work we explore FVS as an Architectural Description Language (ADL) with the possibility to perform formal verification of architectural behavior. We modeled and specified a collection of architectural patterns including typical ones such as publish/subscribe or blackboard as well as some more modern ones in emergent technologies such as embedded software or cloud computing. Using a model checker tool we were able to formally verify architectural patterns in a concrete case of study: a server’s room monitoring system. The results show the potential of our work in the ADL’s domain.
  • Item
    Exploring parallel formal verification of BIG-DATA systems
    (Universidad de Palermo, 2021) Asteasuain, Fernando ; Rodríguez Caldeira, Luciana
    Software Engineering is trying to adapt its tools, mechanisms and techniques to cope with the challenges involved when developing BIG DATA software systems. In particular, formal verification in one of the areas that more urgently is required to step in. In this work we introduce two crucial aspects aiming to adapt FVS to cope with BIG Data requirements. For one side, FVS’s parallel algorithm is proved to be sound and correct. For the other side, we developed a compelling empirical validation of our approach, employing a communication protocol relevant in the industrial world within a context of parallel systems, introducing a load-balancer process and comparing several implementations.
  • 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
    Introducción a la verificación de programas
    (Universidad Abierta Interamericana. Facultad de Tecnología Informática, 2022-6) Rosenfeld, Ricardo Fabián
    Iniciamos una serie de cuatro artículos introductorios sobre la verificación axiomática de programas, en el marco de los programas imperativos de entrada/salida. En este artículo introducimos el método axiomático de verificación para los programas secuenciales determinísticos, y desarrollamos ejemplos de aplicación. Si bien la verificación de programas se expone como una actividad a posteriori (dados un programa y una especificación, verificar que el programa satisface la especificación), la idea que se sostiene en el artículo, y en toda la serie, es tener en cuenta los axiomas y reglas del método para programar al mismo tiempo que verificar, de modo tal de obtener programas correctos por construcción. Con esta perspectiva, al final se ejemplifica un desarrollo sistemático de programa basado en la axiomática presentada.
  • 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
    Open and branching behavioral synthesis with scenario clauses
    (Latin-american Center for Informatics Studies (CLEI), 2021-12-20) Asteasuain, Fernando ; Gamboa, Pablo Daniel ; Calonge, Federico ; Dubinsky, Manuel
    The Software Engineering community has identi_ed behavioral speci_cation as one of the main challenges to be addressed for the transference of formal veri_cation techniques such as model checking. In particular, expressivity of the speci_cation language is a key factor, especially when dealing with Open Systems and controllability of events and branching time behavior reasoning. In this work, we propose the Feather Weight Visual Scenarios (FVS) language as an appealing declarative and formal veri_cation tool to specify and synthesize the expected behavior of systems. FVS can express linear and branching properties in closed and Open systems. The validity of our approach is proved by employing FVS in complex, complete, and industrial relevant case studies, showing the exibility and expressive power of FVS, which constitute the crucial features that distinguish our approach.
  • 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
    Verificación de programas no determinísticos
    (Universidad Abierta Interamericana. Facultad de Tecnología Informática, 2022-12) Rosenfeld, Ricardo Fabián
    Continuando con nuestra serie de artículos introductorios sobre la verificación axiomática de programas, en este segundo trabajo nos enfocamos en el paradigma secuencial no determinístico, siempre en el marco de los programas imperativos de entrada/salida. Como el no determinismo se manifiesta en la concurrencia, el artículo sirve también como introducción a la verificación de programas concurrentes, en los que más se justifica por su complejidad un tratamiento formal de las pruebas de correctitud. Trabajamos con un clásico lenguaje de programación, con selección condicional y repetición no determinísticas, al que luego se incorporan asignaciones aleatorias. Para las pruebas de los programas planteamos una adaptación del método axiomático de verificación descripto en la publicación previa, limitado a la programación secuencial determinística. Presentamos ejemplos de aplicación del método e incluimos un desarrollo sistemático de programa, volviendo a destacar el approach de utilizar los axiomas y reglas para programar al mismo tiempo que verificar, con el objeto de obtener programas correctos por construcción. Finalmente introducimos el concepto de fairness, cuyo efecto es reducir el grado de no determinismo de un programa en base a determinados criterios de equidad en el entorno de ejecución, y describimos un par de adaptaciones en las reglas de prueba para contemplar este aspecto.
  • Item
    Verificación formal de software en sistemas de Big DATA
    (Universidad Champagnat, 2022) Asteasuain, Fernando ; Aragon, Rafael Esteban ; Rodriguez Caldeira, Luciana ; Granata, Nicolás Ezequiel ; Patera, Nahuel Hernán ; Gamboa, Pablo Daniel ; Han, Shaofeng
    La Ingeniería de Software debe evolucionar para poder enfrentar los desafíos de un mundo moderno híper conectado y con grandes volúmenes de información y datos disponibles para ser analizados. En este contexto, nuevas disciplinas como la denominada Ciencia de Datos han surgido recientemente. Para llevar adelante estos desafíos se deben contar con herramientas para la verificación formal de sistemas basados en BIG DATA que cuentan con una fuerte interacción con áreas de la Inteligencia Artificial como Aprendizaje Automático para poder mantener los estándares esperados de rigurosidad y calidad. Esta evolución requiere de novedosas técnicas para componer un sistema a través de sus múltiples aristas, junto con herramientas que sean eficaces pero también lo suficientemente flexibles y expresivas. La presente investigación pretende dar un paso en pos de enfrentar este desafío, combinando técnicas de verificación formal con la Inteligencia Artificial, en especial con la teoría de juegos, la síntesis de comportamiento y el aprendizaje automático.
  • Item
    Verification and behavioral synthesis of agent-based systems
    (Sociedad Argentina de Informática, SADIO, 2020-10) Asteasuain, Fernando ; Gamboa, Pablo Daniel ; D’Angiolo, Federico ; Dubinsky, Manuel
    In this work we explore the FVS language as a formalism to express, validate and synthesize behavior in the agent-based systems'world. Recent work relates Behavioral Synthesis with agent-based systems, opening the possibility for formalisms in the formal verification area to make an impact in the artificial intelligence domain. In this work we analyze FVS as a potential candidate to make a contribution given its desirable characteristics such as exibility, great expressive power and its ability to perform behavioral synthesis in Open Systems. A very well known case of study is analyzed: the Dining Cryptographers protocol, including one variation of the protocol. FVS was able to fully specify,validate and synthesize the behavior of the protocol.