We present a survey of the recent research efforts in integrating model learning with model-based testing. We distinguished two strands of work in this domain, namely test-based learning (also called test-based modeling) and learning-based testing. We classify the results in terms of their underlying models, their test purpose and techniques, and their target domains. © Springer International Publishing AG

This paper is an experience report of team Halmstad from the participation in a competition organised by the i-GAME project, the Grand Cooperative Driving Challenge 2016. The competition was held in Helmond, The Netherlands, during the last weekend of May 2016. We give an overview of our car’s control and communication system that was developed for the competition following the requirements and specifications of the i-GAME project. In particular, we describe our implementation of cooperative adaptive cruise control, our solution to the communication and logging requirements, as well as the high level decision making support. For the actual competition we did not manage to completely reach all of the goals set out by the organizers as well as ourselves. However, this did not prevent us from outperforming the competition. Moreover, the competition allowed us to collect data for further evaluation of our solutions to cooperative driving. Thus, we discuss what we believe were the strong points of our system, and discuss post-competition evaluation of the developments that were not fully integrated into our system during competition time. © 2000-2011 IEEE.

Search and rescue with an autonomous robot is an attractive and challenging task within the research community. This paper presents the development of an autonomous hexacopter that is designed for retrieving a lost object, like a drone, from a vast-open space, like a desert area. Navigating its path with a proposed coverage path planning strategy, the hexacopter can efficiently search for a lost target and locate it using an image-based object detection algorithm. Moreover, after the target is located, our hexacopter can grasp it with a customised gripper and transport it back to a destined location. It is also capable of avoiding static obstacles and dynamic objects. The proposed system was realised in simulations before implementing it in a real hardware setup, i.e. assembly of the drone, crafting of the gripper, software implementation and testing under real-world scenarios. The designed hexacopter won the best UAV design award at the CPS-VO 2018 Competition held in Arizona, USA.

Automatic generation of random test inputs is an approach that can alleviate the challenges of manual test case design. However, random test cases may be ineffective in fault detection and increase testing cost, especially in systems where test execution is resource- and time-consuming. To remedy this, the domain knowledge of test engineers can be exploited to select potentially effective test cases. To this end, test selection constraints suggested by domain experts can be utilized either for filtering randomly generated test inputs or for direct generation of inputs using constraint solvers. In this article, we propose a domain specific language (DSL) for formalizing locality-based test selection constraints of autonomous agents and discuss the impact of test selection filters, specified in our DSL, on randomly generated test cases. We study and compare the performance of filtering and constraint solving approaches in generating selective test cases for different test scenario parameters and discuss the role of these parameters in test generation performance. Through our study, we provide criteria for suitability of the random data filtering approach versus the constraint solving one under the varying size and complexity of our testing problem. We formulate the corresponding research questions and answer them by designing and conducting experiments using QuickCheck for random test data generation with filtering and Z3 for constraint solving. Our observations and statistical analysis indicate that applying filters can significantly improve test efficiency of randomly generated test cases. Furthermore, we observe that test scenario parameters affect the performance of the filtering and constraint solving approaches differently. In particular, our results indicate that the two approaches have complementary strengths: random generation and filteringworks best for large agent numbers and long paths, while its performance degrades in the larger grid sizes and more strict constraints. On the contrary, constraint solving has a robust performance for large grid sizes and strict constraints, while its performance degrades with more agents and long paths. © 2023 Copyright held by the owner/author(s).

The automatic generation of random test inputs offers a potential solution to the challenges associated with manual test case design. However, the use of random test cases may prove ineffective for fault detection and can escalate testing costs, particularly in systems where test execution demands significant resources and time. To address this issue, leveraging the domain knowledge of test engineers becomes crucial for selecting test cases with the potential for effectiveness. One approach involves utilizing test selection constraints recommended by domain experts, which can be applied to generate targeted test inputs. In our previous paper, we introduced a domain-specific language (DSL) designed to formalize locality-based test selection constraints specifically tailored for autonomous agents. In this work, we devise an extended DSL for specifying more detailed test scenarios for a more elaborate model of autonomous agents and environment. We design a questionnaire and ask several experts' opinions about the usefulness of the DSL and also design an experiment to compare the efficiency, in terms of time needed to reach a failure, of the extended DSL with the initially proposed one. The questionnaire results show that some features of the extended DSL look useful in the experts' opinion, and the experiment results show that testing with the extended DSL can considerably improve the efficiency of the testing process.

Automated random testing is useful in finding faulty corner cases that are difficult to find by using manually-defined fixed test suites. However, random test inputs can be inefficient in finding faults, particularly in systems where test execution is time- and resource-consuming. Hence, filtering out less-effective test cases by applying domain knowledge constraints can contribute to test effectiveness and efficiency. In this paper, we provide a domain specific language (DSL) for formalising locality-based test selection constraints for autonomous agents. We use this DSL for filtering randomly generated test inputs. To evaluate our approach, we use a simple case study of autonomous agents and evaluate our approach using the QuickCheck tool. The results of our experiments show that using domain knowledge and applying test selection filters significantly reduce the required number of potentially expensive test executions to discover still existing faults. We have also identified the need for applying filters earlier during the test data generation. This observation shows the need to make a more formal connection between the data generation and the DSL-based filtering, which will be addressed in future work. © 2022, IFIP International Federation for Information Processing.

VerifyThis is a series of competitions that aims to evaluatethe current state of deductive tools to prove functional correctness of programs. Such proofs typically require human creativity, and hence iti s not possible to measure the performance of tools independently of the skills of its user. Similarly, solutions can be judged by humans only. Inthis paper, we discuss the role of the human in the competition setup and explore possible future changes to the current format. Regarding the impact of VerifyThis on deductive verification research, a survey conducted among the previous participants shows that the event is a key enabler for gaining insight into other approaches, and that it fosters collaboration and exchange. © 2019, The Author(s).

In this chapter, concepts already addressed in previous chapters are reconsidered and extended to cater for modularity. In particular, it is shown how method contracts can be used in proofs (as opposed to being verified themselves). Another central topic is nonfunctional framing information, i.e., information on what locations a method may write to or read from. But, there are also items that are discussed here in depth for the first time: model methods, an abstraction of Java methods that are only used in specification, verification of recursive methods, and object invariants. For any of the arising proof obligations the calculus rules needed to dispatch them are shown. © Springer International Publishing AG 2016.

VerifyThis 2017 was a two-day program verification competition which took place from April 22-23rd, 2017 in Uppsala, Sweden as part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2017). It was the sixth instalment in the VerifyThis competition series. This article provides an overview of the VerifyThis 2017 event, the challenges that were posed during the competition, and a high-level overview of the solutions to these challenges. It concludes with the results of the competition.

In the context of the AUTO-CAAS project that deals with model-based testing techniques applied in the automotive domain, we present the preliminary ideas and results of building generalised failure models for non-conformant software components. These models are a necessary building block for our upcoming efforts to detect and analyse failure causes in automotive software built with AUTOSAR components. Concretely, we discuss how to build these generalised failure models using automata learning techniques applied to a guided model-based testing procedure of a failing component. We illustrate our preliminary findings and experiments on a simple integer queue implemented in the C programming language. © 2016 IEEE.

In this paper we discuss a verification method for concurrent Java programs based on the concept of dynamic frames. We build on our earlier work that proposes a new, symbolic permission system for concurrent reasoning and we provide the following new contributions. First, we describe our approach for proving program specifications to be self-framed w.r.t. permissions, which is a necessary condition to maintain soundness in concurrent reasoning. Second, we show how we use predicates to provide modular and reusable specifications for program synchronisation points, like locks or forked threads. Our work primarily targets the KeY verification system with its specification language JML* and symbolic execution proving method. Hence, we also give the current status of the work on implementation and we discuss some examples that are verifiable with KeY. © Springer International Publishing Switzerland 2016

In our earlier work we presented a method for formal verification of concurrent Java programs based on Dynamic Logic and symbolic permissions. Embedded within the explicit dynamic frames method realised through JML⁎ specifications, permissions to heap locations and the actual heap location values are tracked separately and require two independent and often overlapping frame specifications. This is in contrast to well established Separation Logic and sibling frameworks, where program frames are inferred from permission annotations that already provide implicit framing information.

In this paper we show how to avoid redundant frame specifications and move towards the implicit framing approach in our method. We strive to keep as much as possible of the existing reasoning framework to preserve the general verification philosophy and implementation of our verification tool, the KeY verifier. We achieve our goal by only a small alteration of the existing proof obligation generation without changing any core part of the underlying logic, in particular, we maintain its closed character. However, even though specifications become more natural and less redundant, the indirect character of the specifications introduces a clear performance penalty for the verification engine.

We then proceed to a brief discussion why, under our minimal approach assumptions, this extension is still not sufficient to translate Separation Logic specifications into our framework. © 2020, Springer Nature Switzerland AG.

This short paper discusses a handful of perhaps obvious, but important observations about KeY, the state-of-the-art deductive verification tool for Java programs. Two light research ideas surface out during the admittedly divergent discussion, both of which seem to be little explored, at least in the given context. Not all projects survive for as long as KeY does, it takes a good idea and dedicated people for that to happen. Hence, the paper also contributes with a formally proved correspondence between using KeY and being a good researcher. Apart from that, considering the occasion to which this paper is dedicated, a handful of memories about Prof. Hähnle are also shared. © 2022, Springer Nature Switzerland AG.

Motivated by applications in the automotive domain, particularly the Autosar basic software standard, we present a technique to improve model-based testing by allowing model-level fault injections. These models are plugged into a larger system as executable components to test it for general tolerance to slightly varying, possibly faulty components or library implementations. Such model execution is possible through applying an automated mocking mechanism and model cross-referencing. Systematic modelling and testing is possible by having comprehensive fault models which both simulate faults and guide the model-based testing procedure towards quicker discovery of these faults. We show the principles of our method on an illustrative example and discuss how it is implemented in a commercial model-based testing tool QuickCheck and applied to a more realistic case study. More generally, this work explores multi-purpose (or meta) modelling – an approach where one parametric model is used for different test targets, like functional testing or safety testing.

This chapter presents the extension of KeY and JavaDL to handle a particular and peculiar dialect of Java, namely Java Card, for programming smart cards. The necessary extensions to the logic and the specification language are discussed, followed by a number of small case studies. The chapter is concluded with applications of the ideas presented here to on-going and future research, in particular in reasoning about concurrent Java programs. © Springer International Publishing AG 2016

We demonstrate a specific method and technology for model-based testing of large software projects with the QuickCheck tool using property-based specifications. Our specifications are very precise, state-full models of the software under test (SUT). In our approach we define (a) formal descriptions of valid function call sequences (public API), (b) postconditions that check the validity of each call, and (c) call-out specifications that define and validate external system interactions (SUT calling external API). The QuickCheck tool automatically generates and executes tests from these specifications. Commercially, this method and tool have been used to test large parts of the industrially developed automotive libraries based on the Autosar standard. In this paper, we exemplify our approach with a circular buffer specified by Autosar, to demonstrate the capabilities of the model-based testing method of QuickCheck. Our example is small compared to the commercial QuickCheck models, but faithfully addresses many of the same challenges. © W. Mostowski, T. Arts, J. Hughes.

Dynamic method dispatch is a core feature of object-oriented programming by which the executed implementation for a polymorphic method is only chosen at runtime. In this paper, we present a specification and verification methodology which extends the concept of dynamic dispatch to design-by-contract specifications.

The formal specification language JML has only rudimentary means for polymorphic abstraction in expressions. We promote these to fully flexible specification-only query methods called model methods that can, like ordinary methods, be overridden to give specifications a new semantics in subclasses in a transparent and modular fashion. Moreover, we allow them to refer to more than one program state which give us the possibility to fully abstract and encapsulate two-state specification contexts, i.e., history constraints and method postconditions. Finally, we provide an elegant and flexible mechanism to specify restrictions on specifications in subtypes. Thus behavioural subtyping can be enforced, yet it still allows for other specification paradigms.

We provide the semantics for model methods by giving a translation into a first order logic and according proof obligations. We fully implemented this framework in the KeY program verifier and successfully verified relevant examples. We have also implemented an extension to KeY to support permission-based verification of concurrent Java programs. In this context model methods provide a modular specification method to treat code synchronisation through API methods. © The Author(s) 2016.

Autonomous vehicles (AVs) are crucial robotic systems that promise to improve our lives via safe, efficient, and inclusive transport-while posing some new challenges for the education of future researchers in the area, that our current research and education might not be ready to deal with: In particular, we don't know what the AVs of the future will look like, practical learning is restricted due to cost and safety concerns, and a high degree of multidisciplinary knowledge is required. Here, following the broad outline of Active Student Participation theory, we propose a pedagogical approach targeted toward AVs called CAR that combines Creativity theory, Applied demo-oriented learning, and Real world research context. Furthermore, we report on applying the approach to stimulate learning and engagement in a master's course, in which students freely created a demo with 10 small robots running ROS2 and Ubuntu on Raspberry Pis, in connection to an ongoing research project and a real current problem (SafeSmart and COVID-19). The results suggested the feasibility of the CAR approach for enabling learning, as well as mutual benefits for both the students and researchers involved, and indicated some possibilities for future improvement, toward more effective integration of research experiences into second cycle courses. © 2021 IEEE.