An approach to estimate feasibility of a real-time multi-task application with various combinations of the scheduling mode and the protocol of access to shared informational resources when run on a multi-core platform is described. The application structure is specified through a simple formalized profile consisting of segments of three types and specifying access to informational resources shared among application tasks, the amount of the required computing resource being estimated for each segment. The approach is based on the notion of application density introduced by the authors, which characterizes the use of computational resource by this application and is derived from estimation of the application feasibility for various values of processor performance and the number of its cores in case of a multi-core platform. The overall structure of a simulation tool for estimation of the task response time (and therefore, application feasibility) is described, which provides more exact data compared to the known analytical methods where they are applicable. Two dissimilar implementations of this tool were developed and run on a number of benchmarks, including Liu-Layland configurations specified in the described formalism for application structure; the results in form of charts are presented along with their analysis and interpretation. The suggested approach allows to indentify an optimal combination of the scheduling mode and access protocol for the given multi-task application structure.

This article presents a method for the analysis and verification of Use Case Maps (UCM) models with scenario control structures — protected components and failure handling constructs. UCM models are analyzed and verified with the help of coloured 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.

In the paper, we describe a verification method for families of distributed systems generated by context-sensitive network grammar of a special kind. This grammar includes special non-terminal symbols, so called quasi-terminals, which uniquely correspond to grammar terminals. These quasi-terminals specify processes which are merging of base system processes, in contrast to simple nonterminals which specify networks of parallel compositions of the processes. The method is based on model checking technique and abstraction. An abstract representative model for a family of systems depends on their specification grammar and system properties to be verified. This model simulates the behaviour of the systems in such a way that the properties which hold for the representative model are satisfied for all these systems. The properties of the representative model can be verified by model checking method. The properties of a generated system are specified by universal branching time logic ∀CTL with finite deterministic automata as atomic formulas. We show the use of this method for verification of some properties of a multiagent system for conflict resolution, in particular, for context-dependent disambiguation in ontology population. We also suggest that this approach should be used for verification of computations on sub-grids which are sub-graphs of computation grids. In particular, we consider the computation of parity of the active processes number in a sub-grid.

In this paper, we consider the problem of deriving a cascade parallel composition of timed finite state machines (TFSMs). In order to build such a composition we can derive the corresponding binary parallel compositions step-by-step. It is known that if each component of a binary parallel composition is TFSM with output delays that are natural numbers or zero, the result of the composition can be TFSM with output delays that are sets of linear functions. So, the problem of deriving a cascade composition of TFSMs with constant output delays is reduced to the problem of deriving several binary parallel compositions of TFSMs with output delays that are sets of constants or linear functions. In this work, we refine the definition of TFSM and pay special attention to the description of an output delay function. As a tool for deriving the composition we consider balm-ii, and in consequence we study the ways of constructing the corresponding automaton for TFSM with output delays as a set of linear functions. We suggest a new procedure for constructing such an automaton, and unlike the known procedure our procedure does not require further determinization of the derived automaton. Moreover, we describe step by step how to build the composition of the derived automaton by using balm-ii, and discuss a procedure of reverse transformation from the global automaton to TFSM in case when the components are TFSMs with output delays that are sets of linear functions. We use an application example in order to illustrate derivation of the cascade parallel composition of TFSMs.

Extended Finite State Machines (EFSMs) are widely used when deriving tests for checking functional requirements for software implementations. However, the fault coverage of tests covering appropriate paths, variables, etc. of the specification EFSM, remains rather obscure and such tests do not detect many functional faults in EFSM implementations. In this paper, an approach is proposed for deriving complete tests with respect to functional faults of a proper Java EFSM implementation. First, an initial test suite derived against the specification EFSM is checked with respect to faults generated by a µJava tool. Since the EFSM software implementation is template based, each undetected fault can be easily mapped into a mutant EFSM of the specification machine. Thus, a distinguishing sequence is derived for two Finite State Machines modeling two EFSMs instead of deriving such a sequence for two programs. If the corresponding FSMs are too complex or cannot be completely derived, a test suite can be incomplete. However, the performed experiments clearly show that a test suite extended by such distinguishing sequences detects much more functional faults in software implementations of a system whose behaviour is described by the given EFSM.

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 the transducer, next the 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.

The paper is dedicated to the specification of the structure and the behaviour of soft-ware libraries. It describes the existing problems of libraries specifications. A brief overview of the research field concerned with formalizing the specification of libraries and library functions is presented. The requirements imposed on the formalism designed are established; the formalism based on these requirements allows specifying all the properties of the libraries needed for automation of several classes of problems: defects detection in the software, migration of applications into a new environment, gen-eration of software documentation. The requirements on the language tools based on the developed formalism are proposed. The conclusion defines potential directions for further research.

This paper comprises the development and implementation of systems using the concept of Internet of Things. In terms of active development of industries, use the concept of the Internet of Things, the information security problem is urgent. To create a protected module of information-telecommunication system which implements the Internet of Things concept, it is important to take into account all its aspects. To determine relevant threats, it is necessary to use the detailed risk analysis according to existing GOST standards when choosing protection measures, one must rely on identified relevant threats. Actual threats and necessary protective actions are determined in this paper for implementation of Smart House computer appliance module, in order to develop a protected part of Smart House, which is necessary for realization of room access control. We solved the following tasks in the work, namely, a description of the system Smart Home, a description of steps and evaluation system security Smart Home; implementation of hardware assembly and writing a code for the selected fragment of the system; safety evaluation of the selected fragment Smart House and identification of actual threats; make recommendations to counter current threats; software implementation of one of the most urgent threats and software implementation of protective measures for a selected threat. A feature of the work is an integrated approach to the design with the use of the intruder models, analysis of the system’s assets and evaluation of their security.

We plan to create a method of clustering a social network graph. For testing the method there is a need to generate a graph similar in structure to existing social networks. The article presents an algorithm for the graph distributed generation. We took into account basic properties such as power-law distribution of the users communities number, dense intersections of the 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 communities number parameter rather than on the connected users number as it is done in other works. It is connected with a peculiarity of progressing the existing social network structure. There are properties of its graph in the paper. We described a table containing the variables needed for the algorithm. A step-by-step generation algorithm was compiled. Appropriate mathematical parameters were calculated for it. A generation is performed in a distributed way by Apache Spark framework. It was described in detail how the tasks division with the help of this framework runs. The Erdos-Renyi model for random graphs is used in the algorithm. It is the most suitable and easy one to implement. The main advantages of the created method are the small amount of resources in comparison with other similar generators and execution speed. Speed is achieved through distributed work and the fact that in any time network users have their own unique numbers and are ordered by these numbers, so there is no need to sort them out. The designed algorithm will promote not only the efficient clustering method creation. It can be useful in other development areas connected, for example, with the social networks search engines.

We study the bifurcation of the equilibrium states of periodic solutions for the Mackey– Glass equation. This equation is considered as a mathematical model of changes in the density of white blood cells. The equation written in dimensionless variables contains a small parameter at the derivative, which makes it singular. We applied the method of uniform normalization, which allows us to reduce the study of the solutions behavior in the neighborhood of the equilibrium state to the analysis of the countable system of ordinary differential equations. We poot out the equations in ”fast” and ”slow” variables from this system. Equilibrium states of the ”slow” variables equations determine the periodic solutions. The analysis of equilibrium states allows us to study the bifurcation of periodic solutions depending on the parameters of the equation and their stability. The possibility of simultaneous bifurcation of a large number of stable periodic solutions is shown. This situation is called the multistability phenomenon.

Dynamic reconfigurations can modify the architecture of component-based systems without incurring any system downtime. In this context, the main contribution of the present article is the establishment of correctness results proving component-based systems reconfigurations using graph grammars. New 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. Then, after enriching the model with interpreted configurations and reconfigurations in a consistency compatible manner, a simulation relation is exploited to validate component systems’ implementations. This sound implementation is illustrated on a cloud-based multitier application hosting environment managed as a component-based system.

The paper is devoted to analysis of methods for automatic generation of a specialized thesaurus. The main algorithm of generation consists of three stages: selection and preprocessing of a text corpus, recognition of thesaurus terms, and extraction of relations among terms. Our work is focused on exploring methods for semantic relation extraction. We developed a test bench that allow to test well-known algorithms for extraction of synonyms and hypernyms. These algorithms are based on different relation extraction techniques: lexico-syntactic patterns, morpho-syntactic rules, measurement of term information quantity, general-purpose thesaurus WordNet, and Levenstein distance. For analysis of the result thesaurus we proposed a complex assessment that includes the following metrics: precision of extracted terms, precision and recall of hierarchical and synonym relations, and characteristics of the thesaurus graph (the number of extracted terms and semantic relationships of different types, the number of connected components, and the number of vertices in the largest component). The proposed set of metrics allows to evaluate the quality of the thesaurus as a whole, reveal some drawbacks of standard relation extraction methods, and create more efficient hybrid methods that can generate thesauri with better characteristics than thesauri generated by using separate methods. In order to illustrate this fact, one of such hybrid methods is considered in the paper. It combines the best standard algorithms for hypernym and synonym extraction and generates a specialized medical thesaurus. The hybrid method leaves the thesaurus quality on the same level and finds more relations between terms than well-known algorithms.

In this paper, we consider a singularly perturbed system of two differential equations with delay which simulates two coupled oscillators with nonlinear feedback. Feedback function is assumed to be finite, piecewise continuous, and with a constant sign. In this paper, we prove the existence of relaxation periodic solutions and make conclusion about their stability. With the help of the special method of a large parameter we construct asymptotics of the solutions with the initial conditions of a certain class. On this asymptotics we build a special mapping, which in the main describes the dynamics of the original model. It is shown that the dynamics changes significantly with the decreasing of coupling coefficient: we have a stable homogeneous periodic solution if the coupling coefficient is of unity order, and with decreasing the coupling coefficient the dynamics become more complex, and it is described by a special mapping. It was shown that for small values of the coupling under certain values of the parameters several different stable relaxation periodic regimes coexist in the original problem.

We consider chains of identical diffusive weakly coupled oscillation systems with different conditions on coupling on a chain bound. We suppose that every interacting oscillator undergoes Andronov–Hopf bifurcation, and the coefficient of coupling is proportional to the supercriticality value. For this case on a stable integral manifold of the system a normal form is constructed for which, in case of three oscillators interact, we can study the simplest stationary states and their phase transformations. As the coupling parameter changes, for the uniform stationary state corresponding to the uniform cycle of the problem there can be two cases, in the former case it loses stability with the emergence of two stable nonuniform states, and in the latter one it merges with two unstable nonuniform states and transfers to them its stability. For the stationary state corresponding to oscillations in antiphase two cases can be also distinguished. In the first one, this stationary state becomes stable due to the contraction of a stable limit cycle of the system into it (Andronov–Hopf bifurcation), and in the second case it becomes stable after branching from it an unstable limit cycle. If there are four oscillators in the chain, the system of phase difference for a small coupling coefficient was studied.