Visualization of Formal Specifications for Understanding and Debugging an Industrial DSL

  • Ulyana TikhonovaEmail author
  • Maarten Manders
  • Rimco Boudewijns
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9946)


In this work we report on our proof of concept of a generic approach: visualized formal specification of a Domain Specific Language (DSL) can be used for debugging, understanding, and impact analysis of the DSL programs. In our case study we provide a domain-specific visualization for the Event-B specification of a real-life industrial DSL and perform a user study among DSL engineers to discover opportunities for its application. In this paper, we explain the rationale behind our visualization design, discuss the technical challenges of its realization and how these challenges were solved using the Model Driven Engineering (MDE) techniques. Based on the positive feedback of the user study, we present our vision on how this successful experience can be reused and the approach can be generalized for other DSLs.


Event-B Visualization Domain specific language User study 



We would like to thank Lukas Ladenberger (Heinrich-Heine University, Düsseldorf, Germany) for his help with using BMotion Studio. We are very grateful to all ASML engineers who participated in our user study. We also would like to thank Tom Verhoeff and Tim Willemse (both from Eindhoven University of Technology, The Netherlands) for their advice and feedback on this work and this paper.


  1. 1.
    Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York (2010)CrossRefzbMATHGoogle Scholar
  2. 2.
    Bandener, N., Soltenborn, C., Engels, G.: Extending DMM behavior specifications for visual execution and debugging. In: Malloy, B., Staab, S., Brand, M. (eds.) SLE 2010. LNCS, vol. 6563, pp. 357–376. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-19440-5_24 CrossRefGoogle Scholar
  3. 3.
    Chiş, A., Gîrba, T., Nierstrasz, O.: The moldable debugger: a framework for developing domain-specific debuggers. In: Combemale, B., Pearce, D.J., Barais, O., Vinju, J.J. (eds.) SLE 2014. LNCS, vol. 8706, pp. 102–121. Springer, Heidelberg (2014). doi: 10.1007/978-3-319-11245-9_6 Google Scholar
  4. 4.
    Hansen, D., Ladenberger, L., Wiegard, H., Bendisposto, J., Leuschel, M.: Validation of the ABZ landing gear system using ProB. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. CCIS, vol. 433, pp. 66–79. Springer, Heidelberg (2014). doi: 10.1007/978-3-319-07512-9_5 CrossRefGoogle Scholar
  5. 5.
    Ladenberger, L., Bendisposto, J., Leuschel, M.: Visualising Event-B models with B-motion studio. In: Alpuente, M., Cook, B., Joubert, C. (eds.) FMICS 2009. LNCS, vol. 5825, pp. 202–204. Springer, Heidelberg (2009). doi: 10.1007/978-3-642-04570-7_17 CrossRefGoogle Scholar
  6. 6.
    Ladenberger, L., Dobrikov, I., Leuschel, M.: An approach for creating domain specific visualisations of CSP models. In: Canal, C., Idani, A. (eds.) SEFM 2014. LNCS, vol. 8938, pp. 20–35. Springer, Heidelberg (2015). doi: 10.1007/978-3-319-15201-1_2 Google Scholar
  7. 7.
    Mathijssen, A., Pretorius, A.J.: Verified design of an automated parking garage. In: Brim, L., Haverkort, B., Leucker, M., Pol, J. (eds.) FMICS 2006. LNCS, vol. 4346, pp. 165–180. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-70952-7_11 CrossRefGoogle Scholar
  8. 8.
    Mauw, S., Wiersma, W.T., Willemse, T.A.C.: Language-driven system design. Int. J. Softw. Eng. Knowl. Eng. 14(6), 625–663 (2004)CrossRefGoogle Scholar
  9. 9.
    Silva, R., Butler, M.: Shared event composition/decomposition in Event-B. In: Aichernig, B.K., Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 122–141. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-25271-6_7 CrossRefGoogle Scholar
  10. 10.
    Snook, C., Butler, M.: UML-B: formal modeling and design aided by UML. ACM Trans. Softw. Eng. Methodol. 15(1), 92–122 (2006)CrossRefGoogle Scholar
  11. 11.
    Solingen, R.V., Berghout, E.: Goal/Question/Metric Method: A Practical Guide for Quality Improvement of Software Development. McGraw-Hill, Cambridge (1999)Google Scholar
  12. 12.
    Stappers, F.P.M.: Bridging formal models: an engineering perspective. Ph.d. dissertation. Chapter 6: Disseminating Verification Results, pp. 109–125. Eindhoven University of Technology (2012)Google Scholar
  13. 13.
    Tikhonova, U., Manders, M., van den Brand, M., Andova, S., Verhoeff, T.: Applying model transformation and Event-B for specifying an industrial DSL. In: MoDeVVa@MoDELS, pp. 41–50 (2013)Google Scholar
  14. 14.
    Watt, D.A., Muffy, T.: Programming Language Syntax and Semantics. Prentice Hall International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1991)zbMATHGoogle Scholar

Copyright information

© Springer International Publishing AG 2016

Authors and Affiliations

  • Ulyana Tikhonova
    • 1
    Email author
  • Maarten Manders
    • 1
  • Rimco Boudewijns
    • 1
  1. 1.Technische Universiteit EindhovenEindhovenThe Netherlands

Personalised recommendations