Formally Characterizing the Effect of Model Transformations on System Properties

Rikayan Chaki; Anton Wijs

doi:10.1007/978-3-031-20872-0_3

Formally Characterizing the Effect of Model Transformations on System Properties

Rikayan Chaki, Anton Wijs

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

1 Citation (Scopus)

Abstract

In Model-Driven Software Development, models and model transformations are the primary artefacts to develop software in a structured way. Models have been subjected to formal verification for a long time, but the field of formal model transformation verification is relatively young. Existing techniques, when they focus on the effect transformations have on the system components they are applied on, limit their analysis to checking for the preservation of semantics or particular properties, but it is not always the intention of a transformation to preserve these. We propose an approach to characterize the effect of applying a (formal description of a) model transformation when applied on a component that satisfies a given functional property. The given functional property is formalized in Action-based LTL, and our characterization is captured by a system of modal μ -calculus equations.

Original language	English
Title of host publication	Formal Aspects of Component Software - 18th International Conference, FACS 2022, Proceedings
Editors	Silvia Lizeth Tapia Tarifa, José Proença
Publisher	Springer
Pages	39-58
Number of pages	20
ISBN (Print)	9783031208713
DOIs	https://doi.org/10.1007/978-3-031-20872-0_3
Publication status	Published - 2022
Event	18th International Conference on Formal Aspects of Component Software, FACS 2022 - Virtual, Online Duration: 10 Nov 2022 → 11 Nov 2022

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	13712 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	18th International Conference on Formal Aspects of Component Software, FACS 2022
City	Virtual, Online
Period	10/11/22 → 11/11/22

Bibliographical note

Publisher Copyright:
© 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.

Keywords

Büchi automata
Labeled transition systems
Linear temporal logic
Model transformations
system evolution
μ -calculus

Access to Document

10.1007/978-3-031-20872-0_3

Cite this

Chaki, R., & Wijs, A. (2022). Formally Characterizing the Effect of Model Transformations on System Properties. In S. L. Tapia Tarifa, & J. Proença (Eds.), Formal Aspects of Component Software - 18th International Conference, FACS 2022, Proceedings (pp. 39-58). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13712 LNCS). Springer. https://doi.org/10.1007/978-3-031-20872-0_3

Chaki, Rikayan ; Wijs, Anton. / Formally Characterizing the Effect of Model Transformations on System Properties. Formal Aspects of Component Software - 18th International Conference, FACS 2022, Proceedings. editor / Silvia Lizeth Tapia Tarifa ; José Proença. Springer, 2022. pp. 39-58 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{0d97f3dcf29640858b21068c87264081,

title = "Formally Characterizing the Effect of Model Transformations on System Properties",

abstract = "In Model-Driven Software Development, models and model transformations are the primary artefacts to develop software in a structured way. Models have been subjected to formal verification for a long time, but the field of formal model transformation verification is relatively young. Existing techniques, when they focus on the effect transformations have on the system components they are applied on, limit their analysis to checking for the preservation of semantics or particular properties, but it is not always the intention of a transformation to preserve these. We propose an approach to characterize the effect of applying a (formal description of a) model transformation when applied on a component that satisfies a given functional property. The given functional property is formalized in Action-based LTL, and our characterization is captured by a system of modal μ -calculus equations.",

keywords = "B{\"u}chi automata, Labeled transition systems, Linear temporal logic, Model transformations, system evolution, μ -calculus",

author = "Rikayan Chaki and Anton Wijs",

note = "Publisher Copyright: {\textcopyright} 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.; 18th International Conference on Formal Aspects of Component Software, FACS 2022 ; Conference date: 10-11-2022 Through 11-11-2022",

year = "2022",

doi = "10.1007/978-3-031-20872-0_3",

language = "English",

isbn = "9783031208713",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "39--58",

editor = "{Tapia Tarifa}, {Silvia Lizeth} and Jos{\'e} Proen{\c c}a",

booktitle = "Formal Aspects of Component Software - 18th International Conference, FACS 2022, Proceedings",

}

Chaki, R & Wijs, A 2022, Formally Characterizing the Effect of Model Transformations on System Properties. in SL Tapia Tarifa & J Proença (eds), Formal Aspects of Component Software - 18th International Conference, FACS 2022, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 13712 LNCS, Springer, pp. 39-58, 18th International Conference on Formal Aspects of Component Software, FACS 2022, Virtual, Online, 10/11/22. https://doi.org/10.1007/978-3-031-20872-0_3

Formally Characterizing the Effect of Model Transformations on System Properties. / Chaki, Rikayan; Wijs, Anton.
Formal Aspects of Component Software - 18th International Conference, FACS 2022, Proceedings. ed. / Silvia Lizeth Tapia Tarifa; José Proença. Springer, 2022. p. 39-58 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13712 LNCS).

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

TY - GEN

T1 - Formally Characterizing the Effect of Model Transformations on System Properties

AU - Chaki, Rikayan

AU - Wijs, Anton

PY - 2022

Y1 - 2022

N2 - In Model-Driven Software Development, models and model transformations are the primary artefacts to develop software in a structured way. Models have been subjected to formal verification for a long time, but the field of formal model transformation verification is relatively young. Existing techniques, when they focus on the effect transformations have on the system components they are applied on, limit their analysis to checking for the preservation of semantics or particular properties, but it is not always the intention of a transformation to preserve these. We propose an approach to characterize the effect of applying a (formal description of a) model transformation when applied on a component that satisfies a given functional property. The given functional property is formalized in Action-based LTL, and our characterization is captured by a system of modal μ -calculus equations.

AB - In Model-Driven Software Development, models and model transformations are the primary artefacts to develop software in a structured way. Models have been subjected to formal verification for a long time, but the field of formal model transformation verification is relatively young. Existing techniques, when they focus on the effect transformations have on the system components they are applied on, limit their analysis to checking for the preservation of semantics or particular properties, but it is not always the intention of a transformation to preserve these. We propose an approach to characterize the effect of applying a (formal description of a) model transformation when applied on a component that satisfies a given functional property. The given functional property is formalized in Action-based LTL, and our characterization is captured by a system of modal μ -calculus equations.

KW - Büchi automata

KW - Labeled transition systems

KW - Linear temporal logic

KW - Model transformations

KW - system evolution

KW - μ -calculus

UR - http://www.scopus.com/inward/record.url?scp=85142739177&partnerID=8YFLogxK

U2 - 10.1007/978-3-031-20872-0_3

DO - 10.1007/978-3-031-20872-0_3

M3 - Conference contribution

AN - SCOPUS:85142739177

SN - 9783031208713

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 39

EP - 58

BT - Formal Aspects of Component Software - 18th International Conference, FACS 2022, Proceedings

A2 - Tapia Tarifa, Silvia Lizeth

A2 - Proença, José

PB - Springer

T2 - 18th International Conference on Formal Aspects of Component Software, FACS 2022

Y2 - 10 November 2022 through 11 November 2022

ER -

Chaki R, Wijs A. Formally Characterizing the Effect of Model Transformations on System Properties. In Tapia Tarifa SL, Proença J, editors, Formal Aspects of Component Software - 18th International Conference, FACS 2022, Proceedings. Springer. 2022. p. 39-58. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-031-20872-0_3

Formally Characterizing the Effect of Model Transformations on System Properties

Abstract

Publication series

Conference

Bibliographical note

Keywords

Access to Document

Other files and links

Fingerprint

Cite this