Oberseminar
David Mosteller, University of Hamburg
February 26, 2021, 11:00, zoom: https://uni-hamburg.zoom.us/j/94889228942
Title: Model Checking of Synchronized Domain-Specific Multi-Formalism Models Using High-Level Petri Nets
Complex systems require the use of different models that are linked with
each other. Developers are naturally interested to show that their
systems work. Domain practitioners, who work with domain-specific
models, want to verify that their created models perform as desired.
Correctness statements about the behavior of models are only possible if
they have a clear semantics. Support is required for creating the
semantics and also for checking properties of the model.
With the Rmt approach, we make operational semantics usable for the
domain-specific modeling languages (DSML) that are understandable to
domain experts. High-level Petri nets as a target language of our
transformational approach can be analyzed by the MoMoC CTL model
checking tool. In this contribution MoMoC is extended and integrated
with the RMT approach so that the results of verification based on the
defined operational semantics can be applied to DSML.
The presented approach does not work equally well for all languages.
However, it is well suited for languages with discrete states that can
be uniquely named. Provided that they map well to Petri nets, questions
about (reachable) states of multiple linked domain-specific models can
be answered.