Open and branching behavioral synthesis with scenario clauses

Thumbnail Image
Asteasuain, Fernando
Gamboa, Pablo Daniel
Calonge, Federico
Dubinsky, Manuel
Journal Title
Journal ISSN
Volume Title
Latin-american Center for Informatics Studies (CLEI)
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.
open systems, branching reasoning, behavioral specifications, synthesis
Asteasuain, F.; Calonge, F.; Dubinsky, M.; Gamboa, P.D. (2021). Open and branching behavioral synthesis with scenario clauses. En: CLEI Electronic Journal 24(3):1-20