Publications
Learning Mealy Machines with One Timer
We present Mealy machines with a single timer (MM1Ts), a class of models that is both sufficiently expressive to describe the real- time behavior of many realistic applications, and can be learned efficiently. We show how learning algorithms for MM1Ts can be obtained via a reduction to the problem of learning Mealy machines. We describe an implementation of an MM1T learner on top of LearnLib, and compare its performance with recent algorithms proposed by Aichernig et al. and An et al. on several realistic benchmarks.
Using Cyber Digital Twins for Automated Automotive Cybersecurity Testing
Cybersecurity testing of automotive systems has become a practical necessity, with the wide adoption of advanced driving assistance functions and vehicular communications. These functionalities require the integration of information and communication technologies that not only allow for a plethora of on-the-fly configuration abilities, but also provide a huge surface for attacks. Theses circumstances have also been recognized by standardization and regulation bodies, making the need for not only proper cybersecurity engineering but also proving the effectiveness of security measures by verification and validation through testing also a formal necessity. In order to keep pace with the rapidly growing demand of neutral-party security testing of vehicular systems, novel approaches are needed. This paper therefore presents a methodology to create and execute cybersecurity test cases on the fly in a black box setting by using pattern matching-based binary analysis and translation mechanisms to formal attack descriptions as well as model-checking techniques. The approach is intended to generate meaningful attack vectors on a system with next-to-zero a priori knowledge.
A Model-Driven Methodology for Automotive Cybersecurity Test Case Generation
Through international regulations (most prominently the latest UNECE regulation) and standards, the already widely perceived higher need for cybersecurity in automotive systems has been recognized and will mandate higher efforts for cybersecurity engineering. T he UNECE also demands the effectiveness of these engineering to be verified and validated through testing. T his requires both a significantly higher rate and more comprehensiveness of cybersecurity testing that is not effectively to cope with using current, predominantly manual, automotive cybersecurity testing techniques. To allow for comprehensive and efficient testing at all stages of the automotive life cycle, including supply chain parts not at band, and to facilitate efficient third party testing, as well as to test under real-world conditions, also methodologies for testing the cybersecurity of vehicular systems as a black box are necessary. T his paper therefore presents a model and attack tree-based approach to (semi-)automate automotive cybersecurity testing, as well as considerations for automatically black box-deriving models for the use in attack modeling.
Vacuity in Synthesis
In reactive synthesis, one begins with a temporal specification 𝜑, and automatically synthesizes a system 𝑀 such that 𝑀 ⊨ 𝜑. As many systems can satisfy a given specification, it is natural to seek ways to force the synthesis tool to synthesize systems that are of a higher quality, in some well-defined sense. In this article we focus on a well-known measure of the way in which a system satisfies its specification, namely vacuity. Our conjecture is that if the synthesized system 𝑀 satisfies 𝜑 non-vacuously, then 𝑀 is likely to be closer to the user’s intent, because it satisfies 𝜑 in a more “meaningful” way. Narrowing the gap between the formal specification and the designer’s intent in this way, automatically, is the topic of this article. Specifically, we propose a bounded synthesis method for achieving this goal. The notion of vacuity as defined in the context of model checking, however, is not necessarily refined enough for the purpose of synthesis. Hence, even when the synthesized system is technically non-vacuous, there are yet more interesting (equivalently, less vacuous) systems, and we would like to be able to synthesize them. To that end, we cope with the problem of synthesizing a system that is as non-vacuous as possible, given that the set of interesting behaviours with respect to a given specification induce a partial order on transition systems. On the theoretical side we show examples of specifications for which there is a single maximal element in the partial order (i.e., the most interesting system), a set of equivalent maximal elements, or a number of incomparable maximal elements. We also show examples of specifications that induce infinite chains of increasingly interesting systems. These results have implications on how non-vacuous the synthesized system can be. We implemented the new procedure in our synthesis tool PARTY. For this purpose we added to it the capability to synthesize a system based on a property which is a conjunction of universal and existential LTL formulas.