Nemzeti Tehetség Program - Nemzet Fiatal Tehetségeiért Ösztöndíj(NTP-NFTÖ-18)
Felsőoktatási Doktori Hallgatói, Doktorjelölti Kutatói Ösztöndíj(ÚNKP-19-3) Támogató:
ITM
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 statechart-based
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.
