Trends in Configurable Systems Analysis

Most of nowadays computing systems are configurable. Their configuration spaces are usually of exponential size in the number of parameters such that these configurable systems require specialized methods for their design, implementation, and analysis. While there have been significant advances for the analysis of configurable systems in the last decade, e.g., by parametric, family-based, or feature-based analysis, there are still manifold opportunities that have not yet been considered exhaustively. These cover specialized algorithms concerning quantitative aspects, required to model and analyze modern cyber-physical systems, as well as reconfigurations that allow for system adaptations in context-aware system design. The main goal of this workshop is to bring researchers together, presenting ideas and challenges, develop new ideas, and foster collaborations within the field of configurable systems analysis.

The workshop takes place on the 23rd of April 2023 in Paris, France, directly before the main joint conference ETAPS 2023.

Workshop format

The workshop comprises an invited keynote, talks on submitted abstracts, and discussion rounds on trends in configurable systems analysis. It is planned to publish post-proceedings of full papers from the presentations.

  1. Presentation abstracts submitted should not exceed 2 pages and may include already published material, unpublished work, and even challenges. They will be reviewed for suitability. At least one of the authors has to provide a presentation at TiCSA'23, issuing the abstract.
  2. Full papers are submitted after a presentation at the workshop, describe original research, provide surveys, or report on the findings during the workshop. They should not exceed 12 pages excluding references. Such papers will undergo a full reviewing process by at least three members of the program committee. Final versions of accepted papers will be published in the EPTCS workshop series.


Tentative Program

The workshop program is not completely determined. Stay tuned for any changes published here. Location: IHP Room 421
CEST Session Speakers Topic
8:45OpeningMaurice ter Beek and Clemens Dubslaff Workshop format and introduction
9:00KeynoteÉtienne André Configuring timing parameters to ensure opacity
10:00Coffee break
10:30Davide Basile Static Detection of Equivalent Mutants through Monotonicity of Parametric Timed Games
10:55José Proença, Giann Nandi, David Pereira, Sina Borrami, and Jonas Melchert Spreadsheet-based configuration of Families of Real-Time Specifications
11:20Pascal Krapf, Nicole Levy, and Sébastien Berthier Configurable system or product line?
11:45Michel Reniers Supervisory Control for Dynamic Feature Configuration in Product Lines
12:10Saverio Giallorenzo, Cosimo Laneve, and Gianluigi Zavattaro Serverless Scheduling Policies based on Cost Analysis
12:35Lunch break
14:00Thiago D. Simão Offline Reinforcement Learning Algorithms for Factored Environments
14:25Inspiration TalkAlfons Laarman LIMDD -- A Decision Diagram for Simulation of Quantum Computing
14:50Discussion Round Quantum Configurable Systems and Configurable Quantum Systems
16:00Closing
16:05Coffee break

Keynote Speaker

Étienne André

His works focus on theoretical computer science, and more specifically in the formal verification of distributed timed systems, under some uncertainty. In particular, Étienne has a high interest in parametric timed systems, where some timing constants can be uncertain or unknown. He notably focuses on lightweight verification (pattern matching, monitoring) in the presence of uncertainty.

Configuring timing parameters to ensure opacity

Abstract: Timing information leakage occurs whenever an attacker successfully deduces confidential internal information. In this presentation, we consider that the attacker has access (only) to the system execution time. First, we address the following execution-time opacity problem: given a timed system modeled by a timed automaton, a secrete location and a final location, synthesize the execution times from the initial location to the final location for which one cannot deduce whether the system went through the secrete location. We also consider the full execution-time opacity problem, asking whether the system is opaque for all execution times; that is, for each execution time, either the final location is not reachable, or it is reachable for both a run visiting and a run not visiting the secrete location. Second, we add timing parameters, which are a way to configure a system: we identify a subclass of parametric timed automata with some decidability results. In addition, we devise a semi-algorithm for synthesizing timing parameter valuations guaranteeing that the resulting system is opaque. We finally show that our method can also apply to program analysis with configurable internal timings.

This presentation relies on joint works with Didier Lime, Dylan Marinho and Sun Jun.


Program committee

Chairs

Members


Sven Apel
Sven Apel
Saarland University, Germany
David Basile
David Basile
ISTI-CNR Pisa, Italy
Philipp Chrszon
Philipp Chrszon
German Aerospace Center, Braunschweig, Germany
Erik de Vink
Erik de Vink
Eindhoven University of Technology, The Netherlands
Uli Fahrenberg
Uli Fahrenberg
LIX, Palaiseau, France
Sebastian Junges
Sebastian Junges
Radboud University Nijmegen, The Netherlands
Jan Křetínský
Jan Křetínský
Technical University of Munich, Germany
Axel Legay
Axel Legay
UC Louvain, Belgium
Alberto Lluch Lafuente
Alberto Lluch Lafuente
Technical University of Denmark, Denmark
Tatjana Petrov
Tatjana Petrov
University of Konstanz, Germany
José Proença
José Proença
CISTER Research Centre, Portugal
Genaina Rodrigues
Genaina Rodrigues
University of Brasilia, Brazil
Christoph Seidl
Christoph Seidl
IT University of Copenhagen, Denmark
Thomas Thüm
Thomas Thüm
University of Ulm, Germany
Andrea Vandin
Andrea Vandin
Sant'Anna School of Advanced Studies, Pisa, Italy
Mahsa Varshosaz
Mahsa Varshosaz
IT University of Copenhagen, Denmark