Using a DSL and fine-grained model : transformations to explore the boundaries of model verification

M.F. Amstel, van, M.G.J. Brand, van den, L.J.P. Engelen

    Research output: Book/ReportReportAcademic

    84 Downloads (Pure)

    Abstract

    Traditionally, the state-space explosion problem in model checking is handled by applying abstractions and simplifications to the model that needs to be verified. In this paper, we propose a model-driven engineering approach that works the other way around. Instead of making a concrete model more abstract, we propose to refine an abstract model to make it more concrete. We propose to use fine-grained model transformations to enable model checking of models that are as close to the implementation model as possible. We applied our approach in a case study. The results show that it is possible to validate models that are more concrete when fine-grained transformations are applied.
    Original languageEnglish
    Place of PublicationEindhoven
    PublisherTechnische Universiteit Eindhoven
    Publication statusPublished - 2011

    Publication series

    NameComputer science reports
    Volume1102
    ISSN (Print)0926-4515

    Fingerprint Dive into the research topics of 'Using a DSL and fine-grained model : transformations to explore the boundaries of model verification'. Together they form a unique fingerprint.

    Cite this