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]

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]

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]