ProMoBox: A Framework for Generating Domain-Specific Property Languages

  • Bart Meyers
  • Romuald Deshayes
  • Levi Lucio
  • Eugene Syriani
  • Hans Vangheluwe
  • Manuel Wimmer
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8706)


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.


Model Check Structural Pattern Operational Semantic Linear Temporal Logic Generic Language 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Gray, J., Tolvanen, J.P., Kelly, S., Gokhale, A., Neema, S., Sprinkle, J.: Domain-specific modeling. In: Handbook of Dynamic System Modeling (2007)Google Scholar
  2. 2.
    France, R., Rumpe, B.: Model-driven development of complex software: A research roadmap. In: ICSE (2007)Google Scholar
  3. 3.
    Risoldi, M.: A Methodology For The Development Of Complex Domain Specific Languages. PhD thesis, University of Geneva (2010)Google Scholar
  4. 4.
    Visser, W., Dwyer, M., Whalen, M.: The hidden models of model checking. SoSym 11, 541–555 (2012)Google Scholar
  5. 5.
    Meyers, B., Deshayes, R., Lucio, L., Syriani, E., Wimmer, M., Vangheluwe, H.: The ProMoBox approach to language modelling. Technical Report SOCS-TR-2014.3, School of Computer Science, McGill University (2014)Google Scholar
  6. 6.
    Meyers, B., Wimmer, M., Vangheluwe, H.: Towards domain-specific property languages: The ProMoBox approach. In: DSM (2013)Google Scholar
  7. 7.
    Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in Property Specifications for Finite-State Verification. In: ICSE (1999)Google Scholar
  8. 8.
    Kühne, T., Mezei, G., Syriani, E., Vangheluwe, H., Wimmer, M.: Explicit transformation modeling. In: Ghosh, S. (ed.) MODELS 2009. LNCS, vol. 6002, pp. 240–255. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  9. 9.
    Syriani, E.: A Multi-Paradigm Foundation for Model Transformation Language Engineering. PhD thesis, McGill University Montreal, Canada (2011)Google Scholar
  10. 10.
    Guerra, E., de Lara, J., Kolovos, D.S., Paige, R.F.: A Visual Specification Language for Model-to-Model Transformations. In: VL/HCC (2010)Google Scholar
  11. 11.
    Guerra, E., de Lara, J., Wimmer, M., et al.: Automated verification of model transformations based on visual contracts. ASE 20, 5–46 (2013)Google Scholar
  12. 12.
    Holzmann, G.J.: The Model Checker SPIN. TSE 23, 279–295 (1997)CrossRefGoogle Scholar
  13. 13.
    Syriani, E., Vangheluwe, H., Mannadiar, R., Hansen, C., Mierlo, S.V., Ergin, H.: AToMPM: A Web-based Modeling Environment. In: MoDELS Demonstrations (2013)Google Scholar
  14. 14.
    Lin, Y., Gray, J., Jouault, F.: DSMDiff: A Differentiation Tool for Domain-Specific Models. European Journal of Information Systems 16 (2007)Google Scholar
  15. 15.
    Cimatti, A., Mover, S., Tonetta, S.: Proving and Explaining the Unfeasibility of Message Sequence Charts for Hybrid Systems. In: FMCAD (2011)Google Scholar
  16. 16.
    Li, X., Hu, J., Bu, L., Zhao, J., Zheng, G.: Consistency Checking of Concurrent Models for Scenario-Based Specifications. In: Prinz, A., Reed, R., Reed, J. (eds.) SDL 2005. LNCS, vol. 3530, pp. 298–312. Springer, Heidelberg (2005)Google Scholar
  17. 17.
    Pelliccione, P., Inverardi, P., Muccini, H.: CHARMY: A Framework for Designing and Verifying Architectural Specifications. TSE 35, 325–346 (2008)CrossRefGoogle Scholar
  18. 18.
    Brosch, P., Egly, U., Gabmeyer, S., Kappel, G., Seidl, M., Tompits, H., Widl, M., Wimmer, M.: Towards Scenario-Based Testing of UML Diagrams. In: Brucker, A.D., Julliand, J. (eds.) TAP 2012. LNCS, vol. 7305, pp. 149–155. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  19. 19.
    Knapp, A., Wuttke, J.: Model checking of UML 2.0 interactions. In: Kühne, T. (ed.) MoDELS 2006. LNCS, vol. 4364, pp. 42–51. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  20. 20.
    Schäfer, T., Knapp, A., Merz, S.: Model Checking UML State Machines and Collaborations. ENTCS 55, 357–369 (2001)Google Scholar
  21. 21.
    Rivera, J.E., Guerra, E., de Lara, J., Vallecillo, A.: Analyzing Rule-Based Behavioral Semantics of Visual Modeling Languages with Maude. In: Gašević, D., Lämmel, R., Van Wyk, E. (eds.) SLE 2008. LNCS, vol. 5452, pp. 54–73. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  22. 22.
    Gabmeyer, S., Kaufmann, P., Seidl, M.: A classification of model checking-based verification approaches for software models. In: VOLT (2013)Google Scholar
  23. 23.
    Ziemann, P., Gogolla, M.: OCL Extended with Temporal Logic. In: Broy, M., Zamulin, A.V. (eds.) PSI 2003. LNCS, vol. 2890, pp. 351–357. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  24. 24.
    Kanso, B., Taha, S.: Temporal Constraint Support for OCL. In: Czarnecki, K., Hedin, G. (eds.) SLE 2012. LNCS, vol. 7745, pp. 83–103. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  25. 25.
    Bill, R., Gabmeyer, S., Kaufmann, P., Seidl, M.: OCL meets CTL: Towards CTL-Extended OCL Model Checking. In: OCL Workshop (2013)Google Scholar
  26. 26.
    Zalila, F., Crégut, X., Pantel, M.: Leveraging Formal Verification Tools for DSML Users: A Process Modeling Case Study. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part II. LNCS, vol. 7610, pp. 329–343. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  27. 27.
    Combemale, B., Crégut, X., Pantel, M.: A Design Pattern to Build Executable DSMLs and Associated V&V Tools. In: APSEC (2012)Google Scholar
  28. 28.
    Klein, F., Giese, H.: Joint structural and temporal property specification using timed story scenario diagrams. In: Dwyer, M.B., Lopes, A. (eds.) FASE 2007. LNCS, vol. 4422, pp. 185–199. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  29. 29.
    Fischer, T., Niere, J., Torunski, L., Zündorf, A.: Story Diagrams: A New Graph Rewrite Language Based on the Unified Modeling Language and Java. In: Ehrig, H., Engels, G., Kreowski, H.-J., Rozenberg, G. (eds.) TAGT 1998. LNCS, vol. 1764, pp. 296–309. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  30. 30.
    da Costa Cavalheiro, S.A., Foss, L., Ribeiro, L.: Specification Patterns for Properties over Reachable States of Graph Grammars. In: Gheyi, R., Naumann, D. (eds.) SBMF 2012. LNCS, vol. 7498, pp. 83–98. Springer, Heidelberg (2012)Google Scholar
  31. 31.
    Deshayes, R., Palanque, P.A., Mens, T.: A generic framework for executable gestural interaction models. In: VL/HCC (2013)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Bart Meyers
    • 1
  • Romuald Deshayes
    • 2
  • Levi Lucio
    • 3
  • Eugene Syriani
    • 4
  • Hans Vangheluwe
    • 1
    • 3
  • Manuel Wimmer
    • 5
  1. 1.Modeling, Simulation and Design Lab (MSDL)University of AntwerpBelgium
  2. 2.Institut d’InformatiqueUniversit de MonsMonsBelgium
  3. 3.Modeling, Simulation and Design Lab (MSDL)McGill UniversityCanada
  4. 4.Software Engineering Research Group (SERG)University of AlabamaUSA
  5. 5.Business Informatics Group (BIG)Vienna University of TechnologyAustria

Personalised recommendations