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 Author "Dubinsky, Manuel"
  • 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
    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.