Search

Providing efficient theorem proving support for general ASM rules that update proper functions, use sequential and parallel composition, nondeterministic choice and recursion is difficult, since it is not easy to find a predicate logic formula that describes the transition relation of an ASM rule. One important obstacle to achieving this goal is that executing rules may result in a clash, that aborts the ASM run. This paper contributes three results towards this goal. First, it shows that it is possible to compute a first-order formula for each rule that implies clash-freedom when provable. The derived formula is not a precise characterization, but is provable for many ASMs that are used in practice. Second, we give axioms that describe the transition relation for clash-free ASM rules as formulas of predicate logic that can be used to verify pre/post-condition assertions using automated theorem provers. Third, we show that the relational encoding can be used to justify a calculus for clash-free ASM rules based on symbolic execution. Such a calculus is useful for interactive theorem provers such as our tool KIV.

Automatic test input generation (ATG) is a major topic in software engineering, analysis and security. In this paper, we bridge the gap between state-of-the-art white-box ATG techniques, especially Dynamic Symbolic Execution, and the diversity of test objectives that they may be used to cover in practice, including many of those defined by common source-code coverage criteria. We define a new coverage specification mechanism, called labels, for specifying test objectives, and prove it to be both expressive and amenable to efficient automation. We present an efficient approach for detecting – revealing – infeasible (i.e. uncoverable) test objectives expressed as labels. We demonstrate that measuring the achieved coverage can be efficiently performed for labels. Finally, we propose an innovative extension of DSE resulting in an efficient support for label coverage, while the existing naive approach induces an exponential blow-up of the search space. Experiments show that our ATG technique yields very significant savings and confirm the interest of infeasible label detection, enabling to lift DSE to label coverage with only a slight overhead. Overall, we show that label coverage provides the basis of a rich framework allowing one to express and handle test objectives from various contexts in an efficient and generic manner. To illustrate this framework, we describe LTest , an all-in-one testing toolset based on labels and used in the industry, which offers automatic program annotation, ATG, coverage measurement and detection of infeasible test objectives.

Programmable logic controllers (PLCs) are essentially domain-specific computers that are widely used in the industrial field. These industrial devices are usually required to be of high reliability, and program bugs can lead to catastrophes. However, there are few automated testing tools for PLC programs. This paper proposes a framework, named STAutoTester, for automatically generating test cases for IEC 61131-3 Structured Text (ST) programs. It adopts Dynamic Symbol Execution (DSE) combined with redundant path pruning to efficiently perform PLC multi-cycle test data generation under different coverage criteria. We have evaluated STAutoTester on 21 programs. The experimental results show that STAutoTester can effectively handle these programs. Compared to S Y M PLC, a previous symbolic execution based tool for automatically testing PLC software, we achieved comparable statement coverage with much fewer test cases. Besides, we have achieved greater branch coverage and stricter MC/DC coverage, which were not implemented by S Y M PLC.

Concolic testing is a software testing technique that simultaneously combines concrete execution of a program (given specific input, along specific paths) with symbolic execution (generating new test inputs that explore other paths, which gives better path coverage than random test case generation). So far, concolic testing has been applied, mainly at the level of bytecode or assembly code, to programs written in imperative languages that manipulate primitive data types such as integers and arrays. In this article, we demonstrate its application to a functional programming language core, the functional subset of Core Erlang, that supports pattern matching, structured recursive data types such as lists, recursion and higher-order functions. We present CutEr, a tool implementing this testing technique, and describe its architecture, the challenges that it needs to address, its current limitations, and report some experiences from its use.

Classic approaches to automatic input data generation are usually driven by the goal of obtaining program coverage and the need to solve or find solutions to path constraints to achieve this. As inputs are generated with respect to the structure of the code, they can be ineffective, difficult for humans to read, and unsuitable for testing missing implementation. Furthermore, these approaches have known limitations when handling constraints that involve operations with string data types.This paper presents a novel approach for generating string test data for string validation routines, by harnessing the Internet. The technique uses program identifiers to construct web search queries for regular expressions that validate the format of a string type (such as an email address). It then performs further web searches for strings that match the regular expressions, producing examples of test cases that are both valid and realistic. Following this, our technique mutates the regular expressions to drive the search for invalid strings, and the production of test inputs that should be rejected by the validation routine.The paper presents the results of an empirical study evaluating our approach. The study was conducted on 24 string input validation routines collected from 10 open source projects. While dynamic symbolic execution and search-based testing approaches were only able to generate a very low number of values successfully, our approach generated values with an accuracy of 34% on average for the case of valid strings, and 99% on average for the case of invalid strings. Furthermore, whereas dynamic symbolic execution and search-based testing approaches were only capable of detecting faults in 8 routines, our approach detected faults in 17 out of the 19 validation routines known to contain implementation errors. An approach for finding valid values for string data types on the Internet.A mutation algorithm for regular expressions to produce invalid values for string data types.A testing procedure to identify program errors using the valid and invalid values.An empirical study of the approach on 24 open source case studies.An analysis of the approach against two contemporary test data generation tools.

We present a semantics, calculus, and system for compositional verification of Creol, an object-oriented modelling language for concurrent distributed applications. The system is an instance of KeY, a framework for object-oriented software verification, which has so far been applied foremost to sequential Java. Building on KeY characteristic concepts, like dynamic logic, sequent calculus, symbolic execution via explicit substitutions, and the taclet rule language, the presented system addresses functional correctness of Creol models featuring local cooperative thread parallelism and global communication via asynchronous method calls. The calculus heavily operates on communication histories specified by the interfaces of Creol units. Two example scenarios demonstrate the usage of the system. This article extends the conference paper of Ahrendt and Dylla (2009) [5] with a denotational semantics of Creol and an assumption-commitment style semantics of the logic.