Behaviour driven formal model development (BDFMD) enables domain engineers to influence and validate mathematically precise and verified specifications. In previous work we proposed a process where manually authored scenarios are used initially to support the requirements and help the modeller. The same scenarios are used to verify behavioural properties of the model. The model is then mutated to automatically generate scenarios that have a more complete coverage than the manual ones. These automatically generated scenarios are used to animate the model in a final acceptance stage. In this paper, we discuss lessons learned from applying this BDFMD process to a real-life specification: The European Train Control Systems (ETCS) Hybrid Level 3. During the case study, we have developed our understanding of the process, modifying the way we do some stages and developing improved tool support to make the process more efficient. We discuss (1) the need for abstract scenarios during incremental model development and verification, (2) tools and techniques developed to make the running of scenarios more efficient, and (3) improvements to tools that generate new test cases to improve coverage.

Abstract We present a new method for model-based mutation-driven test case generation. Mutants are generated by making small syntactical modifications to the model or source code of the system under test. A test case kills a mutant if the behavior of the mutant deviates from the original system when running the test. In this work, we use hyperproperties—which allow to express relations between multiple executions—to formalize different notions ofkillingfor both deterministic as well as non-deterministic models. The resulting hyperproperties are universal in the sense that they apply to arbitrary reactive models and mutants. Moreover, an off-the-shelf model checking tool for hyperproperties can be used to generate test cases. Furthermore, we propose solutions to overcome the limitations of current model checking tools via a model transformation and a bounded SMT encoding. We evaluate our approach on a number of models expressed in two different modeling languages by generating tests using a state-of-the-art mutation testing tool.

Automated reasoning tools for the verification and synthesis of software often produce proofs to allow independent certification of the correctness of the produced solutions. As proofs can be large, this paper considers the problem of compressing proofs with respect to their space , which is approximately proportional to the memory necessary to check them. Proof checking with a small amount of available memory is analogous to playing a pebbling game with a small number of pebbles. This paper exploits this analogy and describes novel algorithms for playing a pebbling game . The sequence of moves executed in the pebbling game then corresponds to an improved topological ordering of the nodes of the proof, leading to smaller memory consumption when the proof is checked. Because the number of possible pebbling strategies and topological orderings is too large, brute-force approaches to find optimal solutions are impractical, and hence, the new pebbling algorithms proposed here are based on heuristics for finding good, though not necessarily optimal, solutions. The algorithms are evaluated on the task of compressing the space of thousands of propositional resolution proofs generated by SAT- and SMT-solvers.

This work introduces a heuristic-guided branching search algorithm for model-based, mutation-driven test-case generation. The algorithm is designed towards the efficient and computationally tractable exploration of discrete, non-deterministic models with huge state spaces. Asynchronous parallel processing is a key feature of the algorithm. The algorithm is inspired by the successful path planning algorithm Rapidly exploring Random Trees (RRT). We adapt RRT in several aspects towards test-case generation. Most notably, we introduce parametrized heuristics for start and successor state selection, as well as a mechanism to construct test cases from the data produced during the search. We implemented our algorithm in the existing test-case generation framework MoMuT. We present an extensive evaluation of the proposed heuristics and parameters of the algorithm, based on a diverse set of demanding models obtained in an industrial context. In total, we continuously utilized 128 CPU cores on three servers for several weeks to gather the experimental data presented. We show that branching search works well and the use of multiple heuristics is justified. With our new algorithm, we are now able to process models consisting of over 2,300 concurrent objects. To our knowledge, there is no other mutation-driven test-case generation tool that is able to process models of this magnitude.

This work introduces a heuristic-guided branching search algorithm for model-based, mutation-driven test case generation. The algorithm is designed towards the efficient and computationally tractable exploration of discrete, non-deterministic models with huge state spaces. Asynchronous parallel processing is a key feature of the algorithm. The algorithm is inspired by the successful path planning algorithm Rapidly exploring Random Trees (RRT). We adapt RRT in several aspects towards test case generation. Most notably, we introduce parametrized heuristics for start and successor state selection, as well as a mechanism to construct test cases from the data produced during search.

The efficiency of satisfiability modulo theories (SMT) solvers is dependent on the capability of theory reasoners to provide small conflict sets, i.e. small unsatisfiable subsets from unsatisfiable sets of literals. Decision procedures for uninterpreted symbols (i.e. congruence closure algorithms) date back from the very early days of SMT. Nevertheless, to the best of our knowledge, the complexity of generating smallest conflict sets for sets of literals with uninterpreted symbols and equalities had not yet been determined, although the corresponding decision problem was believed to be NP-complete. We provide here an NP-completeness proof, using a simple reduction from SAT.