Vol 51, No 7 (2017)

Component-based systems permit standardisation and re-usability of code through the use of components. The architecture of component-based systems can be modified thanks to dynamic reconfigurations, which contribute to systems’ (self-)adaptation by adding or removing components without incurring any system downtime. In this context, the present article describes a formal model for dynamic reconfigurations of component-based systems. It provides a way of expressing runtime reconfigurations of a system and proving their correctness according to a static invariant for consistency constraints and/or a user-provided post-condition. Guarded reconfigurations allow us to build reconfigurations based on primitive reconfiguration operations using sequences of reconfigurations and the alternative and the repetitive constructs, while preserving configuration consistency. A practical contribution consists of the implementation of a component-based model using the GROOVE graph transformation tool. This implementation is illustrated on a cloud-based multi-tier application hosting environment managed as a component-based system. In addition, after enriching the model with interpreted configurations and reconfigurations in a consistency compatible manner, component systems’ implementations are related to their specifications by a simulation relation.

The article presents a method for the analysis and verification of Use Case Map (UCM) models with scenario control structures—protected components and failure handling constructs. UCM models are analyzed and verified with the help of colored Petri nets (CPN) and the SPIN model checker. Algorithms for translating UCM scenario control structures into CPN and CPN into SPIN input language Promela are described. The number of elements of the resulting CPN model and the number of Promela model states are estimated. The presented algorithm and the verification process are illustrated by the study of a network router firmware update.

The paper considers the problem of deriving a cascade parallel composition of timed finite state machines (TFSMs). It can be reduced to a step-by-step derivation of a binary parallel composition. It is known that if each component of the binary parallel composition is a TFSM with constant output delays, then the composition can result in a TFSM with an infinite set of output delays given by a finite set of linear functions. Therefore, the problem of deriving a cascade composition of TFSMs with constant output delays is reduced to deriving a series of binary parallel compositions of TFSMs with output delays given either as constants or as a set of linear functions. In this paper, we refine the definition of the TFSM with particular attention to the description of the output delay. BALM-II is used as an instrument for deriving the composition. Therefore, we consider the transition from a TFSM with output delays given as a set of linear functions to the corresponding automaton. We propose a new procedure for deriving an automaton. Unlike the known procedure, it does not require subsequent determinization of the derived automaton. In addition, we provide a step-by-step description of how to derive the composition of the corresponding automata using BALM-II, discuss the procedure of reverse transformation from the automaton of the composition to the TFSM, and note some aspects associated with the composition of TFSMs with output delays as a set of linear functions. An example that illustrates the derivation of the cascade parallel composition of TFSMs is given.

Finite state transducers over semigroups are regarded as a formal model of sequential reactive programs that operate in the interaction with the environment. At receiving a piece of data a program performs a sequence of actions and displays the current result. Such programs usually arise at implementation of computer drivers, on-line algorithms, control procedures. In many cases verification of such programs can be reduced to minimization and equivalence checking problems for finite state transducers. Minimization of a transducer over a semigroup is performed in three stages. At first the greatest common left-divisors are computed for all states of a transducer, next a transducer is brought to a reduced form by pulling all such divisors “upstream,” and finally a minimization algorithm for finite state automata is applied to the reduced transducer.

We consider the problem of choosing a balanced set of fault-tolerance techniques for distributed computer systems. In this problem, it is necessary to choose a balanced set of versions of the modules of distributed computer systems, during which the reliability of the set must be maximized under cost constraints (on the set of possible versions of distributed computer systems). We describe the fault-tolerance techniques out of which the choice is made and consider a mathematical model in the context of which the formulation of the problem and the method of its solution are given. This problem is widely considered in the literature. A detailed description of the method for choosing a balanced set of fault-tolerance techniques for distributed computer systems is presented. The proposed method represents an evolutionary algorithm using the scheme of fuzzy logic. The scheme of fuzzy logic in the process of operating the algorithm analyzes the results of its operation in each generation and from this information adjusts the parameters of the evolutionary algorithm. The method makes it possible to obtain an efficient solution, as shown in the experimental research. A key feature of the proposed approach is the use of an adaptive scheme. The method has been implemented as software integrated with the DYANA simulation environment. The conclusions of the paper contain a brief description of future research directions.

The problem of integer balancing of a four-dimensional matrix is studied. The elements of the inner part (all four indices are greater than zero) of the given real matrix are summed in each direction and each two- and three-dimensional section of the matrix; the total sum is also found. These sums are placed into the elements where one or more indices are equal to zero (according to the summing directions). The problem is to find an integer matrix of the same structure, which can be produced from the initial one by replacing the elements with the largest previous or the smallest following integer. At the same time, the element with four zero indices should be produced with standard rules of rounding-off. In the article the problem of finding the maximum multiple flow in the network of any natural multiplicity k is also studied. There are arcs of three types: ordinary arcs, multiple arcs and multi-arcs. Each multiple and multi-arc is a union of k linked arcs, which are adjusted with each other. The network constructing rules are described. The definitions of a divisible network and some associated subjects are stated. There are defined the basic principles for reducing the integer balancing problem of an l-dimensional matrix (l ≥ 3) to the problem of finding the maximum flow in a divisible multiple network of multiplicity k. There are stated the rules for reducing the four-dimensional balancing problem to the maximum flow problem in the network of multiplicity 5. The algorithm of finding the maximum flow, which meets the solvability conditions for the integer balancing problem, is formulated for such a network.

We study the polyhedral properties of three problems of constructing an optimal complete bipartite subgraph (a biclique) in a bipartite graph. In the first problem, we consider a balanced biclique with the same number of vertices in both parts and arbitrary edge weights. In the other two problems we are dealing with unbalanced subgraphs of maximum and minimum weight with non-negative edges. All three problems are established to be NP-hard. We study the polytopes and the cone decompositions of these problems and their 1-skeletons. We describe the adjacency criterion in the 1-skeleton of the polytope of the balanced complete bipartite subgraph problem. The clique number of the 1-skeleton is estimated from below by a superpolynomial function. For both unbalanced biclique problems we establish the superpolynomial lower bounds on the clique numbers of the graphs of nonnegative cone decompositions. These values characterize the time complexity in a broad class of algorithms based on linear comparisons.

For singularly perturbed second-order equations, the dependence of the eigenvalues of the first boundary-value problem on a small parameter at the highest derivative is studied. The main assumption is that the coefficient at the first derivative in the equation is the sign of the variable. This leads to the emergence of so-called turning points. Asymptotic expansions with respect to a small parameter are obtained for all eigenvalues of the considered boundary-value problem. It turns out that the expansions are determined only by the behavior of the coefficients in the neighborhood of the turning points.

The process of plastic flow localization in a composite material consisting of welded steel and copper plates under shear strain is considered. The mathematical model of this physical process is formulated. A new numerical algorithm based on the Courant–Isaacson–Rees scheme is proposed. The algorithm is verified using three test problems. The algorithm efficiency and performance are proved by the test simulations. The proposed algorithm is used for numerical simulation of plastic strain localization on composite materials. The influence of boundary conditions, the initial plastic strain rate, and the width of the materials forming the composite bar on the localization process is studied. It is demonstrated that at the initial stage, the shear velocity for the material layers varies. Theoretical estimates of the oscillation frequency and period are proposed; the calculations using these estimates agree completely with the numerical experiments. It is established that the deformation is localized in the copper part of the composite. One or two localization regions situated at a typical distance from the boundaries are formed, depending on the width of the steel and copper parts, as well as the initial plastic strain rate and the chosen boundary conditions. The dependence of this distance on the initial plastic strain rate is demonstrated and corresponding estimates for boundary conditions of two types are obtained. It is established that in the case of two localization regions, the temperature and deformation in one of them increase much faster than in the other, while at the initial stage these quantities are nearly equal in both regions.

This work is devoted to investigating the dynamic properties of the solutions to the boundaryvalue problems associated with the classic Fermi–Pasta–Ulam (FPU) system. We analyze these problems for an infinite-dimensional case where a countable number of roots of characteristic equations tend to an imaginary axis. Under these conditions, we build a special nonlinear partial differential equation that acts as a quasi-normal form, i.e., determines the dynamics of the original boundary-value problem with the initial conditions in a sufficiently small neighborhood of the equilibrium state. The modified Korteweg–deVries (KdV) equation and the Korteweg–de Vries–Burgers (KdVB) equation act as quasi-normal forms depending on the parameter values. Under some additional assumptions, we apply the renormalization procedure to the boundary-value problems obtained. This procedure leads to an infinite-dimensional system of ordinary differential equations. We describe a method for folding this system into a special boundary- value problem, which is an analog of the normal form. The main contribution of this work is investigating the interaction of the waves moving in different directions in the FPU problem by using analytical methods of nonlinear dynamics. It is shown that the mutual influence of the waves is asymptotically small, does not affect their shape, and contributes only to a shift in their speeds, which does not change over time.

In this paper, we consider a singularly perturbed system of two differential equations with delay, simulating two coupled oscillators with a nonlinear feedback. The feedback function is assumed to be compactly supported and piecewise-continuous and it is assumed that its sign is constant. In this paper, we prove the existence of relaxation periodic solutions and make conclusions about their stability. Using a special large-parameter method, we construct asymptotics of all solutions of the considered system under the assumption that the initial-value conditions belong to a certain class. Using this asymptotics, we construct a special mapping principally describing the dynamics of the original model. It is shown that the dynamics changes fundamentally as the coupling coefficient decreases: we have a stable homogeneous periodic solution if the coupling coefficient is on the order of unity and the dynamics become more complex as the coupling coefficient decreases (it is described by a special map). For small values of the coupling, we show that there are values of the parameters such that several different stable relaxation periodic regimes coexist in the original problem.

In this paper, we consider a mathematical model of synaptic interaction between two pulse neuron elements. Each of the neurons is modeled by a singularly perturbed difference-differential equation with delay. Coupling is assumed to be at the threshold with the time delay being taken into account. The problems of existence and stability of relaxation periodic movements for the systems derived are considered. It turns out that the critical parameter is the ratio between the delay caused by internal factors in the single-neuron model and the delay in the coupling link between the oscillators. The existence and stability of a uniform cycle for the problem are proved in the case where the delay in the link is less than the period of a single oscillator, which depends on the internal delay. As the delay grows, the in-phase regime becomes more complex; specifically, it is shown that, by choosing an adequate delay, we can obtain more complex relaxation oscillations and, during a period, the system can exhibit more than one high-amplitude splash. This means that the bursting effect can appear in a system of two synaptically coupled neuron-type oscillators due to the delay in the coupling link.

It is planned to create a method of clustering a social network graph. To test the method, it is necessary to generate a graph similar in structure to existing social networks. The article presents an algorithm for the graph-distributed generation. We take into account basic properties such as the power-law distribution of the number of user communities, the dense intersections of social networks, and others. This algorithm also considers the problems that are present in similar works of other authors, for example, the multiple edges problem in the generation process. A special feature of the created algorithm is the implementation depending on the number of communities, rather than on the number of connected users, as is done in other works. This is connected with a peculiarity of the development of the existing social network structure. The properties of its graph are described in the paper. We describe a Table 1 containing the variables needed for the algorithm. A step-by-step generation algorithm is compiled. Appropriate mathematical parameters are calculated for it. The generation is performed in a distributed way by the Apache Spark framework. It is described in detail how the division of tasks with the help of this framework operates. The Erdos–Renyi model for random graphs is used in the algorithm. It is the most suitable and easiest one to implement. The main advantages of the created method are the small amount of resources and faster execution speed in comparison with other similar generators. Speed is achieved through distributed work and the fact that at any time, the network users have their own unique numbers and are ordered by these numbers so that there is no need to sort them out. The designed algorithm will not only promote the creation of an efficient clustering method, but can also be useful in other development areas connected, for example, with social network search engines.

First-order program schemata represent one of the most simple models of sequential imperative programs intended for solving verification and optimization problems. We consider the decidable relation of logical-thermal equivalence on these schemata and the problem of their size minimization while preserving logical-thermal equivalence. We prove that this problem is decidable. Further we show that the first-order program schemata supplied with logical-thermal equivalence and finite-state deterministic transducers operating over substitutions are mutually translated into each other. This relationship makes it possible to adapt equivalence checking and minimization algorithms developed in one of these models of computation to the solution of the same problems for the other model of computation. In addition, on the basis of the discovered relationship, we describe a subclass of first-order program schemata such that minimization of the program schemata from this class can be performed in polynomial time by means of known techniques for minimization of finite-state transducers operating over semigroups. Finally, we demonstrate that in the general case the minimization problem for finite state transducers over semigroups may have several non-isomorphic solutions.

During the life-cycle of an Information System (IS) its actual behavior may not correspond to the original system model. However, to the IS support it is very important to have the latest model that reflects the current system behavior. To correct the model the information from the event log of the system may be used. In this paper, we consider the problem of process model adjustment (correction) using the information from event log. The input data for this task is the initial process model (a Petri net) and an event log. The result of correction should be a new process model, better reflecting the real IS behavior than the initial model. The new model could be also built from scratch, for example, with the help of one of the known algorithms for automatic synthesis of the process model from an event log. However, this may lead to crucial changes in the structure of the original model, and it will be difficult to compare the new model with the initial one, hindering its understanding and analysis. Then it is important to keep the initial structure of the model as much as possible. In this paper we propose a method for process model correction based on the principle of “divide and conquer”. The initial model is decomposed into several fragments. For each of the fragments its conformance to the event log is checked. Fragments, which do not match the log, are replaced by newly synthesized ones. The new model is then assembled from the fragments via transition fusion. The experiments demonstrate that our correction algorithm gives good results when it is used for correcting local discrepancies. The paper presents the description of the algorithm, the formal justification for its correctness, as well as the results of experimental testing on artificial examples.

The Takagi function is a simple example of a continuous yet nowhere differentiable function and is given as T(x) = Σ_k=0^∞ 2⁻ⁿ ρ(2ⁿx), where \(\rho (x) = \mathop {\min }\limits_{k \in \mathbb{Z}} |x - k|\). The moments of the Takagi function are given as M_n = ∫₀¹xⁿT(x)dx. The estimate \({M_n} = \frac{{1nn - \Gamma '(1) - 1n\pi }}{{{n^2}1n2}} + \frac{1}{{2{n^2}}} + \frac{2}{{{n^2}1n2}}\phi (n) + O({n^{ - 2.99}})\), where the function \(\phi (x) = \sum\nolimits_{k \ne 0} \Gamma (\frac{{2\pi ik}}{{1n2}})\zeta (\frac{{2\pi ik}}{{1n2}}){x^{ - \frac{{2\pi ik}}{{1n2}}}}\) is periodic in log₂x and Γ(x) and ζ(x) denote the gamma and zeta functions, is the principal result of this work.

In this paper we consider the nonlocal dynamics of the model of two coupled oscillators with delayed feedback. This model has the form of a system of two differential equations with delay. The feedback function is non-linear, compactly supported and smooth. The main assumption in the problem is that the coupling between the generators is sufficiently small. With the help of asymptotic methods we investigate the existence of relaxation periodic solutions of a given system. For this purpose, a special set is constructed in the phase space of the original system. Then we build an asymptotics of the solutions of the given system with initial conditions from this set. Using this asymptotics, a special mapping is constructed. Dynamics of this map describes the dynamics of the original problem in general. It is proved that all solutions of this mapping are non-rough cycles of period two. As a result, we formulate conditions for the coupling parameter such that the initial system has a two-parameter family of non-rough inhomogeneous relaxation periodic asymptotic (with respect to the residual) solutions.

Let n ∈N, and let Q_n = [0 1]ⁿ. For a nondegenerate simplex S ⊂ Rⁿ, by σS we denote the homothetic copy of S with center of homothety in the center of gravity of S and ratio of homothety σ. By ξ(S) we mean the minimal σ > 0 such that Q_n ⊂ σS. By α(S) let us denote the minimal σ > 0 such that Q_n is contained in a translate of σS. By d_i(S) we denote the ith axial diameter of S, i. e. the maximum length of the segment contained in S and parallel to the ith coordinate axis. Formulae for ξ(S), α(S), d_i(S) were proved earlier by the first author. Define ξ_n = min{ξ(S): S ⊂ Q_n}. Always we have ξ_n ≥ n. We discuss some conjectures formulated in the previous papers. One of these conjectures is the following. For every n, there exists γ > 0, not depending on S ⊂ Q_n, such that an inequality ξ(S) − α(S) ≤ γ(ξ(S) − ξ_n) holds. Denote by ϰ_n the minimal γ with such a property. We prove that ϰ₁ = \(\frac{1}{2}\); for n > 1, we obtain ϰ_n ≥ 1. If n > 1 and ξ_n = n, then ϰ_n = 1. The equality holds ξ_n = n if n + 1is an Hadamard number, i. e. there exists an Hadamard matrix of order n + 1. This proposition is known; we give one more proof with the direct use of Hadamard matrices. We prove that ξ₅ = 5. Therefore, there exist n such that n + 1 is not an Hadamard number and nevertheless ξ_n = n. The minimal n with such a property is equal to 5. This involves ϰ₅ = 1 and also disproves the following previous conjecture of the first author concerning the characterization of Hadamard numbers in terms of homothety of simplices: n + 1 is an Hadamard number if and only if ξ_n = n. This statement is valid only in one direction. There S ⊂ Q₅ exists simplex such that the boundary of the simplex 5S contains all the vertices of the cube Q₅. We describe one-parameter family of simplices contained in Q₅ with the property α(S) = ξ(S) = 5. These simplices were found with the use of numerical and symbolic computations. Another new result is an inequality ξ₆ < 6.0166. We also systematize some of our estimates of numbers ξ_n, θ_n, ϰ_n provided by the present day. The symbol θ_n denotes the minimal norm of interpolation projector on the space of linear functions of n variables as an operator from C(Q_n) to C(Q_n).