Write a Blog >>
MODELS 2020
Fri 16 - Fri 23 October 2020
Thu 22 Oct 2020 15:00 - 15:20 at Room A - A5-Behavioural Modeling Chair(s): Massimo Tisi

The automated synthesis of behavioural models in the form of state machines (SMs) from higher-level specifications has a high potential impact on the efficiency and accuracy of software development using models. In this paper, inspired by program synthesis techniques, we propose a model synthesis approach that takes as input a structural model of a system and its desired system properties, and automatically synthesizes executable SMs for its components. To this end, we first generate a synthesis formula for each component, consistent with the system properties, and then perform a State Space Exploration (SSE) of each component, based on its synthesis formula. Each step of the SSE involves simply solving the synthesis formula in different contexts, based on input messages and the current execution state. The result of the SSE is saved in a Labeled Transition System (LTS), for which we then synthesize detailed actions for each of its transitions. Finally, we transform the LTSs into UML-RT (UML real-time profile) SMs, and integrate them with the original structural models. We assess the applicability, performance, and scalability of our approach using several different use cases extracted from the literature.

Conference Day
Thu 22 Oct

Displayed time zone: Eastern Time (US & Canada) change

15:00 - 16:15
A5-Behavioural ModelingTechnical Track at Room A
Chair(s): Massimo Tisi
15:00
20m
Full-paper
Synthesis of State Machine ModelsFT
Technical Track
Pre-print
15:20
20m
Full-paper
Efficient Reordering and Replay of Execution Traces of Distributed Reactive Systems in the Context of Model-driven DevelopmentFT
Technical Track
Majid BabaeiQueen's University, Mojtaba Bagherzadeh, Juergen DingelQueen's University, Kingston, Ontario
Pre-print
15:40
15m
Short-paper
Designing, Animating, and Verifying Partial UML ModelsNIV
Technical Track
Frédéric Jouault ERIS Team, ESEO , France, Valentin Besnard, Théo Le CalvarUniversity of Angers, Ciprian TeodorovENSTA Bretagne, Matthias Brun, Jérôme Delatour
Link to publication DOI Authorizer link Media Attached
15:55
15m
Talk
Mixed-semantics composition of statecharts for the component-based design of reactive systemsJ1st
Technical Track
Bence GraicsBudapest University of Technology and Economics, Vince MolnárBudapest University of Technology and Economics, András VörösBudapest University of Technology and Economics, Istvan MajzikBudapest University of Technology and Economics, Daniel VarroMcGill University / Budapest University of Technology and Economics
Link to publication DOI