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 Subject "behavioral synthesis"
  • 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
    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.