Interaction detection in configurable systems – A formal approach featuring roles
Research output: Contribution to journal › Research article › Contributed › peer-review
Contributors
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 language | English |
---|---|
Article number | 111556 |
Journal | Journal of Systems and Software |
Volume | 196 |
Publication status | Published - Feb 2023 |
Peer-reviewed | Yes |
External IDs
ORCID | /0000-0002-5321-9343/work/160951235 |
---|---|
ORCID | /0000-0003-1724-2586/work/165453616 |
Keywords
ASJC Scopus subject areas
Keywords
- Feature-oriented systems, Formal methods, Model checking, Role-oriented systems, Software product lines