Checking property preservation of refining transformations for model-driven development

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

Research output: Book/ReportReportAcademic

75 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