Checking property preservation of refining transformations for model-driven development

L.J.P. Engelen, A.J. Wijs

    Research output: Book/ReportReportAcademic

    89 Downloads (Pure)


    In Model-Driven Software Development, a software product is created through iteratively refined modelling. It is crucial that this process preserves certain desirable properties of the initial model. However, checking this is increasingly difficult as the models are increasingly more refined. We propose an incremental model checking technique to determine the preservation of safety and liveness properties in models of concurrent systems with respect to changes applied on individual processes, formalised as transformations of Labelled Transition Systems. The preservation check involves checking bisimilarity between transformed and new behaviour, and never involves reexploring unchanged behaviour. We prove its correctness and demonstrate its applicability.
    Original languageEnglish
    Place of PublicationEindhoven
    PublisherTechnische Universiteit Eindhoven
    Number of pages35
    Publication statusPublished - 2012

    Publication series

    NameComputer science reports
    ISSN (Print)0926-4515


    Dive into the research topics of 'Checking property preservation of refining transformations for model-driven development'. Together they form a unique fingerprint.

    Cite this