The purpose of the study is to demonstrate the feasibility of automated code migration to a new set of programming libraries. Code migration is a common task in modern software projects. For example, it may arise when a project should be ported to a more secure or feature-rich library, a new platform or a new version of an already used library. The developed method and tool are based on the previously created by the authors a formalism for describing libraries semantics. The formalism specifies a library behaviour by using a system of extended finite state machines (EFSM). This paper outlines the metamodel designed to specify library descriptions and proposes an easy to use domainspecific language (DSL), which can be used to define models for particular libraries. The mentioned metamodel directly forms the code migration procedure. A process of migration is split into five steps, and each step is also described in the paper. The procedure uses an algorithm based on the breadth- first search extended for the needs of the migration task. Models and algorithms were implemented in the prototype of an automated code migration tool. The prototype was tested by both artificial code examples and a real-world open source project. The article describes the experiments performed, the difficulties that have arisen in the process of migration of test samples, and how they are solved in the proposed procedure. The results of experiments indicate that code migration can be successfully automated.

 

Abstract. The notation of state machines is widely adopted as a formalism to describe the behaviour of systems. Usually, multiple state machine models can be developed for the very same software system. Some of these models might turn out to be equivalent, but, in many cases, different state machines describing the same system also differ in their level of abstraction. In this paper, we present an approach to actually measure the abstractness level of state machines w.r.t. a given implemented software system. A state machine is considered to be less abstract when it is conceptionally closer to the implemented system. In our approach, this distance between state machine and implementation is measured by applying coverage criteria known from software mutation testing. Abstractness of state machines can be considered as a new metric. As for other metrics as well, a known value for the abstractness of a given state machine allows to assess its quality in terms of a simple number. In model-based software development projects, the abstract metric can help to prevent model degradation since it can actually measure the semantic distance from the behavioural specification of a system in form of a state machine to the current implementation of the system. In contrast to other metrics for state machines, the abstractness cannot be statically computed based on the state machine’s structure, but requires to execute both state machine and corresponding system implementation. The article is published in the author’s wording.

 

Static verification of a program source code correctness is an important element of software reliability. Formal verification of software programs involves proving that a program satisfies a formal specification of its behavior. Many languages use both static and dynamic type checking. With such approach, the static type checker verifies everything possible at compile time, and the dynamic one checks the remaining. The current state of the Jolie programming language includes a dynamic type system. Consequently, it allows avoidable run-time errors. A static type system for the language has been formally defined on paper but lacks an implementation yet. In this paper, we describe a prototype of Jolie Static Type Checker (JSTC), which employs a technique based on a SMT solver. We describe the theory behind and the implementation, and the process of static analysis. The article is published in the authors’ wording.

 

Null pointer dereferencing remains one of the major issues in modern object-oriented languages. An obvious addition of keywords to distinguish between never null and possibly null references appears to be insufficient during object initialization when some fields declared as never null may be temporary null before the initialization completes. This work identifies the key reasons of the object initialization problem. It suggests scenarios and metrics to be used as the benchmarks to compare solutions of this problem. Finally, it demonstrates application of the benchmarks on the proposed solution for object initialization in Eiffel. The article is published in the author’s wording.

 

In this paper, we study the problem of existence check and derivation of synchronizing and homing sequences for finite input/output automata. Corresponding sequences can be effectively used for the current state identification of a system under test / verification, after the input sequence is applied. In the model considered in the paper, the alphabet of actions is divided into disjoint sets of inputs and outputs; however, no sets of possible initial or final states are defined. We introduce the notions of homing and synchronizing sequences for a specific class of such machines for which at each state the transitions only under inputs or under outputs are defined, and the machine transition diagram does not contain cycles labeled by outputs, i.e. the language of the machine does not contain traces with infinite postfix of outputs. For such a class of input/output automata, we establish necessary and sufficient conditions for the existence of synchronizing and homing sequences and discuss the length of such sequences. We also define some subclasses of automata for which the worst-case upper bounds (normally, exponential) are not reachable.

 

This work represents the further development of the method for definite iteration verification [7]. It extends the mixed axiomatic semantics method [1] suggested for C-light program verification. This extension includes a verification method for definite iteration over unchangeable arrays with a loop exit in C-light programs. The method includes an inference rule for the iteration without invariants, which uses a special function that expresses loop body. This rule was implemented in verification conditions generator, which is the part of our C-light verification system. To prove generated verification conditions an induction is applied which is a challenge for SMT-solvers. At proof stage the SMT-solver CVC4 is used in our verification system. To overcome mentioned difficulty a rewriting strategy for verification conditions is suggested. A method based on theory extension by new theorems to prove verification conditions is suggested. An example, which illustrates the application of these methods, is considered. The article is published in the authors’ wording.

 

Software-defined networking is a promising technology for constructing communication networks where the network management is the software that configures network devices. This contrasts with the traditional point of view where the network behaviour is updated by manual configuration uploading to devices under control. The software controller allows dynamic routing configuration inside the net depending on the quality of service. However, there must be a proof that ensures that every network flow is secure, for example, we can define security policy as follows: confidential nodes can not send data to the public segment of the network. The paper shows how this problem can be solved by using a semantic security model. We propose a method that allows us to construct semantics that captures necessary security properties the network must follow. This involves the specification that states allowed and forbidden network flows. The specification is then modeled as a decision tree that may be reduced. We use the decision tree for semantic construction that captures security requirements. The semantic can be implemented as a module of the controller software so the correctness of the control plane of the network can be ensured on-the-fly.

 

To ensure traffic safety of railway transport, non-destructive testing of rails is regularly carried out by using various approaches and methods, including magnetic and eddy current flaw detection methods. The paper is devoted to the problem of automatic determination of a threshold level of amplitudes of useful signals (from defects and structural elements of a railway track) during the analysis of defectograms (records) of magnetic and eddy current flaw detectors. A signal is considered useful (and is subject to further analysis) if a deviation of its value from an average of all signals is at least twice the threshold noise level of rails. The probability of obtaining a signal from a section without structural elements (a rail noise signal) is characterized by the normal distribution law. Thus, the rule of three sigma can be used to calculate the threshold noise level. And a signal is useful if its amplitude deviation from a sample mean exceeds twice the threshold noise level. The paper proposes an algorithm for finding the threshold level of a rail noise and gives its theoretical justification, and it also examines examples of its operation on several fragments of real magnetic and eddy current defectograms.

 

The main purpose of the article is to analyze how effectively different types of thesaurus relations can be used for solutions of text classification tasks. The basis of the study is an automatically generated thesaurus of a subject area, that contains three types of relations: synonymous, hierarchical and associative. To generate the thesaurus the authors use a hybrid method based on several linguistic and statistical algorithms for extraction of semantic relations. The method allows to create a thesaurus with a sufficiently large number of terms and relations among them. The authors consider two problems: topical text classification and sentiment classification of large newspaper articles. To solve them, the authors developed two approaches that complement standard algorithms with a procedure that take into account thesaurus relations to determine semantic features of texts. The approach to topical classification includes the standard unsupervised BM25 algorithm and the procedure, that take into account synonymous and hierarchical relations of the thesaurus of the subject area. The approach to sentiment classification consists of two steps. At the first step, a thesaurus is created, whose terms weight polarities are calculated depending on the term occurrences in the training set or on the weights of related thesaurus terms. At the second step, the thesaurus is used to compute the features of words from texts and to classify texts by the algorithm SVM or Naive Bayes. In experiments with text corpora BBCSport, Reuters, PubMed and the corpus of articles about American immigrants, the authors varied the types of thesaurus relations that are involved in the classification and the degree of their use. The results of the experiments make it possible to evaluate the efficiency of the application of thesaurus relations for classification of raw texts and to determine under what conditions certain relationships affect more or less. In particular, the most useful thesaurus connections are synonymous and hierarchical, as they provide a better quality of classification.

 

In the article, the definition of an undirected multiple graph of any natural multiplicity k > 1 is stated. There are edges of three types: ordinary edges, multiple edges and multi-edges. Each edge of the last two types is the union of k linked edges, which connect 2 or k+1 vertices, correspondingly. The linked edges should be used simultaneously. If a vertex is incident to a multiple edge, it can be also incident to other multiple edges and it can be the common ending vertex to k linked edges of some multi-edge. If a vertex is the common end of some multi-edge, it cannot be the common end of any other multi-edge. Also, a class of the divisible multiple graphs is considered. The main peculiarity of them is a possibility to divide the graph into k parts, which are adjusted on the linked edges and which have no common edges. Each part is an ordinary graph. The following terms are generalized: the degree of a vertex, the connectedness of a graph, the path, the cycle, the weight of an edge, and the path length. There is stated the definition of the reachability set for the ordinary and multiple edges. The adjacency property is defined for a pair of reachability sets. It is shown, that we can check the connectedness of some multiple graph with the polynomial algorithm based on the search for the reachability sets and testing their adjacency. There is considered a criterion of the existence of a multiple path between two given vertices. The shortest multiple path problem is stated. Then we suggest an algorithm of finding the shortest path in a multiple graph. It uses Dijkstra’s algorithm of finding the shortest paths in subgraphs, which correspond to different reachability sets.

In this paper, an approach to the construction of nonlinear output tracking control on a finite time interval for a class of weakly nonlinear systems with state-dependent coefficients is considered. The proposed method of control synthesis consists of two main stages. At the first stage, a nonlinear state feedback regulator is constructed by using a previously proposed control algorithm based on the State Dependent Riccati Equation (SDRE). At the second stage, the problem of fullorder observer construction is formulated and then it is reduced to the differential game problem. The form of its solution is obtained with the help of the guaranteed (minimax) control principle, which allows to find the best observer coefficients with respect to a given functional considering the worstcase uncertainty realization. The form of the obtained equations made it possible to use the algorithm from the first stage to determine the observer matrix. The proposed approach is characterized by the nonapplicability of the estimation and control separation principle used for linear systems, since the matrix of observer coefficients turned out to be dependent on the feedback coefficients matrix. The use of numerical-analytical procedures for determination of observer and feedback coefficients matrices significantly reduces the computational complexity of the control algorithm.

 

It is a brief version of the report made by the authors at the seminar “Modeling and Analysis of Information Systems”, Yaroslavl, May 17, 2017. The interrelation of problems of computeraided constructing the thesaurus and specification of verse texts in poetology is considered.