Centro de Altos Estudios en Tecnología Informática

Permanent URI for this community

https://repositorio.uai.edu.ar/handle/123456789/15

Browse

Browsing Centro de Altos Estudios en Tecnología Informática by Author "Asteasuain, Fernando"
  • 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
    Exploring specification pattern based behavioral synthesis with scenario clauses
    (Universidad Nacional del Centro de la Provincia de Buenos Aires, 2018-10) Asteasuain, Fernando ; Calonge, Federico ; Dubinsky, Manuel
    The Software Engineering community has identified behavioral specification as one of the main challenges to be addressed for the transference of formal verification techniques such as model checking. In particular, expressivity of the specification language is a key factor, especially when dealing with open systems and controllability of events. In this work we present an extension of the FVS language to denote behavior in open systems. By relying on an existing behavioral synthesis technique based on the specification patterns we show how FVS specification can be used as input to automatically build a controller from its specification.
  • Item
    Expressing early behavior specifications with branching visual scenarios
    (Edutecne, 2018-11) Asteasuain, Fernando ; Gamboa, Pablo Daniel ; Calonge, Federico ; D’Angiolo, Federico ; Díaz, Federico
    Branching logics enable the software engineer to express interesting type of properties and feature more efficient algorithms for model checking than linear logics. In this work we present an extension of the FVS language (based on a linear representation of systems' execution) in order to contemplate branching properties. The formal semantics of this extension, named Branching FVS, is also introduced in this work. As a case of study we model the behavior of a FLASH memory test chip, a classical hardware verification example. This is a particular domain where branching logics are heavily used to specify the expected behavior of systems.
  • 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
    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 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.