Preview

Modeling and Analysis of Information Systems

Advanced search
Vol 26, No 3 (2019)
View or download the full issue PDF (Russian)

Software

317-331 759
Abstract

A method is developed for assessing the practical persistence of obfuscating transformations of programs based on the calculation of the similarity index for the original, obfuscated and deobfuscated programs. Candidates are proposed for similarity indices, which are based on such program characteristics as the control flow graph, symbolic execution time and degree of coverage for symbolic execution. The control flow graph is considered as the basis for building other candidates for program similarity indicators. On its basis, a new candidate is proposed for the similarity index, which, when calculated, finds the Hamming distance between the adjacency matrices of control flow graphs of compared programs. A scheme for estimating (analyzing) the persistence of obfuscating transformations is constructed, according to which for the original, obfuscated and deobfuscated programs, the characteristics of these programs are calculated and compared in accordance with the chosen comparison model. The developed scheme, in particular, is suitable for comparing programs based on similarity indices. This paper develops and implements one of the key units of the constructed scheme - a block for obtaining program characteristics compiled for the x86/x86 64 architecture. The developed unit allow to find the control flow graph, the time for symbolic execution and the degree of coverage for symbolic execution. Some results of work of the constructed block are given.

332-350 1191
Abstract

We investigate a formal verification problem (mathematically rigorous correctness checking) for digital waveforms used in practical development of digital microelectronic devices (digital circuits) at early design stages. According to modern methodologies, a digital circuit design starts at high abstraction levels provided by hardware description languages (HDLs). One of essential steps of an HDLbased circuit design is an HDL code debug, similar to the same step of program development in means and importance. A popular way of an HDL code debug is based on extraction and analysis of a waveform, which is a collection of plots for digital signals: functional descriptions of value changes related to selected circuit places in real time. We propose mathematical means for automation of correctness checking for such waveforms based on notions and methods of formal verification against temporal logic formulae, and focus on such typical featues of HDL-related digital signals and corresponding (informal) properties, such as real time, three-valuededness, and presence of signal edges. The three-valuededness means that at any given time, besides basic logical values 0 and 1, a signal may have a special undefined value: one of the values 0 and 1, but which one of them is either not known, or not important. An edge point of a signal is a time point at which the signal changes its value. The main results are mathematical notions, propositions, and algorithms which allow to formalize and solve a formal verification problem for considered waveforms, including: definitions for signals and waveforms which the mentioned typical digital signal features; a temporal logic suitable for formalization of waveform correctness properties, and a related verification problem statement; a solution technique for the verification problem, which is based on reduction to signal transfromation and analysis; a corresponding verification algorithm together with its correctness proof and “reasonable” complexity bounds.

Computer System Organization

351-359 747
Abstract
In this work, the model of development of the P2P file exchange network organized by a torrent tracker is considered. The model is constructed on the basis of ordinary differential equations. The phase variables describing a status of a torrent tracker and the network organized by it (in first approximation is the number of the users of the tracker who are actively participate in information exchange, and the number of active torrents) are defined, the factors influencing the change of users number and the number of torrents are analyzed. On the basis of the analysis the system of differential equations, in first approximation describing evolution of the file exchange network organized by the torrent tracker — a hard dynamic model of evolution of the torrent tracker is written. Equilibrium points of hard model of evolution of the tracker are investigated, their possible quantity and type is described. All configurations of the general provision, possible in a hard model of evolution of the torrent tracker are described. The phase portrait of the hard model is represented. On the basis of the analysis of the hard model the system of differential equations describing evolution of a file exchange network with accounting of dependence of new users inflow intensity on a total quantity of potential audience of the torrent tracker, and also dependences of speed of torrents extinction on the number of users falling on one torrent — a soft dynamic model of evolution of a torrent tracker is written. Equilibrium points of a soft model of tracker evolution are investigated, their possible quantity and type is described. All configurations of the general provision, possible in a soft model of evolution of the torrent tracker are described. Phase portraits of each configuration are represented. The ratio of parameters necessary for the stability of the tracker a stable status is received. The influence of different administrative measures on a stock of the tracker stability in whole is analyzed. The need of support of torrents by administration at highly specialized torrent trackers with small potential audience is shown.
360-364 920
Abstract

Based on the analysis of modern tools for creating GRID-type information systems that are part of the European EGI “standard” – UMD repository (including new versions of Globus Toolkit, ARC, dCache, etc.), the applying of GRID systems for computational chemistry is briefly discussed. The GRID system created by the authors combines two clusters with Linux CentOS 7 and is based on software from UMD-4. The relevance and effectiveness of batch processing systems (we use Torque 4.2.10) in quantum chemical calculations is increased for mass calculations of docking complexes (including for drug modeling problems), for which an improved semiempirical method with more efficient approximations was proposed, implemented in the Fortran-95 LSSDOCK software package. For such calculations, new approximation methods have been developed, including for DFT functionals, and their software implementation is carried out. Converters of calculation results by LSSDOCK into a natural for GRID XML-based format CML version 3 are developed. Using the CML format based on dCache software, a single tree of a virtual GRID filesystem distributed between heterogeneous nodes is used to store the results of LSSDOCK calculations.

365-404 926
Abstract

The article is devoted to the mathematical modeling of artificial genetic networks. A phenomenological model of the simplest genetic network called repressilator is considered. This network contains three elements unidirectionally coupled into a ring. More specifically, the first of them inhibits the synthesis of the second, the second inhibits the synthesis of the third, and the third, which closes the cycle, inhibits the synthesis of the first one. The interaction of the protein concentrations and of mRNA (message RNA) concentration is surprisingly similar to the interaction of six ecological populations — three predators and three preys. This allows us to propose a new phenomenological model, which is represented by a system of unidirectionally coupled ordinary differential equations. We study the existence and stability problem of a relaxation periodic solution that is invariant with respect to cyclic permutations of coordinates. To find the asymptotics of this solution, a special relay system is constructed. It is proved in the paper that the periodic solution of the relay system gives the asymptotic approximation of the orbitally asymptotically stable relaxation cycle of the problem under consideration.

Algorithms

405-419 950
Abstract

In this paper, we study the two-step colouring problem for an undirected connected graph. It is required to colour the graph in a given number of colours in a way, when no pair of vertices has the same colour, if these vertices are at a distance of 1 or 2 between each other. Also the corresponding recognition problem is set. The problem is closely related to the classical graph colouring problem. In the article, we study and prove the polynomial reduction of the problems to each other. So it allows us to prove NP-completeness of the problem of two-step colouring. Also we specify some of its properties. Special interest is paid to the problem of two-step colouring in application to rectangular grid graphs. The maximum vertex degree in such a graph is between 0 and 4. For each case, we elaborate and prove the function of two-vertex colouring in the minimum possible number of colours. The functions allow each vertex to be coloured independently from others. If vertices are examined in a sequence, colouring time is polynomial for a rectangular grid graph.

420-440 1053
Abstract

Analysis of the functional equivalence of an original text and its translation based on the achievement of rhythm equivalence is an extremely important task of modern linguistics. Moreover, the rhythm component is an integral part of functional equivalence that cannot be achieved without communication of rhythm figures of the text. To analyze rhythm figures in an original literary text and its translation, the authors developed the ProseRhythmDetector software tool that allows to find and visualize lexical and syntactic figures in English- and Russian-language prose texts: anaphora, epiphora, symploce, anadiplosis, epanalepsis, reduplication, epistrophe, polysyndeton, and aposiopesis. The goal of this work is to present the results of ProseRhythmDetector testing on two works by English authors and their translations into Russian: Ch. Bronte “Villette” and I. Murdoch “The Black Prince”. Basing on the results of the tool, the authors compared rhythm figures in an original text and its translation both in aspects of the rhythm and their contexts. This experiment made it possible to identify how the features of the author’s style are communicated by the translator, to detect and explain cases of mismatch of rhythm figures in the original and translated texts. The application of the ProseRhythm-Detector software tool made it possible to significantly reduce the amount of linguistsexperts work by automated detection of lexical and syntactic figures with quite high precision (from 62 % to 93 %) for various rhythm figures.

Discrete Mathematics in Relation to Computer Science

441-449 811
Abstract
Suppose \(n\in {\mathbb N}\). Let \(B_n\) be a Euclidean unit ball in \({\mathbb R}^n\) given by the inequality \(\|x\|\leq 1\), \(\|x\|:=\left(\sum\limits_{i=1}^n x_i^2\right)^{\frac{1}{2}}\). By \(C(B_n)\) we mean a set of continuous functions \(f:B_n\to{\mathbb R}\) with the norm \(\|f\|_{C(B_n)}:=\max\limits_{x\in B_n}|f(x)|\). The symbol \(\Pi_1\left({\mathbb R}^n\right)\) denotes a set of polynomials in \(n\) variables of degree \(\leq 1\), i.e. linear functions upon \({\mathbb R}^n\). Assume that \(x^{(1)}, \ldots, x^{(n+1)}\) are vertices of an \(n\)-dimensional nondegenerate simplex \(S\subset B_n\). The interpolation projector \(P:C(B_n)\to \Pi_1({\mathbb R}^n)\) corresponding to \(S\) is defined by the equalities \(Pf\left(x^{(j)}\right)=f\left(x^{(j)}\right).\) Denote by \(\|P\|_{B_n}\) the norm of \(P\) as an operator from \(C(B_n)\) on to \(C(B_n)\). Let us define \(\theta_n(B_n)\) as the minimal value of \(\|P\|_{B_n}\) under the condition \(x^{(j)}\in B_n\). We describe the approach in which the norm of the projector can be estimated from the bottom through the volume of the simplex. Let \(\chi_n(t):=\frac{1}{2^nn!}\left[ (t^2-1)^n \right] ^{(n)}\) be the standardized Legendre polynomial of degree \(n\). We prove that \(\|P\|_{B_n}\geq\chi_n^{-1}\left(\frac{vol(B_n)}{vol(S)}\right).\) From this, we obtain the equivalence \(\theta_n(B_n)\) \(\asymp\) \(\sqrt{n}\). Also we estimate the constants from such inequalities and give the comparison with the similar relations for linear interpolation upon the \(n\)-dimensional unit cube. These results have applications in polynomial interpolation and computational geometry.
450-468 912
Abstract

An object shape analysis is a problem that is related to such areas as geometry, topology, image processing and machine learning. For analyzing the form, the deformation between the source and terminal form of the object is estimated. The most used form analysis model is the Large Deformation Diffeomorphic Metric Mapping (LDDMM) model. The LDDMM model can be supplemented with functional non-geometric information about objects (volume, color, formation time). The paper considers algorithms for constructing sets of barcodes for comparing diffeomorphic images, which are real values taken by persistent homology. A distinctive feature of the use of persistent homology with respect to methods of algebraic topology is to obtain more information about the shape of the object. An important direction of the application of persistent homology is the study invariants of big data. A method based on persistent cohomology is proposed that combines persistent homology technologies with embedded non-geometric information presented as functions of simplicial complexes. The proposed structure of extended barcodes using cohomology increases the effectiveness of persistent homology methods. A modification of the Wasserstein method for finding the distance between images by introducing non-geometric information was proposed. The possibility of the formation of barcodes of images invariant to transformations of rotation, shift and similarity is considered.

 



Creative Commons License
This work is licensed under a Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)