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 Issue Date

Jump to a point in the index:
  • 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.
  • 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
    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
    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
    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
    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
    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.