Applying model transformation and Event-B for specifying an industrial DSL

U. Tikhonova, M.W. Manders, M.G.J. Brand, van den, S. Andova, T. Verhoeff

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    8 Citations (Scopus)
    60 Downloads (Pure)

    Abstract

    In this paper we describe our experience in applying the Event-B formalism for specifying the dynamic semantics of a real-life industrial 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 generation of Event-B specifications of the DSL programs. The model transformations implement a modular approach for specifying the semantics of the DSL and, therefore, improve scalability of the specifications and the reuse of their verification. Keywords: domain specific language, Event-B, model transformations, verification and validation, reuse, scalability
    Original languageEnglish
    Title of host publicationMoDeVVa 2013 : Workshop on Model Driven Engineering, Verification and Validation : Proceedings of the 10th International Workshop on Model Driven Engineering, Verification and Validation co-located with 16th International Conference on Model Driven Engineering Miami, Florida, October 1st, 2013
    EditorsF. Boulanger, M. Famelis, D. Ratiu
    PublisherCEUR-WS.org
    Pages41-50
    Publication statusPublished - 2013
    Event10th International Workshop on Model Driven Engineering, Verification and Validation -
    Duration: 1 Oct 20131 Oct 2013

    Publication series

    NameCEUR Workshop Proceedings
    Volume1069
    ISSN (Print)1613-0073

    Conference

    Conference10th International Workshop on Model Driven Engineering, Verification and Validation
    Period1/10/131/10/13

    Fingerprint Dive into the research topics of 'Applying model transformation and Event-B for specifying an industrial DSL'. Together they form a unique fingerprint.

    Cite this