Dynamic Reconfiguration via Typed Modalities

TY - GEN

T1 - Dynamic Reconfiguration via Typed Modalities

AU - Tutu, Ionut

AU - Chirita, Claudia

AU - Fiadeiro, José Luiz

N1 - Copyright: © 2021 Springer Nature Switzerland AG.

PY - 2021/11/10

Y1 - 2021/11/10

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

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

KW - Modal logic

KW - Partial first-order logic

KW - Reconfigurable systems

KW - Standard translation

KW - Typed modalities

UR - https://www.scopus.com/pages/publications/85119828654

U2 - 10.1007/978-3-030-90870-6_32

DO - 10.1007/978-3-030-90870-6_32

M3 - Conference contribution

SN - 9783030908690

T3 - Lecture Notes in Computer Science

SP - 599

EP - 615

BT - Formal Methods

A2 - Huisman, Marieke

A2 - Păsăreanu, Corina

A2 - Zhan, Naijun

PB - Springer

ER -