Search

This special issue contains six revised and extended versions of tool papers that appeared in the proceedings of TACAS 2021, the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. The issue is dedicated to the realization of algorithms in tools and the studies of the application of these tools for analysing hard- and software systems. [ABSTRACT FROM AUTHOR]

We address the safety verification and synthesis problems for real-time systems. We introduce real-time programs that are made of instructions that can perform assignments to discrete and real-valued variables. They are general enough to capture interesting classes of timed systems such as timed automata, stopwatch automata, time(d) Petri nets and hybrid automata. We propose a semi-algorithm using refinement of trace abstractions to solve both the reachability verification problem and the parameter synthesis problem for real-time programs. All of the algorithms proposed have been implemented and we have conducted a series of experiments, comparing the performance of our new approach to state-of-the-art tools in classical reachability, robustness analysis and parameter synthesis for timed systems. We show that our new method provides solutions to problems which are unsolvable by the current state-of-the-art tools. [ABSTRACT FROM AUTHOR]

Heatpump-based floor-heating systems for domestic heating offer flexibility in energy consumption patterns, which can be utilized for reducing heating costs—in particular when considering hour-based electricity prices. Such flexibility is hard to exploit via classical Model Predictive Control (MPC), and in addition, MPC requires a priori calibration (i.e., model identification) which is often costly and becomes outdated as the dynamics and use of a building change. We solve these shortcomings by combining recent advancements in stochastic model identification and automatic (near-)optimal controller synthesis. Our method suggests an adaptive model-identification using the tool CTSM-R , and an efficient control synthesis based on Q-learning for Euclidean Markov Decision Processes via Uppaal Stratego. This paper investigates three potential control strategy perspectives (i.e., fixed-target, target-band, and setbacks) to achieve energy efficiency in the heating system. To examine the performance of the suggested approaches, we demonstrate our method on an experimental Danish family-house from the OpSys project. The results show that a fixed-target strategy offers up to a 39 % reduction in heating cost while retaining comparable comfort to a standard bang-bang controller. Even better, target-band and setbacks strategies gain up to 46-49 % energy cost savings. Furthermore, we show the flexibility of our method by computing the Pareto-frontier that visualizes the cost/comfort tradeoff. Additionally, we discuss the applicability of Stratego for an old-fashioned binary-mode heat-pump system and report significant cost savings (33 %) as compared to the bang-bang controller. Moreover, we also present the performance analysis of Stratego against an industry-standard control strategy. [ABSTRACT FROM AUTHOR]

Automatic strategy synthesis for a given control objective can be used to generate correct-by-construction controllers of real-time reactive systems. The existing symbolic approach for continuous timed game is a computationally hard task and current tools like UPPAAL TiGa often scale poorly with the model complexity. We suggest an explicit approach for strategy synthesis in the discrete-time setting and show that even for systems with closed guards, the existence of a safety discrete-time strategy does not imply the existence of a safety continuous-time strategy and vice versa. Nevertheless, we prove that the answers to the existence of discrete-time and continuous-time safety strategies coincide on a practically motivated subclass of urgent controllers that either react immediately after receiving an environmental input or wait with the decision until a next event is triggered by the environment. We then develop an on-the-fly synthesis algorithm for discrete timed-arc Petri net games. The algorithm is implemented in our tool TAPAAL, and based on the experimental evidence, we discuss the advantages of our approach compared to the symbolic continuous-time techniques. [ABSTRACT FROM AUTHOR]

Increasing the penetration of Renewable Energy Sources (RES), e.g. wind and solar, intermittency and volatility of the supply-side are increasing in power systems worldwide. Therefore, the power systems need alternative forms of flexibility potentials to hedge against the intermittent power. District Heating Systems (DHS), especially Heat Pump Systems (HPS), show true potentials to provide demand-side flexibility for power systems. This paper aims to survey the literature on the applications of DHS in power system flexibility. In this way, first of all, the basic structure of the DHS, including the heat resources, thermal units, and thermal storage, is surveyed to give insight into the DHS problem. Afterward, classifying flexibility potentials of the DHS, the conventional and advanced control strategies of the DHS are reviewed comprehensively to investigate the role of heat controllers on power system flexibility. To study the compatibility of the controllers to flexible energy markets, the roles of different control schemes in successive trading floors of the electricity markets, from the energy market to ancillary service markets, are investigated. Finally, the optimization solutions, including mathematical and heuristic approaches, with software tools are reviewed to give readers general insight into the way a DHS problem is modeled and solved. • Review of flexibility potentials of district heating in uncertain electricity markets. • Classification of heat controllers based on flexibility requirements of supply-side. • Hierarchical integration of flexibility potentials of district heating systems. • Focus on software tools to unlock heat flexibility of district heating systems. • Applications of the flexibility of thermal inertia of building, heat carriers, and heat storage. [ABSTRACT FROM AUTHOR]

The Attack Defense Tree framework was developed to facilitate abstract reasoning about security issues of complex systems. As such, a zoo of techniques and extensions have emerged in an attempt to extend the simple Boolean logic of Attack Defense Trees with behavioral properties and quantities. In this paper we expand the modeling power of Attack Defense Trees by introducing a notion of temporal dependencies between attacks, forcing specific ordering of event in successful attacks. Importantly, we introduce a notion of policy for the defender, facilitating a pseudo-active defender, mechanically reacting to the choices of an attacker. To easen the use of Attack Defense Trees we introduce a domain specific language (DSL) and an accompanying tool. The introduction of the DSL facilitates reuse, modularity, collaborative tree construction and separation of logical properties and quantitative/behavioral elements. The usefulness of our framework is exhibited on a small running example, utilizing the policy-notion to implement a reactive Break The Glass policy. We note that all the implemented analysis techniques use well established tools from the formal methods community to produce the given results, relying on non-trivial and automatic translation to and from the target formalisms. Lastly we present our Open Source prototype-tool, capable of conducting various analysis and visualizing the results. [ABSTRACT FROM AUTHOR]