Menu

Publications

Editor-in-Chief

**Nikiforov**

Vladimir O.

D.Sc., Prof.

Vladimir O.

D.Sc., Prof.

Partners

**Summaries of the Issue**

### PARADIGM AUTOMATA PROGRAMMING

AUTOMATA-BASED PROGRAMMING PARADIGM
Shalyto Anatoly Abramovich

3

Automata-based programming and its advantages for software development are described in this paper. Tools for automata-based programming and examples of its successful application are also described. Procedure-based programming and object-oriented programming with explicit state emphasis are described. Automata-based programs can be efficiently verified, for their construction genetic algorithms can be applied.

### BUILDING MACHINES FOR MANAGEMENT UNMANNED DEVICES BASED ON USING GENETIC ALGORITHMS

APPLICATION OF GENETIC PROGRAMMING FOR GENERATION OF AUTOMATA HAVING A LOT OF INPUT VARIABLE
N. Polikarpova, N. Tochilin, Shalyto Anatoly Abramovich

24

Efficiency of the known methods of automatic generation of finite automata based on genetic programming exponentially decreases when number of input variables increases. In this paper presented a method that does not have these deficiencies. Preference for the application of the proposed method with a large number of input variables substantiated theoretically. The method was implemented in a tool to automate the development of control system of aircraft at a high level of abstraction.

42

Application of genetic algorithms for unmanned aircraft control system construction is considered in this paper. Control system contains a finite state machine and an artificial neural net. Neural net converts real input variables into finite state machine boolean input variables. Finite state machine generates input actions. Genetic algorithms are used for optimization of such model.

APPLICATION OF GENETIC PROGRAMMING AND OF REDUCED TRANSITION TABLES METHOD AND OF DECISION TREES METHOD FOR CONSTRUCTING A CONTROL SYSTEM FOR A MODEL OF AN UNMANNED AIRCRAFT
Dmitry Sokolov, Fedor Tsarev, Andrey Davydov

60

Application of genetic algorithms for construction of control systems for systems with complex behavior is considered in this paper. Two methods (reduced tables method and decision trees method) of automata representation are used. Application of these methods is illustrated on the problem of unmanned aircraft control.

CONSTRUCTION OF A CONTROL SYSTEM FOR A HELICOPTER MODEL USING GENETIC ALGORITHMS
Pavel Lobanov, Sergey Sytnik, Shalyto Anatoly Abramovich

79

The genetic algorithm for constructing the autopilot for a simplified model of a helicopter is proposed. Goal for helicopter is to pass predefined set of targets in predefined order. Implementation of genetic algorithm was made with Java programming language. Computational experiments to demonstrate the effectiveness of the algorithm are implemented.

CONSTRUCTION OF A CONTROL SYSTEM FOR ROBOCODE TANK USING GENETIC ALGORITHMS
Yury Bedny, Shalyto Anatoly Abramovich

88

The paper proposes a method of developing of the control system of the tank for the game Robocode, based on genetic algorithms that can automate the process of building control systems. In addition, the way to improve generated control systems by the use of more sophisticated algorithms realized with finite automaton.

### APPLICATION OF GENETIC ALGORITHMS TO GENERATE AUTOMATA

DEVELOPMENT OF A TOOL FOR FINITE STATE MACHINE GENERATION
WITH GENETIC ALGORTIHMS
Evgeny Mandrikov, Vladimir Kulev

100

As part of the research the tool is created for generating automata based on genetic programming, which allows you to increase the automation of development of automata-based programs. This tool name is GAAP (Genetic Algorithms for Automata-based Programming).

103

The paper proposes a new method for representation of automaton as an individual in an evolutionary algorithm based on a decision trees. Application of this method greatly reduces amount of memory needed for running evolutionary algorithm. The method of genetic programming based on the proposed representation is created. Efficiency of this method is illustrated on the example of solving one of the variants of “Artificial ant” problem.

APPLICATION OF GENETIC ALGORTIHMS FOR MOORE AUTOMATA AND SYSTEMS OF MEALY AUTOMATA CONSTRUCTION IN “ARTIFICIAL ANT” PROBLEM
Dmitry Sokolov, Fedor Tsarev, Andrey Davydov

108

A genetic algorithm for constructing Moore finite state machines is proposed in this paper. The same algorithm can be used for constructing systems of interaction Mealy finite state machines. For these types of automata genetic operations of mutation and cross-over were developed. Genetic algorithms are implemented with Java programming language. Application of these algorithms is illustrated on the example of “Artificial Ant” problem.

114

Three ways is proposed to increase the rate of convergence of standard genetic algorithms for the class of problems in which the solution is a finite automaton. First of them allows to greatly reduce number of automaton states thanks to usage of flags. Method of recovering of links between states allows reducing number of unused states. Method of sorting states in usage order allows reducing number of states in automata.

### VERIFICATION OF AUTOMATIC PROGRAMS

METHODS OF AUTOMATA-BASED PROGRAMS VERIFICATION
Sergey Velder, Shalyto Anatoly Abramovich

123

This article discusses ways of converting automata-based programs to Kripke models, designed to check the properties related to the behavior of the system. These properties are described with temporal logic formulas. Several methods of such a transformation are proposed.

VERIFICATION OF AUTOMATA-BASED PROGRAMS WITH SMV TOOL
Evgeny Kurbatsky

137

We consider the method of verification of automata-based programs using Model Checking method. To verify the model the tool SMV is used. In the proposed approach, transition system is not built in explicit form. This allows the program to verify systems with large number of states.

VERIFICATION OF AUTOMATA-BASED PROGRAMS WITH SPIN VERIFIER
Shalyto Anatoly Abramovich, Michael Lukin

145

A way to use SPIN verifier for the verification of automata-based programs is proposed. When using this verifier model is described with Promela language and requirements are specified with LTL language. A method of automated automata-based program to Promela model transformation is proposed. For LTL-formulas
transformation a special program was developed. Usage of this methods is illustrated on the example of cashmachine model verification.

VERIFICATION OF AUTOMATA-BASED PROGRAMS WITH UNIMOD.VERIFIER TOOL
Vadim Gurov, Bulat Jaminov

162

This article describes the verifier of automata-based programs created with the tool to support automata-based programming UniMod. Verifier works by integrating tool UniMod and verifier Bogor. Using developed verifier there is no need to convert automata-based program to the input language of the verifier. Requirements for the program are written in the language of temporal logic LTL.

DEVELOPMENT OF A VERIFIER FOR AUTOMATA-BASED PROGRAMS
Kirill Egorov, Shalyto Anatoly Abramovich

177

This article describes verifier of automata-based programs created with the tool to support automatic programming UniMod. When it is used, in contrast to the well-known verifiers, there is no need to describe the model in the input language of the verifier. Requirements for the program are written in the language of temporal
logic of linear time LTL (Linear Time Logic). Using this logic verification carried out by intersection of automaton-product of the model and Byuhi automaton built to deny LTL formula.

189

The article proposes an approach that increases the reliability of the development of Java Card applets. Features of applet developing using automata-based approach are formulated. Enhanced representation model to describe the functionality, code generator with plugs and tools for automatic testing of applets are provided.

DEVELOPMENT OF CORECT JAVA CARD-APPLICATION WITH AUTOMATA-BASED APPROACH
Клебанов А. А., Shalyto Anatoly Abramovich

198

In this paper describes the results of studies aimed at establishing the correct Java Card-code. In doing so, the code is generated from the high level description of automata-based programming. An additional advantage of this approach is the ability to generate a formal specification of the application. Compliance with the source or byte-code specifications can be verified by various verifiers or tools for dynamic and static testing.

VERIFICATION OF INTERACTION OF PARTS OF A REACTIVE SYSTEM IMPLEMENTED USING AUTOMATA-BASED APPROACH
Sergey Kanzhelev

211

Verification of interaction of parts of a reactive system implemented with automata-based approach is discussed in this paper. Problems which can appear in such systems and methods of their detection for several types of semantical interpretation are considered.

221

Method of automatic dynamic verification of Mealy finite state machines system based on alternating automat traversal. Structure of method, rules of building protocols and specification are described. Functional characteristics of this method are analysed on the base of its implementation.

### METHODS OF DEVELOPMENT OF AUTOMATIC PROGRAMS

DECLARATIVE APPROACH TO EMBEDDING AND INHERITANCE OF AUTOMATA CLASSES WITH IMPERATIVE PROGRAMMING LANGUAGES
Artem Astafurov

230

Declarative approach for automata-based objects in object-oriented imperative programming languages with static type checking is discussed in this paper. Main feature of this method is the ability of application of inheritance and embedding of macrostates.

INHERITANCE OF AUTOMATA CLASSED WITH DYNAMIC PROGRAMMING LANGUAGES ON THE EXAMPLE OF RUBY
Kirill Timofeev, Artem Astafurov

238

Object-oriented programming with explicit state emphasis has advantages of object-oriented and automta-based paradigms. Main advantages of such an approach are scalability, flexibility and presence of mechanism for complex behaviour description on the base of finite state machines. Object-oriented and dynamic approaches for inheritance and embedding of automata classes in dynamic programming languages.

### TOOLS AUTOMATA PROGRAMMING

A TOOL SUPPORTING AUTOMATA-BASED PROGRAMMING – UNIMOD 2. DESIGN. VALIDATION. VERIFICATION. IMPLEMENTATION
Dmitry Kochelev, Ivan Lagunov, Bulat Khasanzyanov, Bulat Jaminov

251

This article gives a short overview of instrumental tool with automata based programming UniMod 2. This tool was designed for development of automata based programs and provides means for visual designing, debugging, validation and verification of automata based programs.

### TEXTUAL LANGUAGES AUTOMATA PROGRAMMING

TEXTUAL LANGUAGE FOR AUTOMATA-BASED PROGRAMMING
Vadim Gurov, Maxim Mazin, Shalyto Anatoly Abramovich

258

Textual automata-based programming language is described in this paper. This language is built on the base of JetBrains MetaProgramming System (MPS). This language does not have such drawbacks of graphical language as low speed of entering diagrams and is more habitual to programmer.

263

UniMod tool allows designing and running automata-based programs. Its main constraint is graphical language for description of finite state machines. Textual automata-based programming language FSML (Finite State Machine Language) is described in this paper. An editor for this language was also created. It allows to describe finite state machines in UniMod with textual language.

### TESTING THE APPLICATION AND THE STATE MACHINE

A METHOD OF TESTS FOR API GENERATION ON THE BASE OF FINITE-STATE MODEL OF TESTING
Konstantin Rubinov, Vladimir Vedeneev, Vladimir Parfenov

273

An automata-based model approach for testing API is described in this paper. Method proposed is based on constructing graphical automata-based model for testing. After it test-cases are built with transitions graph traversal. Such an approach allows simplifying and formalizing test-case generation not only for functions, but for aggregation of functions.

### AUTOMATA PROGRAMMING MOBILE ROBOTS

APPLICATION OF AUTOMATA-BASED APPROACH FOR A MOBILE ROBOT CONTROL SYSTEM
Vitaliy Kleban, Vladimir Parfenov, Shalyto Anatoly Abramovich

281

An automata-based approach for design of control system for mobile robot is described in this paper. Automatabased programming is used for creating software for KVARK-M robot on three levels: on the top level three automata are used, on the middle there are five, on the bottom – eleven. Such an approach allows to greatly
heighten the quality of software for robots.

### APPLICATION OF FINITE STATE MACHINES FOR AUTOMATIZATION OF DOCUMENTS CIRCULATION

APPLICATION OF FINITE STATE MACHINES FOR AUTOMATIZATION OF DOCUMENTS CIRCULATION
Vitaliy Kleban, Fedor Novikov

286

Problem of automatization of documents circulation is considered in this paper. Finite state machines are used for building such a system. Such an approach has some advantages in comparison with traditional approach. Example of this approach – development of a Microsoft Office-based tool for automated quality management system for project based production – is described in this paper.

### ARTIFICIAL INTELLIGENCE AND THE STATE MACHINE

A MACHINE LEARINIGN METHOD FOR COMPLX SYSTEMS WITH A LOT OF INPUT DATA AND OUTPUT ACTIONS
Alexander Krass

295

A machine learning method for complex systems with many input variables and many output actions is described in this paper. This method allows taking into consideration behaviour restrictions. It greatly reduces size of a search space. This method also allows splitting system into subsystems on the base of subproblems. Solutions for subproblems can be united with rather complex conditions on transitions between them.