Skip to main navigation Skip to search Skip to main content

Formally Characterizing the Effect of Model Transformations on System Properties

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

4 Downloads (Pure)

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 languageEnglish
Title of host publicationFormal Aspects of Component Software
Subtitle of host publication18th International Conference, FACS 2022, Virtual Event, November 10–11, 2022, Proceedings
EditorsSilvia Lizeth Tapia Tarifa, José Proença
Place of PublicationCham
PublisherSpringer
Pages39-58
Number of pages20
ISBN (Electronic)978-3-031-20872-0
ISBN (Print)978-3-031-20871-3
DOIs
Publication statusPublished - 2 Nov 2022
Event18th International Conference on Formal Aspects of Component Software, FACS 2022 - Virtual, Online
Duration: 10 Nov 202211 Nov 2022

Publication series

NameLecture Notes in Computer Science (LNCS)
Volume13712
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference18th International Conference on Formal Aspects of Component Software, FACS 2022
CityVirtual, Online
Period10/11/2211/11/22

Keywords

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

Fingerprint

Dive into the research topics of 'Formally Characterizing the Effect of Model Transformations on System Properties'. Together they form a unique fingerprint.

Cite this