Dynamic Reconfiguration via Typed Modalities

Ionut Tutu, Claudia Chirita, José Luiz Fiadeiro

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

Abstract

Modern software systems are increasingly exhibiting dynamic-reconfiguration features analogous to naturally occurring phenomena where the architecture of a complex changes dynamically, at run time, on account of interactions between its components. This has led to a renewed interest in modal logics for formal system development, building on the intuitive idea that system configurations can be regarded as local models of a Kripke structure, while reconfigurations are captured by accessibility relations. We contribute to this line of research by advancing a modal logic with varying quantification domains that employs typed modalities and dedicated modal operators to specify and reason about a new generation of Kripke structures, called dynamic networks of interactions, that account for the context of a system’s dynamics, identifying which actants have triggered a reconfiguration and what are its outcomes. To illustrate the expressiveness of the formalism, we provide a specification of the biological process of membrane budding, which we then analyse using a sound and complete proof-by-translation method that links dynamic networks of interactions with partial first-order logic.

Original languageEnglish
Title of host publicationFormal Methods
Subtitle of host publication24th International Symposium, FM 2021, Virtual Event, November 20–26, 2021, Proceedings
EditorsMarieke Huisman, Corina Păsăreanu, Naijun Zhan
PublisherSpringer
Pages599-615
Number of pages17
Edition1
ISBN (Electronic)9783030908706
ISBN (Print)9783030908690
DOIs
Publication statusPublished - 10 Nov 2021

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume13047
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Keywords

  • Modal logic
  • Partial first-order logic
  • Reconfigurable systems
  • Standard translation
  • Typed modalities

Fingerprint

Dive into the research topics of 'Dynamic Reconfiguration via Typed Modalities'. Together they form a unique fingerprint.

Cite this