Abstrakt. Modellomvandlingar används i modelldriven utveckling för att mekanisera interoperabilitet och integration mellan modellspråk. På grund av modellernas grafteoretiska karaktär ger teorin om graftransformeringssystem och dess tekniska stöd en bekväm miljö för formalisering och verifiering av modelltransformationer, som sedan kan användas för att definiera semantiken hos modellbaserade domänspecifika språk. I detta dokument presenterar vi en metod för att formalisera och verifiera QVT-liknande omvandlingar som återanvänder de viktigaste begreppen i graftransformeringssystem. Specifikt formaliserar vi modellomvandlingar som teorier i omskrivningslogik, så att Maudes räckviddsanalys och modellkontrollfunktioner kan användas för att verifiera dem. Detta tillvägagångssätt ger också ett nytt perspektiv på grafomvandlingssystem, där deras formella semantik ges i omskrivningslogik. Alla idéer som presenteras är implementerade i MOMENT2. På så sätt kan vi definiera formella modellomvandlingar i Eclipse Modeling Framework (EMF) och vi kan verifiera dem i Maude. Vi använder en modell av en distribuerad algoritm för ömsesidig uteslutning för att illustrera tillvägagångssättet.
En annan arbetslinje som föreslås i REF definierar ett QVT-liknande modelltransformeringsspråk som återanvänder de viktigaste begreppen i graftransformeringssystem.
Rewriting Logic Semantics and Verification of Model Transformations
{'venue': 'FASE', 'journal': None, 'mag_field_of_study': ['Computer Science']}