Arrow Research search

Author name cluster

Volker Stolz

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers
1 author row

Possible papers

2

FM Conference 2026 Conference Paper

Distributed Runtime Verification in Proximity-Based Networks: A Tutorial on the Aggregate Programming Approach

  • Giorgio Audrito
  • Ferruccio Damiani
  • Giordano Scarso
  • Volker Stolz
  • Gianluca Torta

Abstract Distributed runtime verification (DRV) addresses the problem of checking the correctness of distributed systems during execution, coping with partial knowledge, dynamic topologies, and the absence of global time. These challenges are particularly prominent in proximity-based networks, such as those arising in IoT and Far Edge computing scenarios, where large numbers of devices interact through local communication. This tutorial presents an approach to DRV based on Aggregate Programming (AP), a paradigm for designing distributed collective systems via high-level abstractions over computational fields. We show how temporal and spatial properties (expressed in past-CTL and SLCS, respectively) can be systematically compiled into aggregate monitors grounded in the eXchange Calculus and executed using the FCPP C++ framework and simulator for AP. The tutorial combines conceptual foundations with practical guidance: participants learn how to specify spatio-temporal properties, generate corresponding monitors, and execute them in a 3D simulation environment. Examples are drawn from ongoing industrial collaborations and research projects, which we use to illustrate realistic monitoring scenarios and motivate open challenges for AP-based DRV.

DOI

TCS Journal 2025 Journal Article

Modular soundness checking of feature model evolution plans

  • Crystal Chang Din
  • Charaf Eddine Dridi
  • Ida Sandberg Motzfeldt
  • Violet Ka I Pun
  • Volker Stolz
  • Ingrid Chieh Yu

Feature model evolution plans (FMEPs) describe how feature models for software product lines (SPLs) evolve over time. While different feature models can exist for different points in time over the lifetime of the product line, an FMEP describes how to compute a feature model for a given time point. SPLs capitalise on the variability and reusability of the software through combining optional and mandatory features. As business requirements change over time, FMEPs should support intermediate update. A plan hence contains updates to an initial model by adding, deleting, moving or changing elements at different points in time, in line with the evolving business requirements on the SPL, potentially affecting feature models that should be derived in the future from the plan. A recurring challenge in maintaining FMEPs is that updates may lead to inconsistent intermediate feature models, most notably so-called paradoxes. A paradox may not materialise at the first point in time an update on the plan is performed to obtain a particular feature model, but may only in combination with a later modification prescribed by the plan create a structurally invalid model. Correspondingly, a single modification to a plan may require multiple checks over the liftetime of the affected elements to rule out paradoxes. Current approaches require the analysis from the point in time an update is applied to an FMEP throughout the entire lifetime of the plan. In this paper, we define a so-called interval-based feature model (IBFM) to represent FMEPs, with a precise definition of spatial and temporal scopes that narrow the time interval and the sub-models that an update can affect. We propose a rule system for updating IBFMs, and also prove the soundness of the proposed rules and show their modularity, i. e. , that each rule operates strictly within its temporal and spatial scopes. We have conducted a detailed evaluation on our modular approach and present the experimental results, which show that we outperform an existing linear approach.

Details DOI
v2026.09.13