Temporal Logic Specification and Analysis for Model Transformations

Sobhan Yassipour Tehrani; Kevin Charles Lano

Temporal Logic Specification and Analysis for Model Transformations

Sobhan Yassipour Tehrani, Kevin Charles Lano

Research output: Chapter in Book/Report/Conference proceeding › Conference paper › peer-review

45 Downloads (Pure)

Abstract

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.

Original language	English
Title of host publication	Staf Workshop on Verification of Model Transformations, VOLT 2015
Publisher	Verification Of ModeL Transformation (VOLT 2015)
Publication status	Published - 23 Jul 2015
Event	Staf Workshop on Verification of Model Transformations - L'Aquila, Italy Duration: 23 Jul 2015 → 23 Jul 2015

Conference

Conference	Staf Workshop on Verification of Model Transformations
Country/Territory	Italy
City	L'Aquila
Period	23/07/2015 → 23/07/2015

Access to Document

Temporal Logic Specification_YASSIPOUR-TEHRANI_Accepted12June2015_GREEN AAMAccepted author manuscript, 84.7 KB

http://volt2015.big.tuwien.ac.at/data/submissions/paper_1.pdf

Cite this

@inbook{4dddaae8248b446789f793d17a6c1ebf,

title = "Temporal Logic Specification and Analysis for Model Transformations",

abstract = "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.",

author = "{Yassipour Tehrani}, Sobhan and Lano, {Kevin Charles}",

year = "2015",

month = jul,

day = "23",

language = "English",

booktitle = "Staf Workshop on Verification of Model Transformations, VOLT 2015",

publisher = "Verification Of ModeL Transformation (VOLT 2015)",

note = "Staf Workshop on Verification of Model Transformations ; Conference date: 23-07-2015 Through 23-07-2015",

}

Yassipour Tehrani, S & Lano, KC 2015, Temporal Logic Specification and Analysis for Model Transformations. in Staf Workshop on Verification of Model Transformations, VOLT 2015. Verification Of ModeL Transformation (VOLT 2015), Staf Workshop on Verification of Model Transformations, L'Aquila, Italy, 23/07/2015. <http://volt2015.big.tuwien.ac.at/data/submissions/paper_1.pdf>

TY - CHAP

T1 - Temporal Logic Specification and Analysis for Model Transformations

AU - Yassipour Tehrani, Sobhan

AU - Lano, Kevin Charles

PY - 2015/7/23

Y1 - 2015/7/23

N2 - 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.

AB - 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.

UR - http://volt2015.big.tuwien.ac.at/index.html

M3 - Conference paper

BT - Staf Workshop on Verification of Model Transformations, VOLT 2015

PB - Verification Of ModeL Transformation (VOLT 2015)

T2 - Staf Workshop on Verification of Model Transformations

Y2 - 23 July 2015 through 23 July 2015

ER -

Temporal Logic Specification and Analysis for Model Transformations

Abstract

Conference

Access to Document

Other files and links

Fingerprint

Cite this