King's College London

Research portal

Temporal Logic Specification and Analysis for Model Transformations

Research output: Chapter in Book/Report/Conference proceedingConference paper

Original languageEnglish
Title of host publicationStaf Workshop on Verification of Model Transformations, VOLT 2015
PublisherVerification Of ModeL Transformation (VOLT 2015)
Publication statusPublished - 23 Jul 2015
EventStaf Workshop on Verification of Model Transformations - L'Aquila, Italy
Duration: 23 Jul 201523 Jul 2015


ConferenceStaf Workshop on Verification of Model Transformations


King's Authors


In this paper we outline an approach for using temporal logic specifications and model-checking tools to express and verify model transformation properties. Linear Temporal Logic (LTL) is used to express transformation semantics, and the SMV formalism is used to encode this semantics and to perform model checking.

View graph of relations

© 2018 King's College London | Strand | London WC2R 2LS | England | United Kingdom | Tel +44 (0)20 7836 5454