Framework para el Desarrollo de Software mediante Modularización Avanzada. 2da. Etapa
Permanent URI for this collection
Browse
Browsing Framework para el Desarrollo de Software mediante Modularización Avanzada. 2da. Etapa by Subject "synthesis"
Results Per Page
Sort Options
-
ItemController synthesis for IoT protocols verification(Universidad Tecnológica Nacional, 2021-11) Asteasuain, FernandoAlmost 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.
-
ItemOpen 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, ManuelThe 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.