Formal verification techniques, such as model checking, can provide valuable insights and guarantees for (safety-critical) devices and their possible behavior. However, these guarantees only hold true as long as the model correctly reflects the system. Automata learning provides a huge advantage there as it enables not only the automatic creation of the needed models but also ensures their correct reflection of the system behavior. However, and this holds especially true for real-time systems, model learning techniques can become very time consuming. To combat this, we show how to integrate given domain knowledge into an existing approach based on genetic programming to speed up the learning process. In particular, we show how the genetic programming approach can take a (possibly abstracted, incomplete or incorrect) untimed skeleton of an automaton, which can often be obtained very cheaply, and augment it with timing behavior to form timed automata in a fast and efficient manner. We demonstrate the approach on several examples of varying sizes.

Testing and verification of reinforcement learning policies are becoming ever more important. One of the open questions for testing such policies is how to determine test adequacy. Neuron activation has been proposed both as a metric for determining test adequacy, as well as for steering the test-case generation. However, recent studies have shown that increasing neuron coverage is not necessarily beneficial and might even be harmful. In this paper, we add an additional take on the evaluation of neuron coverage as a metric. We present different approaches to selecting test cases based on a Markov decision process, which is generated via model learning. We evaluate and compare the efficiency as well as the neuron activation achieved by each of the test suites. The approach is demonstrated on an RL agent playing Super Mario Bros. The results show that an intelligent selection of test cases leads to higher failure detection by the test cases, but does not imply high neuron coverage.

The use of formal methods to prove the correctness of compositional embedded systems is increasingly important. However, the required models and algorithms can induce an enormous complexity. Our approach divides the formal system model into layers and these in turn into modules with defined interfaces, so that reduced formal models can be created for the verification of concrete functional and non-functional requirements. In this work, we use Uppaal to (1) model an RTOS kernel in a modular way and formally specify its internal requirements, (2) model abstract tasks that trigger all kernel functionalities in all combinations or scenarios, and (3) verify the resulting system with regard to task synchronization, resource management, and timing. The result is a fully verified model of the operating system layer that can henceforth serve as a dependable foundation for verifying compositional applications w.r.t. various aspects, such as timing or liveness.

We present a technique for learning explainable timed automata from passive observations of a black-box function, such as an artificial intelligence system. Our method accepts a single, long, timed word with mixed input and output actions and learns a Mealy machine with one timer. The primary advantage of our approach is that it constructs a symbolic observation tree from a concrete timed word. This symbolic tree is then transformed into a human comprehensible automaton. We provide a prototype implementation and evaluate it by learning the controllers of two systems: a brick-sorter conveyor belt trained with reinforcement learning and a real-world derived smart traffic light controller. We compare different model generators using our symbolic observation tree as their input and achieve the best results using k-tails. In our experiments, we learn smaller and simpler automata than existing passive timed learners while maintaining accuracy.

Safe and optimal controller synthesis for switched-controlled hybrid systems, which combine differential equations and discrete changes of the system's state, is known to be intricately hard. Reinforcement learning has been leveraged to construct near-optimal controllers, but their behavior is not guaranteed to be safe, even when it is encouraged by reward engineering. One way of imposing safety to a learned controller is to use a shield, which is correct by design. However, obtaining a shield for non-linear and hybrid environments is itself intractable. In this paper, we propose the construction of a shield using the so-called barbaric method, where an approximate finite representation of an underlying partition-based two-player safety game is extracted via systematically picked samples of the true transition function. While hard safety guarantees are out of reach, we experimentally demonstrate strong statistical safety guarantees with a prototype implementation and UPPAAL STRATEGO. Furthermore, we study the impact of the synthesized shield when applied as either a pre-shield (applied before learning a controller) or a post-shield (only applied after learning a controller). We experimentally demonstrate superiority of the pre-shielding approach. We apply our technique on a range of case studies, including two industrial examples, and further study post-optimization of the post-shielding approach.

A specification theory combines notions of specifications and implementations with a satisfaction relation, a refinement relation and a set of operators supporting stepwise design. We develop a complete specification framework for real-time systems using Timed I/O Automata as the specification formalism, with the semantics expressed in terms of Timed I/O Transition Systems. We provide constructs for refinement, consistency checking, logical and structural composition, and quotient of specifications -- all indispensable ingredients of a compositional design methodology. The theory is backed by rigorous proofs and is being implemented in the open-source tool ECDAR.

Automata learning is a technique for automatically inferring models of existing systems, that enables formal verification of black-box systems. In this paper we propose a way of learning timed automata, extended final state machines that can measure the progress of time. We make use of SMT solving to learn timed automata consistent with the observations in a set of timed traces, which can be gathered via active testing or passive monitoring. By imposing a set of restrictions to the learnt models, we ensure that our solutions are not overly general. The presented SMT encoding of the problem allows for two ways of incremental solving and different search orders. We present a prototype implementation with results from case studies and randomly generated timed automata of varying size and complexity. We perform an extensive evaluation over six SMT solvers, using different theories and exploration strategies, as well as incremental and non-incremental solving.

Erroneous behaviour in safety critical real-time systems may inflict serious consequences. In this paper, we show how to synthesize timed shields from timed safety properties given as timed automata. A timed shield enforces the safety of a running system while interfering with the system as little as possible. We present timed post-shields and timed pre-shields. A timed pre-shield is placed before the system and provides a set of safe outputs. This set restricts the choices of the system. A timed post-shield is implemented after the system. It monitors the system and corrects the system's output only if necessary. We further extend the timed post-shield construction to provide a guarantee on the recovery phase, i.e., the time between a specification violation and the point at which full control can be handed back to the system. In our experimental results, we use timed post-shields to ensure the safety in a reinforcement learning setting for controlling a platoon of cars, during the learning and execution phase, and study the effect.

Model-based mutation testing is a fault-based method in the model-based testing area of research. It has been applied to several modeling formalisms, including timed automata. We propose a model transformation termed "diabolic completion" that allows for conformance testing directly in the UPPAAL tool. We have also developed a system to automate most of the process, which include taking a model, and performing diabolic completion, with the additions of allowing creation of mutants, conformance checking using the UPPAAL verification engine, and test case generation. We then set up a case study using a car alarm system model, which has been used several times in this area of research, and compare the efficiency with two existing tools, Ecdar 2.2 and MoMuT::TA, observing a significant speedup.

Reinforcement learning algorithms discover policies that maximize reward. However, these policies generally do not adhere to safety, leaving safety in reinforcement learning (and in artificial intelligence in general) an open research problem. Shield synthesis is a formal approach to synthesize a correct-by-construction reactive system called a shield that enforces safety properties of a running system while interfering with its operation as little as possible. A shield attached to a learning agent guarantees safety during learning and execution phases. In this paper we summarize three types of shields that are synthesized from different specification languages, and discuss their applicability to reinforcement learning. First, we discuss deterministic shields that enforce specifications expressed as linear temporal logic specifications. Second, we discuss the synthesis of probabilistic shields from specifications in probabilistic temporal logic. Third, we discuss how to synthesize timed shields from timed automata specifications. This paper summarizes the application areas, advantages, disadvantages and synthesis approaches for the three types of shields and gives an overview of experimental results.

This report presents the activities of the first working group of the COST Action ArVI, Runtime Verification beyond Monitoring. The report aims to provide an overview of some of the major core aspects involved in Runtime Verification. Runtime Verification is the field of research dedicated to the analysis of system executions. It is often seen as a discipline that studies how a system run satisfies or violates correctness properties. The report exposes a taxonomy of Runtime Verification (RV) presenting the terminology involved with the main concepts of the field. The report also develops the concept of instrumentation, the various ways to instrument systems, and the fundamental role of instrumentation in designing an RV framework. We also discuss how RV interplays with other verification techniques such as model-checking, deductive verification, model learning, testing, and runtime assertion checking. Finally, we propose challenges in monitoring quantitative and statistical data beyond detecting property violation.

Model learning has gained increasing interest in recent years. It derives behavioural models from test data of black-box systems. The main advantage offered by such techniques is that they enable model-based analysis without access to the internals of a system. Applications range from fully automated testing over model checking to system understanding. Current work focuses on learning variations of finite state machines. However, most techniques consider discrete time. In this paper, we present a novel method for learning timed automata, finite state machines extended with real-valued clocks. The learning method generates a model consistent with a set of timed traces collected via testing. This generation is based on genetic programming, a search-based technique for automatic program creation. We evaluate our approach on \(\mathbf {44}\) timed systems, comprised of four systems from the literature (two industrial and two academic) and \(\mathbf {40}\) randomly generated examples.

Railway scheduling is a complex and safety critical problem that has recently attracted attention in the formal verification community. We provide a formal model of railway scheduling as a stochastic timed game and using the tool Uppaal Stratego, we synthesise the most permissive control strategy for operating the lights and points at the railway scenario such that we guarantee system's safety (avoidance of train collisions). Among all such safe strategies, we then select (with the help of reinforcement learning) a concrete strategy that minimizes the time needed to move all trains to their target locations. This optimizes the speed and capacity of a railway system and advances the current state-of-the-art where the optimality criteria were not considered yet. We successfully demonstrate our approach on the models of two Danish railway stations, and discuss the applicability and scalability of our approach.

In this paper we review how the Uppaal Tool Suite served in industrial projects and was both driven and improved by them throughout the last 20 years. We show how the need of industry for model-based validation, performance evaluation and synthesis shaped the tool suite and how the tool suite aided the use cases it was applied in. The paper highlights a number of selected cases, including success stories and pitfalls, and we discuss the important roles of both basic research and industrial projects.

Model-based mutation testing is a fault-based technique for generating effective test suites. Given a formal model of a system and a set of slightly altered variants of the model (mutants), the approach generates a test suite that is able to distinguish the original model from all (non-equivalent) mutants. Generally, this is done via conformance checks between the mutants and the correct specification where witness traces of non-conformance are transformed into test cases. While this procedure generates high-quality test suites, the conformance checks are computationally expensive, resulting in a high test-case generation time. To ensure that the specification is correct, many safety-critical systems are additionally specified via properties, e.g., timed computation tree logic (TCTL) properties. These can be used to verify the specification model via model checking. After this check, the properties are often not used any further. In this paper, we propose to reuse the properties in a combination of model-based mutation testing and the model-checking of properties for real-time systems. That is, we generate a set of mutated models, and check whether they still satisfy the specified properties. In case of a violation, we receive a trace to this violation, which can be transformed into a test case in the same way as in the traditional approach. The advantages of the approach are manifold: the checking of individual small properties is often more efficient than a full conformance check; the resulting test suite is smaller in size and mainly focuses on the safety-critical parts that were specified by the properties; the distribution of the generated test cases gives a very good indication on the quality of the properties; the technique can also be applied to certain kinds of non-functional properties. We apply the technique to an industrial case study of an automated gear controller. It is modeled as a network of timed automata and specified via 46 TCTL properties. We use the tool UPPAAL and its model-checking capabilities to demonstrate the approach.

In this paper we review 20 years of significant industrial application of the Uppaal Tool Suite for model-based validation, performance evaluation and synthesis. The paper will highlight a number of selected cases, and discuss successes and pitfalls in achieving industrial impact as well as tool sustainability in an academic setting.

Model checking of real-time systems has evolved throughout the years. Recently, the model checker Ecdar, using timed I/O automata, was used to perform compositional verification. However, in order to fully integrate model checking of real-time systems into industrial development, we need a productive and reliable way to test if such a system conforms to its corresponding model. Hence, we present an extension of Ecdar that integrates conformance testing into a new IDE that now features modelling, verification, and testing. The new tool uses model-based mutation testing, requiring only the model and the system under test, to locate faults and to prove the absence of certain types of faults. It supports testing using either real-time or simulated time. It parallelises test-case generation and test execution to provide a significant speed-up. We also introduce new mutation operators that improve the ability to detect and locate faults. Finally, we conduct a case study with 140 faulty systems, where Ecdar detects all faults.

Model learning has gained increasing interest in recent years. It derives behavioural models from test data of black-box systems. The main advantage offered by such techniques is that they enable model-based analysis without access to the internals of a system. Applications range from fully automated testing over model checking to system understanding. Current work focuses on learning variations of finite state machines. However, most techniques consider discrete time. In this paper, we present a method for learning timed automata, finite state machines extended with real-valued clocks. The learning method generates a model consistent with a set of timed traces collected by testing. This generation is based on genetic programming, a search-based technique for automatic program creation. We evaluate our approach on 44 timed systems, comprising four systems from the literature and 40 randomly generated examples.

Formalising requirements has the potential to solve problems arising from deficiencies in natural language descriptions. While behavioural requirements are rarely described formally in industry, increasing complexity and new safety standards have renewed the interest in formal specifications. The goal of this paper is to explore how behavioural requirements for embedded systems can be formalised and aligned with verification tasks. Over the course of a 2.5-year project with industry, we modelled existing requirements from a safety-critical automotive software function in several iterations. Taking practical limitations and stakeholder preferences into account, we explored the use of models on different abstraction levels. The final model was used to generate test cases and was evaluated in three interviews with relevant industry practitioners. We conclude that models on a high level of abstraction are most suitable for industrial requirements engineering, especially when they need to be interpreted by other stakeholders.

Model-based testing is a well-known technique for automating the otherwise tedious process of testing. Test cases are automatically created from a formal model, according to some test criterion which determines when the test suite is complete. In model-based mutation testing, the test criterion is defined via faulty models, called mutants, which are used to create test cases that specifically target the modeled faults. To be able to reveal timing related faults, timed automata can be used as the test model. While model-based mutation testing has already been applied to timed automata, we show how to implement the technique more efficiently with the tool Ecdar, which belongs to the well-known UPPAAL tool family. The tool is used to perform an unbounded conformance check between the correct specification and the mutants, based on a notion of timed refinement. If a mutant does not refine the specification, Ecdar creates a strategy for reaching the non-conformance, which can be used as an adaptive test case. We applied the procedure to the timed automata model of a car alarm system, which was used in the previous approach of model-based mutation testing for timed automata, and compare the two approaches based on the results.