Interaction detection in configurable systems – A formal approach featuring roles

Publikation: Beitrag in FachzeitschriftForschungsartikelBeigetragenBegutachtung

Abstract

Modern software systems are increasingly complex due to their configurability and adaptivity. For modeling and implementing such systems, the concept of roles is particularly well-suited as it allows capturing context-dependent properties and behavior. Similar to other compositional approaches, notably the feature-oriented development approach, the detection of (unintended) interactions between roles is a challenging task. We consider two new aspects of interactions. Hierarchical interactions may occur between systems and active interplays describe the actual situations in a sequence of events where components interact. To reason about such interactions, we introduce a compositional modeling framework based on concepts and notions of roles, comprising role-based automata (RBAs). Based on this formal foundation, we present a modeling language for succinctly describing RBAs and an implementation for translating this language into the input language of the probabilistic model checker PRISM. This enables a formal analysis of functional and non-functional properties including system dynamics, context changes, and interactions. We carry out three experimental studies as a proof of concept of such analyses: First, a peer-to-peer protocol study illustrates how undesired hierarchical interactions can be discovered automatically. Second, a study on a self-adaptive production cell demonstrates how undesired interactions influence quality-of-service measures such as reliability and throughput. Third, we illustrate how to incorporate feature-oriented system design in our role-oriented framework by means of the elevator community benchmark system.

Details

OriginalspracheEnglisch
Aufsatznummer111556
FachzeitschriftJournal of Systems and Software
Jahrgang196
PublikationsstatusVeröffentlicht - Feb. 2023
Peer-Review-StatusJa

Externe IDs

ORCID /0000-0002-5321-9343/work/160951235
ORCID /0000-0003-1724-2586/work/165453616

Schlagworte

Schlagwörter

  • Feature-oriented systems, Formal methods, Model checking, Role-oriented systems, Software product lines

Bibliotheksschlagworte