Danny Weyns

SE
h-index9
21papers
790citations
Novelty31%
AI Score35

21 Papers

SEApr 4, 2022
Lifelong Self-Adaptation: Self-Adaptation Meets Lifelong Machine Learning

Omid Gheibi, Danny Weyns

In the past years, machine learning (ML) has become a popular approach to support self-adaptation. While ML techniques enable dealing with several problems in self-adaptation, such as scalable decision-making, they are also subject to inherent challenges. In this paper, we focus on one such challenge that is particularly important for self-adaptation: ML techniques are designed to deal with a set of predefined tasks associated with an operational domain; they have problems to deal with new emerging tasks, such as concept shift in input data that is used for learning. To tackle this challenge, we present \textit{lifelong self-adaptation}: a novel approach to self-adaptation that enhances self-adaptive systems that use ML techniques with a lifelong ML layer. The lifelong ML layer tracks the running system and its environment, associates this knowledge with the current tasks, identifies new tasks based on differentiations, and updates the learning models of the self-adaptive system accordingly. We present a reusable architecture for lifelong self-adaptation and apply it to the case of concept drift caused by unforeseen changes of the input data of a learning model that is used for decision-making in self-adaptation. We validate lifelong self-adaptation for two types of concept drift using two cases.

SEApr 13, 2022
Deep Learning for Effective and Efficient Reduction of Large Adaptation Spaces in Self-Adaptive Systems

Danny Weyns, Omid Gheibi, Federico Quin et al.

Many software systems today face uncertain operating conditions, such as sudden changes in the availability of resources or unexpected user behavior. Without proper mitigation these uncertainties can jeopardize the system goals. Self-adaptation is a common approach to tackle such uncertainties. When the system goals may be compromised, the self-adaptive system has to select the best adaptation option to reconfigure by analyzing the possible adaptation options, i.e., the adaptation space. Yet, analyzing large adaptation spaces using rigorous methods can be resource- and time-consuming, or even be infeasible. One approach to tackle this problem is by using online machine learning to reduce adaptation spaces. However, existing approaches require domain expertise to perform feature engineering to define the learner, and support online adaptation space reduction only for specific goals. To tackle these limitations, we present 'Deep Learning for Adaptation Space Reduction Plus' -- DLASeR+ in short. DLASeR+ offers an extendable learning framework for online adaptation space reduction that does not require feature engineering, while supporting three common types of adaptation goals: threshold, optimization, and set-point goals. We evaluate DLASeR+ on two instances of an Internet-of-Things application with increasing sizes of adaptation spaces for different combinations of adaptation goals. We compare DLASeR+ with a baseline that applies exhaustive analysis and two state-of-the-art approaches for adaptation space reduction that rely on learning. Results show that DLASeR+ is effective with a negligible effect on the realization of the adaptation goals compared to an exhaustive analysis approach, and supports three common types of adaptation goals beyond the state-of-the-art approaches.

SEApr 14, 2022
The Vision of Self-Evolving Computing Systems

Danny Weyns, Thomas Baeck, Rene Vidal et al.

Computing systems are omnipresent; their sustainability has become crucial for our society. A key aspect of this sustainability is the ability of computing systems to cope with the continuous change they face, ranging from dynamic operating conditions, to changing goals, and technological progress. While we are able to engineer smart computing systems that autonomously deal with various types of changes, handling unanticipated changes requires system evolution, which remains in essence a human-centered process. This will eventually become unmanageable. To break through the status quo, we put forward an arguable opinion for the vision of self-evolving computing systems that are equipped with an evolutionary engine enabling them to evolve autonomously. Specifically, when a self-evolving computing system detects conditions outside its operational domain, such as an anomaly or a new goal, it activates an evolutionary engine that runs online experiments to determine how the system needs to evolve to deal with the changes, thereby evolving its architecture. During this process the engine can integrate new computing elements that are provided by computing warehouses. These computing elements provide specifications and procedures enabling their automatic integration. We motivate the need for self-evolving computing systems in light of the state of the art, outline a conceptual architecture of self-evolving computing systems, and illustrate the architecture for a future smart city mobility system that needs to evolve continuously with changing conditions. To conclude, we highlight key research challenges to realize the vision of self-evolving computing systems.

LGNov 4, 2022
Dealing with Drift of Adaptation Spaces in Learning-based Self-Adaptive Systems using Lifelong Self-Adaptation

Omid Gheibi, Danny Weyns

Recently, machine learning (ML) has become a popular approach to support self-adaptation. ML has been used to deal with several problems in self-adaptation, such as maintaining an up-to-date runtime model under uncertainty and scalable decision-making. Yet, exploiting ML comes with inherent challenges. In this paper, we focus on a particularly important challenge for learning-based self-adaptive systems: drift in adaptation spaces. With adaptation space we refer to the set of adaptation options a self-adaptive system can select from at a given time to adapt based on the estimated quality properties of the adaptation options. Drift of adaptation spaces originates from uncertainties, affecting the quality properties of the adaptation options. Such drift may imply that eventually no adaptation option can satisfy the initial set of the adaptation goals, deteriorating the quality of the system, or adaptation options may emerge that allow enhancing the adaptation goals. In ML, such shift corresponds to novel class appearance, a type of concept drift in target data that common ML techniques have problems dealing with. To tackle this problem, we present a novel approach to self-adaptation that enhances learning-based self-adaptive systems with a lifelong ML layer. We refer to this approach as lifelong self-adaptation. The lifelong ML layer tracks the system and its environment, associates this knowledge with the current tasks, identifies new tasks based on differences, and updates the learning models of the self-adaptive system accordingly. A human stakeholder may be involved to support the learning process and adjust the learning and goal models. We present a general architecture for lifelong self-adaptation and apply it to the case of drift of adaptation spaces that affects the decision-making in self-adaptation. We validate the approach for a series of scenarios using the DeltaIoT exemplar.

SEDec 4, 2025
Generative AI for Self-Adaptive Systems: State of the Art and Research Roadmap

Jialong Li, Mingyue Zhang, Nianyu Li et al.

Self-adaptive systems (SASs) are designed to handle changes and uncertainties through a feedback loop with four core functionalities: monitoring, analyzing, planning, and execution. Recently, generative artificial intelligence (GenAI), especially the area of large language models, has shown impressive performance in data comprehension and logical reasoning. These capabilities are highly aligned with the functionalities required in SASs, suggesting a strong potential to employ GenAI to enhance SASs. However, the specific benefits and challenges of employing GenAI in SASs remain unclear. Yet, providing a comprehensive understanding of these benefits and challenges is complex due to several reasons: limited publications in the SAS field, the technological and application diversity within SASs, and the rapid evolution of GenAI technologies. To that end, this paper aims to provide researchers and practitioners a comprehensive snapshot that outlines the potential benefits and challenges of employing GenAI's within SAS. Specifically, we gather, filter, and analyze literature from four distinct research fields and organize them into two main categories to potential benefits: (i) enhancements to the autonomy of SASs centered around the specific functions of the MAPE-K feedback loop, and (ii) improvements in the interaction between humans and SASs within human-on-the-loop settings. From our study, we outline a research roadmap that highlights the challenges of integrating GenAI into SASs. The roadmap starts with outlining key research challenges that need to be tackled to exploit the potential for applying GenAI in the field of SAS. The roadmap concludes with a practical reflection, elaborating on current shortcomings of GenAI and proposing possible mitigation strategies.

LGSep 11, 2023
Online ML Self-adaptation in Face of Traps

Michal Töpfer, František Plášil, Tomáš Bureš et al.

Online machine learning (ML) is often used in self-adaptive systems to strengthen the adaptation mechanism and improve the system utility. Despite such benefits, applying online ML for self-adaptation can be challenging, and not many papers report its limitations. Recently, we experimented with applying online ML for self-adaptation of a smart farming scenario and we had faced several unexpected difficulties -- traps -- that, to our knowledge, are not discussed enough in the community. In this paper, we report our experience with these traps. Specifically, we discuss several traps that relate to the specification and online training of the ML-based estimators, their impact on self-adaptation, and the approach used to evaluate the estimators. Our overview of these traps provides a list of lessons learned, which can serve as guidance for other researchers and practitioners when applying online ML for self-adaptation.

SEDec 12, 2021
Report on A Formally-Founded Model-Based Approach to Engineer Self-Adaptive Systems

Danny Weyns, Usman Iftikhar

Self-adaptive systems manage themselves to deal with uncertainties that can only be resolved during operation. A common approach to realize self-adaptation is by adding a feedback loop to the system that monitors the system and adapts it to realize a set of adaptation goals. ActivFORMS (Active FORmal Models for Self-adaptation) provides an end-to-end approach for engineering self-adaptive systems. ActivFORMS relies on feedback loops that consists of formally verified models that are directly deployed and executed at runtime to realize self-adaptation. At runtime, the approach relies on statistical verification techniques that allow efficient analysis of the possible options for adaptation. Further, ActivFORMS supports on-the-fly changes of adaptation goals and updates of the verified models to to meet the new goals. ActivFORMSi provides a tool-supported instance of ActivFORMS. The approach has been validates using an IoT application for building security monitoring. This report provides complementary material to the paper ``ActivFORMS: A Formally-Founded Model-Based Approach to Engineer Self-Adaptive Systems'' [Weyns and Iftikhar 2019].

SEAug 19, 2021
Lifelong Computing

Danny Weyns, Thomas Bäck, Renè Vidal et al.

Computing systems form the backbone of many aspects of our life, hence they are becoming as vital as water, electricity, and road infrastructures for our society. Yet, engineering long running computing systems that achieve their goals in ever-changing environments pose significant challenges. Currently, we can build computing systems that adjust or learn over time to match changes that were anticipated. However, dealing with unanticipated changes, such as anomalies, novelties, new goals or constraints, requires system evolution, which remains in essence a human-driven activity. Given the growing complexity of computing systems and the vast amount of highly complex data to process, this approach will eventually become unmanageable. To break through the status quo, we put forward a new paradigm for the design and operation of computing systems that we coin "lifelong computing." The paradigm starts from computing-learning systems that integrate computing/service modules and learning modules. Computing warehouses offer such computing elements together with data sheets and usage guides. When detecting anomalies, novelties, new goals or constraints, a lifelong computing system activates an evolutionary self-learning engine that runs online experiments to determine how the computing-learning system needs to evolve to deal with the changes, thereby changing its architecture and integrating new computing elements from computing warehouses as needed. Depending on the domain at hand, some activities of lifelong computing systems can be supported by humans. We motivate the need for lifelong computing with a future fish farming scenario, outline a blueprint architecture for lifelong computing systems, and highlight key research challenges to realise the vision of lifelong computing.

SEAug 18, 2021
Towards Mapping Control Theory and Software Engineering Properties using Specification Patterns

Ricardo Caldas, Razan Ghzouli, Alessandro V. Papadopoulos et al.

A traditional approach to realize self-adaptation in software engineering (SE) is by means of feedback loops. The goals of the system can be specified as formal properties that are verified against models of the system. On the other hand, control theory (CT) provides a well-established foundation for designing feedback loop systems and providing guarantees for essential properties, such as stability, settling time, and steady state error. Currently, it is an open question whether and how traditional SE approaches to self-adaptation consider properties from CT. Answering this question is challenging given the principle differences in representing properties in both fields. In this paper, we take a first step to answer this question. We follow a bottom up approach where we specify a control design (in Simulink) for a case inspired by Scuderia Ferrari (F1) and provide evidence for stability and safety. The design is then transferred into code (in C) that is further optimized. Next, we define properties that enable verifying whether the control properties still hold at code level. Then, we consolidate the solution by mapping the properties in both worlds using specification patterns as common language and we verify the correctness of this mapping. The mapping offers a reusable artifact to solve similar problems. Finally, we outline opportunities for future work, particularly to refine and extend the mapping and investigate how it can improve the engineering of self-adaptive systems for both SE and CT engineers.

SEMar 21, 2021
How do we Evaluate Self-adaptive Software Systems?

Ilias Gerostathopoulos, Thomas Vogel, Danny Weyns et al.

With the increase of research in self-adaptive systems, there is a need to better understand the way research contributions are evaluated. Such insights will support researchers to better compare new findings when developing new knowledge for the community. However, so far there is no clear overview of how evaluations are performed in self-adaptive systems. To address this gap, we conduct a mapping study. The study focuses on experimental evaluations published in the last decade at the prime venue of research in software engineering for self-adaptive systems -- the International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS). Results point out that specifics of self-adaptive systems require special attention in the experimental process, including the distinction of the managing system (i.e., the target of evaluation) and the managed system, the presence of uncertainties that affect the system behavior and hence need to be taken into account in data analysis, and the potential of managed systems to be reused across experiments, beyond replications. To conclude, we offer a set of suggestions derived from our study that can be used as input to enhance future experiments in self-adaptive systems.

SEMar 19, 2021
Towards Better Adaptive Systems by Combining MAPE, Control Theory, and Machine Learning

Danny Weyns, Bradley Schmerl, Masako Kishida et al.

Two established approaches to engineer adaptive systems are architecture-based adaptation that uses a Monitor-Analysis-Planning-Executing (MAPE) loop that reasons over architectural models (aka Knowledge) to make adaptation decisions, and control-based adaptation that relies on principles of control theory (CT) to realize adaptation. Recently, we also observe a rapidly growing interest in applying machine learning (ML) to support different adaptation mechanisms. While MAPE and CT have particular characteristics and strengths to be applied independently, in this paper, we are concerned with the question of how these approaches are related with one another and whether combining them and supporting them with ML can produce better adaptive systems. We motivate the combined use of different adaptation approaches using a scenario of a cloud-based enterprise system and illustrate the analysis when combining the different approaches. To conclude, we offer a set of open questions for further research in this interesting area.

SEMar 18, 2021
On the Impact of Applying Machine Learning in the Decision-Making of Self-Adaptive Systems

Omid Gheibi, Danny Weyns, Federico Quin

Recently, we have been witnessing an increasing use of machine learning methods in self-adaptive systems. Machine learning methods offer a variety of use cases for supporting self-adaptation, e.g., to keep runtime models up to date, reduce large adaptation spaces, or update adaptation rules. Yet, since machine learning methods apply in essence statistical methods, they may have an impact on the decisions made by a self-adaptive system. Given the wide use of formal approaches to provide guarantees for the decisions made by self-adaptive systems, it is important to investigate the impact of applying machine learning methods when such approaches are used. In this paper, we study one particular instance that combines linear regression to reduce the adaptation space of a self-adaptive system with statistical model checking to analyze the resulting adaptation options. We use computational learning theory to determine a theoretical bound on the impact of the machine learning method on the predictions made by the verifier. We illustrate and evaluate the theoretical result using a scenario of the DeltaIoT artifact. To conclude, we look at opportunities for future research in this area.

SEMar 16, 2021
Decentralized Self-Adaptive Systems: A Mapping Study

Federico Quin, Danny Weyns, Omid Gheibi

With the increasing ubiquity and scale of self-adaptive systems, there is a growing need to decentralize the functionality that realizes self-adaptation. Our focus is on architecture-based self-adaptive systems where one or more functions for monitoring, analyzing, planning, and executing are realized by multiple components that coordinate with one another. While some earlier studies have shed light on existing work on the decentralization of self-adaptive systems, there is currently no clear overview of the state of the art in decentralization of self-adaptive systems. Yet, having a precise view on the state of the art in decentralized self-adaptive systems is crucial for researchers to understand existing solutions and drive future research efforts. To address this gap, we conducted a mapping study. The study focused on papers published at 24 important venues that publish research on self-adaptation. The study focused on the motivations for choosing a decentralized approach to realize self-adaptation, the adaptation functions that are decentralized, the realization of the coordination, and the open challenges in the area.

NEMar 6, 2021
Applying Machine Learning in Self-Adaptive Systems: A Systematic Literature Review

Omid Gheibi, Danny Weyns, Federico Quin

Recently, we witness a rapid increase in the use of machine learning in self-adaptive systems. Machine learning has been used for a variety of reasons, ranging from learning a model of the environment of a system during operation to filtering large sets of possible configurations before analysing them. While a body of work on the use of machine learning in self-adaptive systems exists, there is currently no systematic overview of this area. Such overview is important for researchers to understand the state of the art and direct future research efforts. This paper reports the results of a systematic literature review that aims at providing such an overview. We focus on self-adaptive systems that are based on a traditional Monitor-Analyze-Plan-Execute feedback loop (MAPE). The research questions are centred on the problems that motivate the use of machine learning in self-adaptive systems, the key engineering aspects of learning in self-adaptation, and open challenges. The search resulted in 6709 papers, of which 109 were retained for data collection. Analysis of the collected data shows that machine learning is mostly used for updating adaptation rules and policies to improve system qualities, and managing resources to better balance qualities and resources. These problems are primarily solved using supervised and interactive learning with classification, regression and reinforcement learning as the dominant methods. Surprisingly, unsupervised learning that naturally fits automation is only applied in a small number of studies. Key open challenges in this area include the performance of learning, managing the effects of learning, and dealing with more complex types of goals. From the insights derived from this systematic literature review we outline an initial design process for applying machine learning in self-adaptive systems that are based on MAPE feedback loops.

SEMar 3, 2021
Uncertainty in Self-Adaptive Systems: A Research Community Perspective

Sara M. Hezavehi, Danny Weyns, Paris Avgeriou et al.

One of the primary drivers for self-adaptation is ensuring that systems achieve their goals regardless of the uncertainties they face during operation. Nevertheless, the concept of uncertainty in self-adaptive systems is still insufficiently understood. Several taxonomies of uncertainty have been proposed, and a substantial body of work exists on methods to tame uncertainty. Yet, these taxonomies and methods do not fully convey the research community's perception on what constitutes uncertainty in self-adaptive systems and how to tackle it. To understand this perception and learn from it, we conducted a survey comprising two complementary stages. In the first stage, we focused on current research and development. In the second stage, we focused on directions for future research. The key findings of the first stage are: a) an overview of uncertainty sources considered in self-adaptive systems, b) an overview of existing methods used to tackle uncertainty in concrete applications, c) insights into the impact of uncertainty on non-functional requirements, d) insights into different opinions in the perception of uncertainty within the community, and the need for standardised uncertainty-handling processes to facilitate uncertainty management in self-adaptive systems. The key findings of the second stage are: a) the insight that over 70% of the participants believe that self-adaptive systems can be engineered to cope with unanticipated change, b) a set of potential approaches for dealing with unanticipated change, c) a set of open challenges in mitigating uncertainty in self-adaptive systems, in particular in those with safety-critical requirements. From these findings, we outline an initial reference process to manage uncertainty in self-adaptive systems.

SEApr 24, 2020
Towards Bridging the Gap between Control and Self-Adaptive System Properties

Javier Cámara, Alessandro V. Papadopoulos, Thomas Vogel et al.

Two of the main paradigms used to build adaptive software employ different types of properties to capture relevant aspects of the system's run-time behavior. On the one hand, control systems consider properties that concern static aspects like stability, as well as dynamic properties that capture the transient evolution of variables such as settling time. On the other hand, self-adaptive systems consider mostly non-functional properties that capture concerns such as performance, reliability, and cost. In general, it is not easy to reconcile these two types of properties or identify under which conditions they constitute a good fit to provide run-time guarantees. There is a need of identifying the key properties in the areas of control and self-adaptation, as well as of characterizing and mapping them to better understand how they relate and possibly complement each other. In this paper, we take a first step to tackle this problem by: (1) identifying a set of key properties in control theory, (2) illustrating the formalization of some of these properties employing temporal logic languages commonly used to engineer self-adaptive software systems, and (3) illustrating how to map key properties that characterize self-adaptive software systems into control properties, leveraging their formalization in temporal logics. We illustrate the different steps of the mapping on an exemplar case in the cloud computing domain and conclude with identifying open challenges in the area.

MASep 8, 2019
An Architectural Style for Self-Adaptive Multi-Agent Systems

Danny Weyns, Flavio Oquendo

Modern distributed software systems often operate in dynamic environments in which operation conditions change continuously and subsystems may come and go at will, e.g. intelligent traffic management and multi-robot systems. To manage these dynamics, these systems have to self-adapt their structures and behaviors dynamically. While we have witnessed significant progress over the past decade in the manner in which such systems are designed, persistent challenges remain. In particular, dealing with distribution and decentralized control remains one of the major challenges in self-adaptive systems. This report presents an architecture style that supports software architects with designing architectures for a family of decentralized self-adaptive systems. The architecture style structures the software in a number of interacting autonomous entities (agents) that cooperatively realize the system tasks. Multi-agent systems derived from the architectural style realize flexibility (agents adapt their behavior and interactions to variable operating conditions) and openness (agents cope autonomously with other agents that enter and leave the system). The architectural style consists of five related patterns that distill domain-specific architectural knowledge derived from extensive experiences with developing various multi-agent systems. The architectural patterns are specified using pi-ADL, a formal architectural description language supporting specification of dynamic architectures. This specification provides architects with a rigorous description of the architecture elements of the patterns, their interactions and behavior. We illustrate how we have applied the architectural style with excerpts of two cases from our practice: an experimental system for anticipatory traffic routing and an industrial logistic system for automated transportation in warehouse environments.

SEAug 29, 2019
ActivFORMS: A Formally-Founded Model-Based Approach to Engineer Self-Adaptive Systems

Danny Weyns, M. Usman Iftikhar

Self-adaptation equips a computing system with a feedback loop that enables it dealing with change caused by uncertainties during operation, such as changing availability of resources and fluctuating workloads. To ensure that the system complies with the adaptation goals, recent research suggests the use of formal techniques at runtime. Yet, existing approaches have three limitations that affect their practical applicability: (i) they ignore correctness of the behavior of the feedback loop, (ii) they rely on exhaustive verification at runtime to select adaptation options to realize the adaptation goals, which is time and resource demanding, and (iii) they provide limited or no support for changing adaptation goals at runtime. To tackle these shortcomings, we present ActivFORMS (Active FORmal Models for Self-adaptation). ActivFORMS contributes an end-to-end approach for engineering self-adaptive systems, spanning four main stages of the life cycle of a feedback loop: design, deployment, runtime adaptation, and evolution. We also present ActivFORMS-ta, a tool-supported instance of ActivFORMS that leverages timed automata models and statistical model checking at runtime. We validate the research results using an IoT application for building security monitoring that is deployed in Leuven. The experimental results demonstrate that ActivFORMS supports correctness of the behavior of the feedback loop, achieves the adaptation goals in an efficient way, and supports changing adaptation goals at runtime.

SEMar 12, 2019
Perpetual Assurances for Self-Adaptive Systems

Danny Weyns, Nelly Bencomo, Radu Calinescu et al.

Providing assurances for self-adaptive systems is challenging. A primary underlying problem is uncertainty that may stem from a variety of different sources, ranging from incomplete knowledge to sensor noise and uncertain behavior of humans in the loop. Providing assurances that the self-adaptive system complies with its requirements calls for an enduring process spanning the whole lifetime of the system. In this process, humans and the system jointly derive and integrate new evidence and arguments, which we coined perpetual assurances for self-adaptive systems. In this paper, we provide a background framework and the foundation for perpetual assurances for self-adaptive systems. We elaborate on the concrete challenges of offering perpetual assurances, requirements for solutions, realization techniques and mechanisms to make solutions suitable. We also present benchmark criteria to compare solutions. We then present a concrete exemplar that researchers can use to assess and compare approaches for perpetual assurances for self-adaptation.

SEMar 18, 2017
Engineering Trustworthy Self-Adaptive Software with Dynamic Assurance Cases

Radu Calinescu, Danny Weyns, Simos Gerasimou et al.

Building on concepts drawn from control theory, self-adaptive software handles environmental and internal uncertainties by dynamically adjusting its architecture and parameters in response to events such as workload changes and component failures. Self-adaptive software is increasingly expected to meet strict functional and non-functional requirements in applications from areas as diverse as manufacturing, healthcare and finance. To address this need, we introduce a methodology for the systematic ENgineering of TRUstworthy Self-adaptive sofTware (ENTRUST). ENTRUST uses a combination of (1) design-time and runtime modelling and verification, and (2) industry-adopted assurance processes to develop trustworthy self-adaptive software and assurance cases arguing the suitability of the software for its intended application. To evaluate the effectiveness of our methodology, we present a tool-supported instance of ENTRUST and its use to develop proof-of-concept self-adaptive software for embedded and service-based systems from the oceanic monitoring and e-finance domains, respectively. The experimental results show that ENTRUST can be used to engineer self-adaptive software systems in different application domains and to generate dynamic assurance cases for these systems.

SEAug 22, 2012
A Case Study on Formal Verification of Self-Adaptive Behaviors in a Decentralized System

M. Usman Iftikhar, Danny Weyns

Self-adaptation is a promising approach to manage the complexity of modern software systems. A self-adaptive system is able to adapt autonomously to internal dynamics and changing conditions in the environment to achieve particular quality goals. Our particular interest is in decentralized self-adaptive systems, in which central control of adaptation is not an option. One important challenge in self-adaptive systems, in particular those with decentralized control of adaptation, is to provide guarantees about the intended runtime qualities. In this paper, we present a case study in which we use model checking to verify behavioral properties of a decentralized self-adaptive system. Concretely, we contribute with a formalized architecture model of a decentralized traffic monitoring system and prove a number of self-adaptation properties for flexibility and robustness. To model the main processes in the system we use timed automata, and for the specification of the required properties we use timed computation tree logic. We use the Uppaal tool to specify the system and verify the flexibility and robustness properties.