Visualization of Formal Specifications for Understanding and Debugging an Industrial DSL
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.
KeywordsEvent-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.
- 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
- 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.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.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