Centro de Altos Estudios en Tecnología Informática
Permanent URI for this community
Browse
Browsing Centro de Altos Estudios en Tecnología Informática by Author "Dubinsky, Manuel"
Results Per Page
Sort Options
-
ItemExploring specification pattern based behavioral synthesis with scenario clauses(Universidad Nacional del Centro de la Provincia de Buenos Aires, 2018-10) Asteasuain, Fernando ; Calonge, Federico ; Dubinsky, ManuelThe Software Engineering community has identified behavioral specification as one of the main challenges to be addressed for the transference of formal verification techniques such as model checking. In particular, expressivity of the specification language is a key factor, especially when dealing with open systems and controllability of events. In this work we present an extension of the FVS language to denote behavior in open systems. By relying on an existing behavioral synthesis technique based on the specification patterns we show how FVS specification can be used as input to automatically build a controller from its specification.
-
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.
-
ItemVerification and behavioral synthesis of agent-based systems(Sociedad Argentina de Informática, SADIO, 2020-10) Asteasuain, Fernando ; Gamboa, Pablo Daniel ; D’Angiolo, Federico ; Dubinsky, ManuelIn 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.