Publication
Title
ProMoBox : a framework for generating domain-specific property languages
Author
Abstract
Specifying and verifying properties of the modelled system has been mostly neglected by domain-specific modelling (DSM) approaches. At best, this is only partially supported by translating models to formal representations on which properties are specified and evaluated based on logic-based formalisms, such as linear temporal logic. This contradicts the DSM philosophy as domain experts are usually not familiar with the logics space. To overcome this shortcoming, we propose to shift property specification and verification tasks up to the domain-specific level. The ProMoBox framework consists of (i) generic languages for modelling properties and representing verification results, (ii) a fully automated method to specialize and integrate these generic languages to a given DSM language, and (iii) a verification backbone based model checking directly plug-able to DSM environments. In its current state, ProMoBox offers the designer modelling support for defining temporal properties, and for visualizing verification results, all based on a given DSM language. We report results of applying ProMoBox to a case study of an elevator controller.
Language
English
Source (journal)
Lecture notes in computer science. - Berlin, 1973, currens
Publication
Berlin : 2014
ISSN
0302-9743 [print]
1611-3349 [online]
Volume/pages
8706(2014), p. 1-20
ISI
000348352300002
Full text (Publisher's DOI)
UAntwerpen
Faculty/Department
Research group
Publication type
Subject
Affiliation
Publications with a UAntwerp address
External links
Web of Science
Record
Identification
Creation 13.03.2015
Last edited 18.07.2017
To cite this reference