-
Tools at the Frontiers of Quantitative Verification
Authors:
Roman Andriushchenko,
Alexander Bork,
Carlos E. Budde,
Milan Češka,
Kush Grover,
Ernst Moritz Hahn,
Arnd Hartmanns,
Bryant Israelsen,
Nils Jansen,
Joshua Jeppson,
Sebastian Junges,
Maximilian A. Köhl,
Bettina Könighofer,
Jan Křetínský,
Tobias Meggendorfer,
David Parker,
Stefan Pranger,
Tim Quatmann,
Enno Ruijters,
Landon Taylor,
Matthias Volk,
Maximilian Weininger,
Zhen Zhang
Abstract:
The analysis of formal models that include quantitative aspects such as timing or probabilistic choices is performed by quantitative verification tools. Broad and mature tool support is available for computing basic properties such as expected rewards on basic models such as Markov chains. Previous editions of QComp, the comparison of tools for the analysis of quantitative formal models, focused o…
▽ More
The analysis of formal models that include quantitative aspects such as timing or probabilistic choices is performed by quantitative verification tools. Broad and mature tool support is available for computing basic properties such as expected rewards on basic models such as Markov chains. Previous editions of QComp, the comparison of tools for the analysis of quantitative formal models, focused on this setting. Many application scenarios, however, require more advanced property types such as LTL and parameter synthesis queries as well as advanced models like stochastic games and partially observable MDPs. For these, tool support is in its infancy today. This paper presents the outcomes of QComp 2023: a survey of the state of the art in quantitative verification tool support for advanced property types and models. With tools ranging from first research prototypes to well-supported integrations into established toolsets, this report highlights today's active areas and tomorrow's challenges in tool-focused research for quantitative verification.
△ Less
Submitted 22 May, 2024;
originally announced May 2024.
-
RTLola on Board: Testing Real Driving Emissions on your Phone
Authors:
Sebastian Biewer,
Bernd Finkbeiner,
Holger Hermanns,
Maximilian A. Köhl,
Yannik Schnitzer,
Maximilian Schwenger
Abstract:
This paper is about ship** runtime verification to the masses. It presents the crucial technology enabling everyday car owners to monitor the behaviour of their cars in-the-wild. Concretely, we present an Android app that deploys RTLola runtime monitors for the purpose of diagnosing automotive exhaust emissions. For this, it harvests the availability of cheap bluetooth adapters to the On-Board-D…
▽ More
This paper is about ship** runtime verification to the masses. It presents the crucial technology enabling everyday car owners to monitor the behaviour of their cars in-the-wild. Concretely, we present an Android app that deploys RTLola runtime monitors for the purpose of diagnosing automotive exhaust emissions. For this, it harvests the availability of cheap bluetooth adapters to the On-Board-Diagnostics (OBD) ports, which are ubiquitous in cars nowadays. We detail its use in the context of Real Driving Emissions (RDE) tests and report on sample runs that helped identify violations of the regulatory framework currently valid in the European Union.
△ Less
Submitted 9 November, 2021;
originally announced November 2021.
-
An Executable Structural Operational Formal Semantics for Python
Authors:
Maximilian A. Köhl
Abstract:
Python is a popular high-level general-purpose programming language also heavily used by the scientific community. It supports a variety of different programming paradigms and is preferred by many for its ease of use. With the vision of harvesting static analysis techniques like abstract interpretation for Python, we develop a formal semantics for Python. A formal semantics is an important corners…
▽ More
Python is a popular high-level general-purpose programming language also heavily used by the scientific community. It supports a variety of different programming paradigms and is preferred by many for its ease of use. With the vision of harvesting static analysis techniques like abstract interpretation for Python, we develop a formal semantics for Python. A formal semantics is an important cornerstone for any sound static analysis technique. We base our efforts on the general framework of structural operational semantics yielding a small-step semantics in principle allowing for concurrency and interaction with an environment. The main contributions of this thesis are twofold: first, we develop a meta-theoretic framework for the formalization of structural operational semantics in tandem with the necessary tool support for the automated derivation of interpreters from such formal semantics, and, second, we validate the suitability of this approach for the formalization of modern programming languages develo** a semantics for Python.
△ Less
Submitted 7 September, 2021;
originally announced September 2021.
-
Towards a Characterization of Explainable Systems
Authors:
Dimitri Bohlender,
Maximilian A. Köhl
Abstract:
Building software-driven systems that are easily understood becomes a challenge, with their ever-increasing complexity and autonomy. Accordingly, recent research efforts strive to aid in designing explainable systems. Nevertheless, a common notion of what it takes for a system to be explainable is still missing. To address this problem, we propose a characterization of explainable systems that con…
▽ More
Building software-driven systems that are easily understood becomes a challenge, with their ever-increasing complexity and autonomy. Accordingly, recent research efforts strive to aid in designing explainable systems. Nevertheless, a common notion of what it takes for a system to be explainable is still missing. To address this problem, we propose a characterization of explainable systems that consolidates existing research. By providing a unified terminology, we lay a basis for the classification of both existing and future research, and the formulation of precise requirements towards such systems.
△ Less
Submitted 30 January, 2019;
originally announced February 2019.
