All software developers dream of the times when computers will write programs for them, or, if it is not possible, that computers will at least help them in this hard task. The goal in the “Programming technologies” research direction of the Computer Technologies Laboratory is to create SBSE methods that would allow to automate the processes of software design, development, testing and verification.
Constructing control programs from their specification
Control software systems have complex behavior – they can produce different control actions in response to the same input events depending on the history of interaction - it is advisable to use state-based models for design and analysis of such systems. The most well-known deterministic state-based model is a finite-state machine. The programming paradigm in which control program logic is expressed in the form of interacting finite-state machines is known as automata-based programming. Since designing control software systems, including systems based on finite-state machines, is an extremely complex and time-consuming process, automated finite-state model inference methods are being actively developed.
Finite-state model construction problems can often be reduced to optimization problems. In most cases such problems cannot be solved with traditional optimization methods since the search space, which is the set of all possible finite-state machines, is not a continuous one. Furthermore, these optimization problems are often at least NP-hard, therefore the most widely used solution methods include various metaheuristic algorithms and propositional encoding in SAT and CSP languages.
Fig. 1 shows a barrel roll performed by an autopilot model based on a finite-state machine. The finite-state machine itself is situated on the right-hand side of the figure. This finite-state machine was constructed using ant colony optimization from trajectories of several flights performed by people using a flight simulator.
Fig. 1 Autopilot model based on a finite-state machine
Finite-state models are widely applied for control system development. For example, in the industrial standard IEC 61499 control programs are implemented in the form of networks of interconnected function blocks (Fig. 2); basic function blocks consists of finite-state machines (Fig. 3). One the the research directions involves automatic generation of finite-state models of function blocks based on behavior examples and temporal specification.
Fig. 2. A fragment of a function block network
Fig. 3. Underlying finite-state machine of a basic function block
In the framework of the program “Research and development for priority areas of the development of scientific and technological complex of Russia for 2014-2020” research is being conducted on the topics of design, verification and testing of cyber-physical systems. In particular, methods for generating a formal model of the plant based on its simulation model are being developed (Fig. 4). These methods are aimed at increasing the reliability of cyber-physical systems by using closed-loop formal verification.
Fig. 4. Plant model generation from its simulation model
Test generation using evolutionary algorithms
Testing is one of the most resource-consuming stages of software development – experts estimate it takes up to 50 % of time and more than 50 % of software development cost.
Research in the “Programming technologies” direction aims to solve one of the problems that arise in testing – finding test data that maximizes the runtime of tested software. Genetic algorithms are used to generate such tests.
Aside from software development such tests are needed in education – for organizing contests on olympiad programming. Furthermore, these test generation methods are applicable for automated software optimization. This is done by coevolving programs and tests, which leads to emergence of faster versions of the original program.
Experimental evaluation of methods under development is performed on generating tests for programming contests. Plots on Fig. 5 illustrate test generation against max-flow algorithms.
Fig. 5. Plots illustrate test generation against max-flow algorithms.