Publication
Title
A framework for temporal verification support in domain-specific modelling
Author
Abstract
In Domain-Specific Modelling (DSM) the general goal is to provide Domain-Specific Modelling Languages (DSMLs) for domain users to model systems using concepts and notations they are familiar with, in their problem domain. Verifying whether a model satisfies a set of requirements is considered to be an important challenge in DSM, but is nevertheless mostly neglected. We present a solution in the form of ProMoBox, a framework that integrates the definition and verification of temporal properties in discrete-time behavioural DSMLs, whose semantics can be described as a schedule of graph rewrite rules. Thanks to the expressiveness of graph rewriting, this covers a very large class of problems. With ProMoBox, the domain user models not only the system with a DSML, but also its properties, input model, run-time state and output trace. A DSML is thus comprised of five sublanguages, which share domain-specific syntax, and are generated from a single metamodel. Generic transformations to and from a verification backbone ensure that both the language engineer and the domain user are shielded from underlying notations and techniques. We explicitly model the ProMoBox framework's process in the paper. Furthermore, we evaluate ProMoBox to assert that it supports the specification and verification of properties in a highly flexible and automated way.
Language
English
Source (journal)
IEEE transactions on software engineering. - New York, N.Y., 1975, currens
Publication
New York, N.Y. : Institute of Electrical and Electronics Engineers, 2020
ISSN
0098-5589 [print]
1939-3520 [online]
Volume/pages
46:4(2020), p. 362-404
ISI
000529529700002
Full text (Publisher's DOI)
Full text (open access)
UAntwerpen
Faculty/Department
Research group
Publication type
Subject
Affiliation
Publications with a UAntwerp address
External links
Web of Science
Record
Identification
Creation 08.10.2018
Last edited 27.07.2021
To cite this reference