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

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Conferentiebijdrage › Academic › peer review

1 Citaat (Scopus)

Samenvatting

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.

Originele taal-2	Engels
Titel	Formal Aspects of Component Software - 18th International Conference, FACS 2022, Proceedings
Redacteuren	Silvia Lizeth Tapia Tarifa, José Proença
Uitgeverij	Springer
Pagina's	39-58
Aantal pagina's	20
ISBN van geprinte versie	9783031208713
DOI's	https://doi.org/10.1007/978-3-031-20872-0_3
Status	Gepubliceerd - 2022
Evenement	18th International Conference on Formal Aspects of Component Software, FACS 2022 - Virtual, Online Duur: 10 nov. 2022 → 11 nov. 2022

Publicatie series

Naam	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	13712 LNCS
ISSN van geprinte versie	0302-9743
ISSN van elektronische versie	1611-3349

Congres

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

Bibliografische nota

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

Toegang tot document

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

Andere bestanden en links

Link naar publicatie in Scopus

Citeer dit

Chaki, R., & Wijs, A. (2022). Formally Characterizing the Effect of Model Transformations on System Properties. In S. L. Tapia Tarifa, & J. Proença (editors), Formal Aspects of Component Software - 18th International Conference, FACS 2022, Proceedings (blz. 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. redacteur / Silvia Lizeth Tapia Tarifa ; José Proença. Springer, 2022. blz. 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",

address = "Germany",

}

Chaki, R & Wijs, A 2022, Formally Characterizing the Effect of Model Transformations on System Properties. in SL Tapia Tarifa & J Proença (uitgave), 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, blz. 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. uitgave / Silvia Lizeth Tapia Tarifa; José Proença. Springer, 2022. blz. 39-58 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13712 LNCS).

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Conferentiebijdrage › 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, redacteurs, Formal Aspects of Component Software - 18th International Conference, FACS 2022, Proceedings. Springer. 2022. blz. 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

Samenvatting

Publicatie series

Congres

Bibliografische nota

Toegang tot document

Andere bestanden en links

Vingerafdruk

Citeer dit