Framework para el Desarrollo de Software mediante Modularización Avanzada. 2da. Etapa
Permanent URI for this collection
Browse
Recent Submissions
1 - 5 of 10
-
ItemA flexible and expressive formalism to specify metamorphic properties for BIG DATA systems validation(Universidad Nacional de La Rioja - EUDELAR, 2023-1)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.
-
ItemVerificación formal de software en sistemas de Big DATA(Universidad Champagnat, 2022)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.
-
ItemIntroducción a la verificación de programas(Universidad Abierta Interamericana. Facultad de Tecnología Informática, 2022-6)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.
-
ItemVerificación de programas no determinísticos(Universidad Abierta Interamericana. Facultad de Tecnología Informática, 2022-12)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.
-
ItemDeclarative specification and verification of modern software architecture patterns(Universidad Tecnológica Nacional. Facultad Regional San Francisco, 2021-3)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.