Mixed-semantics composition of statecharts for the component-based design of reactive systems
- PDF / 3,557,592 Bytes
- 35 Pages / 595.276 x 790.866 pts Page_size
- 21 Downloads / 203 Views
THEME SECTION PAPER
Mixed-semantics composition of statecharts for the component-based design of reactive systems Bence Graics1,2
· Vince Molnár1,2 · András Vörös1,2 · István Majzik1 · Dániel Varró1,2,3
Received: 16 June 2019 / Revised: 5 May 2020 / Accepted: 7 May 2020 © The Author(s) 2020
Abstract The increasing complexity of reactive systems can be mitigated with the use of components and composition languages in model-driven engineering. Designing composition languages is a challenge itself as both practical applicability (support for different composition approaches in various application domains), and precise formal semantics (support for verification and code generation) have to be taken into account. In our Gamma Statechart Composition Framework, we designed and implemented a composition language for the synchronous, cascade synchronous and asynchronous composition of statechartbased reactive components. We formalized the semantics of this composition language that provides the basis for generating composition-related Java source code as well as mapping the composite system to a back-end model checker for formal verification and model-based test case generation. In this paper, we present the composition language with its formal semantics, putting special emphasis on design decisions related to the language and their effects on verifiability and applicability. Furthermore, we demonstrate the design and verification functionality of the composition framework by presenting case studies from the cyber-physical system domain. Keywords Component-based design · Statecharts · Composition language · Formal semantics · Formal verification
List of symbols
Communicated by Federico Ciccozzi, Antonio Cicchetti and Andreas Wortmann.
B
Bence Graics [email protected] Vince Molnár [email protected] András Vörös [email protected] István Majzik [email protected] Dániel Varró [email protected]
1
Deptartment of Measurement and Information Systems, Budapest University of Technology and Economics, Budapest, Hungary
2
MTA-BME Lendület Cyber-physical Systems Research Group, Budapest, Hungary
3
Department of Electrical and Computer Engineering, McGill University, Montreal, Canada
Tuples, sets and sequences (. . .) Tuple {. . .} Set |...| Size of set . . . Sequence The set of finite (possible repeating) sequences of A∗ the elements of the set A ε The empty sequence |s| The length of sequence s s[i] The ith element of sequence s σ (a) A permutation of set a All permutations of set a Sσ (a)
Indices and sizes i A generic index variable j A secondary generic index variable a Another value for variable a n A generic size variable k An index used for components K The number of components
123
B. Graics et al.
Temporal valuations a Next value of a The value of variable a in the ith step a (i) Component types − Definition of synchronous components (“singlethreaded”) −k The kth synchronous component s Definition of synchronous composites c Definition of cascade composites ? − ? as a synchronous com Definition
Data Loading...
