Automatic test case generation is a popular software testing strategy. However, many reports show shortage of such test cases in poor quality and doubtable efficiency. In order to alleviate these problems and to make test cases trustable, we propose an interactive post-processing method which allows (1) analyzing the path that is examined by the test case, (2) making safe changes to the path which will eliminate the shortcomings while leaving the coverage targets of the test case unharmed. The method is based on visualization of the path along the control flow graph of the model with additional information about factual evaluation history of all variables and possible alternative variants of behavior. The method reduces the time spent on researching the results of test generation and editing the obtained test cases, and its use has a positive effect on the quality and efficiency of the test suite.

This paper presents a new data flow coverage criterion for a deeper analysis of possible refinements to the constraints on paths unfolding of software program's behavior. Such refinements represent a feasible chain of usages of the same variable without redefinitions in-between. An algorithm for reasonable chains selection is proposed.

In this paper a method for generation of formal models from legacy systems code is proposed. The purpose of these models is to have a possibility of their application in different tasks such as automatic generation of executable tests, translation to modern programming languages, reverse engineering. The method pursues goals to decrease complexity of state space search and checking formulas satisfiability in relation to the direct code modeling, and to help legacy systems understanding and implementing in modern technologies. We focused on formalization of Cobol memory model as it is the most common language in legacy systems. Formal model is an attribute transition system with control flow. We proposed an algorithm for building enumerated types for any variables whose usage fulfills certain conditions, including translation procedure of numeric variables to enumerated ones. We considered a problem of translating non-comparable structures which overlap in memory (operator redefines in Cobol), are copied or compared with each other. In opposite to common approach of using union semantics (like union construction in C++), we described a method of structure fields decomposition which has no drawbacks of unions and makes for minimization of bytewise approach. We considered the developed method on the examples of structures as with simple fields as with arrays. We also gave examples of realization of bytewise approach in Java and C++ languages for those variables that cannot be represented as enumerated or numeric attributes. We tried this work for tests generation for middle-sized projects (up to 100 000 lines of code) where it showed efficiency of developed method, also generated formal models were used for debugging of Cobol to Java translator and business rules extraction.

Data flow-oriented coverage criteria are widely used in software testing. This paper proposes three novel def-use coverage criteria. The main objective of these criteria is to improve the specificity of test goals, to obtain more easily understood test cases, and to strengthen fault detection of derived test suites.

The purpose of the method is to increase the sensitivity of an automatically generated test suite to mutations of a model. Unlike existing methods for generating test scenarios that use the mutational approach to assess the resulting test set, the proposed method analyzes the possibility of detecting mutations on the fly, in the process of analyzing the model’s behavior space, by adding of special coverage goals. Two types of mutants manifestation are considered: deviations in the behavior of paths for (weak case) and in the observed output (strong case). A new algorithm is proposed for efficient search of a path with observable effect of a mutation.

Testing of modernized legacy systems is difficult due to that typically requirements specifications do not exist and that detailed knowledge of the architecture and design of the system may have been lost. In this paper we present an approach which derives test suites for a modernized legacy systems from the legacy code. We extend our earlier presented approach deriving test suites from use case map (UCM) specifications of a system by transforming the legacy code into a UCM model. We further discuss enhancements to the test generation process required to operate on the large models obtained from realistic legacy systems and to assure that the generated tests are meaningful to the tester. This approach has been used to validate the modernization of large (in excess of 20 million lines of code) mainframe applications implemented in COBOL.

This paper focuses on challenges to automatic test suite generation from formal models of software systems. Popular tools and methods and their limitations are discussed. Data cohesion, meaningfulness of derived behavior, usefulness for debugging, coverage evenness, coverage overlap, fault detection ability, and size of the generated test suite are considered as quality indicators for generated tests. A novel composite weight-based heuristic method for improving the quality of automatically generated test scenarios is proposed.

A survey on methods for automatic verificatoin of formal models of software systems is presented. Verifiable properties, methods of reduction and modern verification tools are considered.

We give a short overview of main functionalities and specification language of the VRS system. That environment was succesfully used for formalization and verification of ~30 software development projects implemented in Motorola. The system support both model checking and theorem proving techniques enhanced with invariants generation.