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

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

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

    4 Citations (Scopus)

    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 models that are more concrete can be validated when fine-grained transformations are applied.
    Original languageEnglish
    Title of host publicationProceedings of the 2011 IEEE Fourth International Conference on Software Testing, Verification and Validation Workshops (ICSTW 2011, Berlin, Germany, March 21-25, 2011)
    Place of PublicationPiscataway
    PublisherInstitute of Electrical and Electronics Engineers
    Pages63-66
    ISBN (Print)978-0-7695-4345-1
    DOIs
    Publication statusPublished - 2011
    Event4th IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW 2011) - Berlin, Germany
    Duration: 21 Mar 201125 Mar 2011
    Conference number: 4

    Conference

    Conference4th IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW 2011)
    Abbreviated titleICSTW 2011
    CountryGermany
    CityBerlin
    Period21/03/1125/03/11

    Fingerprint

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

    Cite this