Applying model transformation and Event-B for specifying an industrial DSL
Ulyana Tikhonova, MW Maarten Manders, Mark van den Brand, Suzana Andova, T Tom Verhoeff · TU/e Research Portal · 2013
Abstract. In this paper we describe our experience in applying the Event-B formalism for specifying the dynamic semantics of a real-life in-dustrial DSL. The main objective of this work is to enable the industrial use of the broad spectrum of specification analysis tools that support Event-B. To leverage the usage of Event-B and its analysis techniques we developed model transformations, that allowed for automatic gener-ation of Event-B specifications of the DSL programs. The model trans-formations implement a modular approach for specifying the semantics of the DSL and, therefore, improve scalability of the specifications and the reuse of their verification. Key words: domain specific language, Event-B, model transformations, verification and validation, reuse, scalability 1