z-logo
open-access-imgOpen Access
Open and Branching Behavioral Synthesis with Scenario Clauses
Author(s) -
Fernando Asteasuain,
Federido Calonge,
Manuel Dubinsky,
Pablo Gamboa
Publication year - 2021
Publication title -
clei electronic journal
Language(s) - English
Resource type - Journals
ISSN - 0717-5000
DOI - 10.19153/cleiej.24.3.1
Subject(s) - computer science , branching (polymer chemistry) , controllability , flexibility (engineering) , programming language , expressive power , software engineering , artificial intelligence , theoretical computer science , mathematics , statistics , materials science , composite material
The 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 and branching time behavior reasoning. In this work, we propose the Feather Weight Visual Scenarios (FVS) language as an appealing declarative and formal verification 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 flexibility and expressive power of FVS, which constitute the crucial features that distinguish our approach.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.
Having issues? You can contact us here