Checking property preservation of refining transformations for model-driven development

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

Onderzoeksoutput: Boek/rapportRapportAcademic

68 Downloads (Pure)

Samenvatting

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.
Originele taal-2Engels
Plaats van productieEindhoven
UitgeverijTechnische Universiteit Eindhoven
Aantal pagina's35
StatusGepubliceerd - 2012

Publicatie series

NaamComputer science reports
Volume1208
ISSN van geprinte versie0926-4515

Vingerafdruk Duik in de onderzoeksthema's van 'Checking property preservation of refining transformations for model-driven development'. Samen vormen ze een unieke vingerafdruk.

Citeer dit