DI-UMONS : Dépôt institutionnel de l’université de Mons

Recherche transversale
(titres de publication, de périodique et noms de colloque inclus)
2014-09-15 - Article/Dans un journal avec peer-review - Anglais - 20 page(s)

Deshayes Romuald, Meyers Bart, Lucio Levi, Syriani Eugene, Wimmer Manuel, Vangheluwe Hans, "ProMoBox: A Framework for Generating Domain-Specific Property Languages" in Lecture Notes in Computer Science, 8706, 1-20, 10.1007/978-3-319-11245-9_1

  • Edition : Springer, Heidelberg (Germany)
  • Codes CREF : Informatique appliquée logiciel (DI2570), Informatique générale (DI1162)
  • Unités de recherche UMONS : Génie Logiciel (S852)
  • Instituts UMONS : Institut de Recherche sur les Systèmes Complexes (Complexys), Institut NUMEDIART pour les Technologies des Arts Numériques (Numédiart)
  • Centres UMONS : Modélisation mathématique et informatique (CREMMI)

Abstract(s) :

(Anglais) 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.

Identifiants :
  • DOI : 10.1007/978-3-319-11245-9_1