Mathematical models of distributed computations, based on the calculus of mobile processes (π-calculus) are widely used for checking the information security properties of cryptographic protocols. Since π-calculus is Turing-complete, this problem is undecidable in general case. Therefore, the study is carried out only for some special classes of π-calculus processes with restricted computational capabilities, for example, for non-recursive processes, in which all runs have a bounded length, for processes with a bounded number of parallel components, etc. However, even in these cases, the proposed checking procedures are time consuming. We assume that this is due to the very nature of the π -calculus processes. The goal of this paper is to show that even for the weakest model of passive adversary and for relatively simple protocols that use only the basic π-calculus operations, the task of checking the information security properties of these protocols is co-NP-complete.

This paper presents the ontology of the concurrent processes close to Hoare communicating sequential processes. It is the part of the intellectual system for supporting verification of behavioural properties of these processes. Our ontological representation of the processes is oriented both to the application of formal verification methods and to the extraction of information from technical documentation (by our previously developed system of information extraction from a natural language text). We describe the ontology classes and domains that define communicating concurrent processes. These processes are characterized by sets of local and shared variables, a list of actions on these variables which change their values, a list of channels for the process communication (which, in turn, are characterized by the type of reading messages, capacity, ways of writing and reading, and reliability), and also a list of communication actions for sending messages. In addition to the formal mathematical definition of classes and domains of the ontology, examples of descriptions of some ontological classes as well as typical properties and axioms for them are specified in the editor Prot ́eg ́e in the OWL language with the use of the inference rules in the SWRL language. The formal operational semantics of communicating processes is determined on their ontological representation and is given as a labelled transition system. It is reduced to the local operational semantics of separate process instances in the interleaving model. We specialize several types of processes from the subject domain of automatic control systems that model the typical functional elements of the automatic control system (sensors, comparators and regulators) as well as their combinations. The concepts of the specialized ontology are illustrated by the example of a control part for a bottle-filling system.

Formal modelling languages play a key role in the development of software: they enable users to specify functional requirements that serve as documentation as well; they enable users to prove the correctness of system properties, especially for critical systems. However, there is still an open question on how to map formal models to a specific programming language. In order to propose a solution, this paper presents a source-to-source mapping between Event-B models, a formal modelling language for reactive systems, and Eiffel programs, an Object Oriented (O-O) programming language. The mapping not only generates an actual Eiffel code of the Event-B model, but also translates model properties as contracts. The contracts follow the Design by Contract principle and are natively supported by the programming language. The mapping is implemented in the freely available Rodin plug-in EB2Eiffel. Thus, users can develop systems (i) starting with the modelling of functional requirements (properties) in Event-B, then (ii) formally proving the correctness of such properties in Rodin and finally (iii) by using EB2Eiffel to translate the model into Eiffel. In Eiffel, users can extend/customise the implementation of the model and formally prove it against the initial model. This paper also presents different Event-B models from the literature to test EB2Eiffel and its limitations. The article is published in the authors’ wording.

The project “Platform-independent approach to formal specification and verification of standard mathematical functions” is aimed onto the development of incremental combined approach to specification and verification of standard Mathematical functions like sqrt, cos, sin, etc. Platform-independence means that we attempt to design a relatively simple axiomatization of the computer arithmetics in terms of real arithmetics (i.e. the field \(\mathbb{R}\) of real numbers) but do not specify neither base of the computer arithmetics, nor a format of numbers representation. Incrementality means that we start with the most straightforward specification of the simplest case to verify the algorithm in real numbers and finish with a realistic specification and a verification of the algorithm in computer arithmetics. We call our approach combined because we start with manual (pen-and-paper) verification of the algorithm in real numbers, then use this verification as proof-outlines for a manual verification of the algorithm in computer arithmetics, and finish with a computer-aided validation of the manual proofs with a proof-assistant system (to avoid appeals to “obviousness” that are common in human-carried proofs).
In the paper, we apply our platform-independent incremental combined approach to specification and verification of the standard Mathematical square root function. Currently a computer-aided validation was carried for correctness (consistency) of our fix-point arithmetics and for the existence of a look-up table with the initial approximations of the square roots for fix-point numbers.

To ensure traffic safety of railway transport, non-destructive test of rails is regularly carried out by using various approaches and methods, including magnetic and eddy current flaw detection methods. An automatic analysis of large data sets (defectgrams) that come from the corresponding equipment is an actual problem. The analysis means a process of determining the presence of defective sections along with identifying structural elements of railway tracks on defectograms. This article is devoted to the problem of recognition of rail structural element images in magnetic and eddy current defectograms. Three classes of rail track structural elements are considered: 1) a bolted joint with straight or beveled connection of rails, 2) a butt weld of rails, and 3) an aluminothermic weld of rails. Images that cannot be assigned to these three classes are conditionally considered as defects and are placed in a separate fourth class. For image recognition of structural elements in defectograms a neural network is applied. The neural network is implemented by using the open library TensorFlow. To this purpose each selected (picked out) area of a defectogram is converted into a graphic image in a grayscale with size of 20 x 39 pixels.

Let \(C\) be a convex body and let \(S\) be a nondegenerate simplex in \({\mathbb R}^n\). Denote by \(\tau S\) the image of \(S\) under homothety with a center of homothety in the center of gravity of \(S\) and the ratio \(\tau\). We mean by \(\xi(C;S)\) the minimal \(\tau>0\) such that \(C\) is a subset of the simplex \(\tau S\). Define \(\alpha(C;S)\) as the minimal \(\tau>0\) such that \(C\) is contained in a translate of \(\tau S\). Earlier the author has proved the equalities \(\xi(C;S)=(n+1)\max\limits_{1\leq j\leq n+1}\max\limits_{x\in C}(-\lambda_j(x))+1\)  (if \(C\not\subset S\)), \(\alpha(C;S)=\sum\limits_{j=1}^{n+1} \max\limits_{x\in C} (-\lambda_j(x))+1.\)
Here \(\lambda_j\) are the linear functions that are called the basic Lagrange polynomials corresponding to \(S\).
The numbers \(\lambda_j(x),\ldots, \lambda_{n+1}(x)\) are the barycentric coordinates of a point \(x\in{\mathbb R}^n\). In his previous papers, the author investigated these formulae in the case when \(C\) is the \(n\)-dimensional unit cube \(Q_n=[0,1]^n\). The present paper is related to the case when \(C\) coincides with the unit Euclidean ball \(B_n=\{x: \|x\|\leq 1\},\) where \(\|x\|=\left(\sum\limits_{i=1}^n x_i^2 \right)^{1/2}.\) We establish various relations for \(\xi(B_n;S)\) and \(\alpha(B_n;S)\), as well as we give their geometric interpretation. For example, if \(\lambda_j(x)=l_{1j}x_1+\ldots+l_{nj}x_n+l_{n+1,j},\) then \(\alpha(B_n;S)=\sum\limits_{j=1}^{n+1}\left(\sum\limits_{i=1}^n l_{ij}^2\right)^{1/2}\). The minimal possible value of each characteristics \(\xi(B_n;S)\) and \(\alpha(B_n;S)\) for \(S\subset B_n\) is equal to \(n\). This value corresponds to a regular simplex inscribed into \(B_n\). Also we compare our results with those obtained in the case \(C=Q_n\).

In this paper, we consider the key problem of geometric modeling, connected with the construction of the intersection curves of surfaces. Methods for constructing the intersection curves in complex cases are found: by touching and passing through singular points of surfaces. In the first part of the paper, the problem of determining the tangent line of two surfaces given in parametric form is considered. Several approaches to the solution of the problem are analyzed. The advantages and disadvantages of these approaches are revealed. The iterative algorithms for finding a point on the line of tangency are described. The second part of the paper is devoted to methods for overcoming the difficulties encountered in solving a problem for singular points of intersection curves, in which a regular iterative process is violated. Depending on the type of problem, the author dwells on two methods. The first of them suggests finding singular points of curves without using iterative methods, which reduces the running time of the algorithm of plotting the intersection curve. The second method, considered in the final part of the article, is a numerical method. In this part, the author introduces a function that achieves a global minimum only at singular points of the intersection curves and solves the problem of minimizing this function. The application of this method is very effective in some particular cases, which impose restrictions on the surfaces and their arrangement. In conclusion, this method is considered in the case when the function has such a relief, that in the neighborhood of the minimum point the level surfaces are strongly elongated ellipsoids. All the images given in this article are the result of the work of algorithms on methods proposed by the author. Images are built in the author’s software environment.

Finding graph-edit distance (graph similarity) is an important task in many computer science areas, such as image analysis, machine learning, chemicalinformatics. Recently, with the development of process mining techniques, it became important to adapt and apply existing graph analysis methods to examine process models (annotated graphs) discovered from event data. In particular, finding graph-edit distance techniques can be used to reveal patterns (subprocesses), compare discovered process models. As it was shown experimentally and theoretically justified, exact methods for finding graph-edit distances between discovered process models (and graphs in general) are computationally expensive and can be applied to small models only. In this paper, we present and assess accuracy and performance characteristics of an inexact genetic algorithm applied to find distances between process models discovered from event logs. In particular, we find distances between BPMN (Business Process Model and Notation) models discovered from event logs by using different process discovery algorithms. We show that the genetic algorithm allows us to dramatically reduce the time of comparison and produces results which are close to the optimal solutions (minimal graph edit distances calculated by the exact search algorithm).

The ability to identify semantic relations between words has made a word2vec model widely used in NLP tasks. The idea of word2vec is based on a simple rule that a higher similarity can be reached if two words have a similar context. Each word can be represented as a vector, so the closest coordinates of vectors can be interpreted as similar words. It allows to establish semantic relations (synonymy, relations of hypernymy and hyponymy and other semantic relations) by applying an automatic extraction. The extraction of semantic relations by hand is considered as a time-consuming and biased task, requiring a large amount of time and some help of experts. Unfortunately, the word2vec model provides an associative list of words which does not consist of relative words only. In this paper, we show some additional criteria that may be applicable to solve this problem. Observations and experiments with well-known characteristics, such as word frequency, a position in an associative list, might be useful for improving results for the task of extraction of semantic relations for the Russian language by using word embedding. In the experiments, the word2vec model trained on the Flibusta and pairs from Wiktionary are used as examples with semantic relationships. Semantically related words are applicable to thesauri, ontologies and intelligent systems for natural language processing.