Interaction detection in configurable systems – A formal approach featuring roles

Research output: Contribution to journalResearch articleContributedpeer-review

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

Original languageEnglish
Article number111556
JournalJournal of Systems and Software
Volume196
Publication statusPublished - Feb 2023
Peer-reviewedYes

External IDs

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

Keywords

Keywords

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

Library keywords