Research on formal methods of software development and verification focuses on building specifications using incremental and iterative development methodologies. The presence of several levels of specifications simplifies proving of properties, since it is possible to reuse the proofs that were performed for more abstract layers of the model. It is desirable to use the same models that were used for formal verification also in testing of real systems for compliance with the requirements set by these models. In practice, large software systems are described by multi-level models. There was no experience of using such models as the basis for testing and monitoring. The paper discusses various methods for developing multi-level models, new opportunities that can be obtained through a combination of functional specifications and implementation-level refinements, limitations that must be considered during testing and monitoring of real systems for compliance with multi-level models.

The paper considers the problem of verification of compliance between models representing the same system on different level of abstraction. The existing approaches are mostly based on refinement relation. But the models representing industrial systems are quite big and complex, while semantics gap between the level is quite big. As a result, the existing methods became too complex and labour intensive. The paper presents new verification techniques that targets to prove multimodel compliance in terms of individual trace semantics. The techniques assume that each model is verified, i.e. it is proved that starting from initial states of labelled transition system is not possible to reach unsafe states by using valid transitions. The first proposed technique allows to prove that the detailed model satisfies to requirements of the abstract model, i.e. reachable states of detailed model do not include states corresponding to unsafe states of the abstract model. The second proposed technique allows to prove that the detailed model satisfies to behaviour specification of the abstract model, i.e. all reachable transitions of the detailed model do not include transitions corresponding to invalid transitions of the abstract model. For each technique the correspondence relation is defined in terms of the models, i.e. the relations are formally defined and they can be used for analysis with interactive or automated provers. At the same time, there are some requirements to that relations that are expressed in terms of low level events that exist hypothetically only and can be analyzed theoretically only. As a result, the proposed techniques provides a reasonable approach to prove compliance between mulilevel models in more approachable way for industrial settings.

Models of mandatory integrity control in operating systems usually restrict accesses of active components of a system to passive ones and represent the accesses directly. This is suitable in case of monolithic operating systems whose components that provide access to resources are part of the trusted computing base. However, due to the sheer complexity of such components, it is extremely nontrivial to prove such a model to be adequate to the real system. KasperskyOS is a microkernel operating system that organizes access to resources via components that are not necessarily part of the trusted computing base. KasperskyOS implements a specifically developed mandatory integrity control model that takes such components into account. This paper formalizes the model and describes the process of automated proof of the model’s properties. For formalization, we use the Event-B language. We clarify parts specific to Event-B to make our presentation accessible to professionals familiar with discrete mathematics but not necessarily with Event-B. We reflect on the proof experience obtained in the Rodin platform.

Real-time partitioned operating systems meet the current avionics standard of reliable software; they are capable of responding to events from devices with an expected speed, as well as sharing processor time and memory between isolated partitions. Model-based Checking is a formal verification technique in which a software model is developed and then it is automatically checked for the compliance with formal requirements. This method allows proving the correct operation of the model on all possible input data, all possible ways of processes switching and interactions. In this article, we describe a formalized model of an open-source partitioned operating system POK. We implement the model in Promela language for SPIN tool with the purposes of formal verification using the Model Checking method. The model is designed to describe the behavior of: partition and process schedulers, system calls through a software interrupt, kernel libraries for working with synchronization primitives and processes awaiting, user code which consists of several processes in different partitions that are synchronized through a semaphore. The described approach can be used to verify the correct synchronization, the proper operation of the scheduler algorithms, and the accurate data access from different partitions by introducing the corresponding requirements in the form of formulas of the linear-time temporal logic.

The ergodic system keeps the time average is the same for almost all initial points. It is important for computer systems to prevent the degradation of the properties of the system over time. Ergodicity is especially required for mission-critical systems in demanding industries. Software development based on the functional safety requirements of the IEC 60880 category A standard is implemented only on newly created software that meets the most stringent requirements for nuclear power plants, it is impossible to use standard operating systems and compilers. For these purposes, a prototype of the runtime environment and application software of the command display system (DSCU) was implemented. The runtime was created based on the Active Oberon A2 system. A2 is a single-user multi-tasking system. Application area - industrial embedded real-time systems, high reliability systems. The DSKU execution environment is implemented by a significant revision of the minimum subset A2 to meet the requirements of the standard. The system of restrictions formed according to the requirements of the standard makes it possible to create computer systems with new properties. The use of these constraints leads to the proof that there is no possibility of the occurrence of the failures they cause and allows us to consider a computer system based on the presumption of non-ergodicity. This «via negative» approach is based on restrictions, the addition of which allows one to obtain new qualitative properties. The more restrictions, the greater the gain in system reliability and stability.

Nowadays, most of the services are moving online, which allows users to receive the service at any time. The high availability of the service leads to an increase in the number of users, which entails an increase in the load on the system. High load has a negative impact on system components, which can lead to malfunctions and data loss. To avoid this, the article discusses several design and monitoring approaches, the observance of which will help prevent system malfunctioning. The article describes the most popular way to distribute the area of responsibility of each service, in accordance with the DDD pattern, the use of which will allow you to separate the components of the system logically by use and physically when scaling the system. This approach will also be useful when scaling a team and allow developers to work independently on different system components without interfering with each other. The integration of new people into the project will also take the shortest possible time. When designing the system architecture, it is worth paying attention to the scheme of interaction between services. Using the CQRS pattern allows you to separate reading and writing into different components, which later allows the user to quickly receive a response from the system. Particular attention in the article is paid to monitoring the system, since with an increase in the size of the system, the time to search for errors in the system reaches a large amount of time, which can lead to a long unavailability of the system, which will entail the loss of clients. All the methods described in the article have been applied on many projects, for example, MTS POISK. Thanks to a properly designed system, it was possible to reduce the waiting time for a service response from two minutes to several seconds without losing the quality of the result, and a sophisticated system monitoring system allows you to monitor all processes within the system in real time and prevent accidents. As a result, at the beginning of the system design, special attention should be paid to the architecture, the issue of monitoring and testing the system. Subsequently, these temporary investments will reduce the risks of data loss and system unavailability.

Svace is a static analysis tool for bug detection in C/C++/Java source code. To analyze a program, Svace performs an intra-procedure analysis of individual functions, starting from the leaves of a call-graph and moving towards the roots, and uses summaries of previously analyzed procedures at call-cites. In this paper, we overview the approaches and techniques employed by Svace for the intra-procedural analysis. This phase is performed by an analyzer engine and an extensible set of detectors. The core engine employs a symbolic execution approach with state merging. It uses value numbering to reduce the set of symbolic expressions, maintains points-to relationship graph for memory modeling, and performs strong and weak updates of program values. Detectors are responsible for discovering and reporting bugs. They calculate different properties of program values using a variety of abstract domains. All detectors work simultaneously orchestrated by the engine. Svace analysis is unsound and employs a variety of heuristics to speed-up. We designed Svace to analyze big projects (several MLOCs) in just a few hours and report as many warnings as possible, while keeping a good quality of reports ≥ 65 of true positives). For example, Tizen 5.5 (20MLOC) analysis takes 8.6 hours and produces 18,920 warnings, more than 70% of which are true-positive.

The mathematical foundations of abstract interpretation provide a unified method of formalization and research of program analysis algorithms for a broad spectrum of practical problems. However, its practical usage for binary code analysis faces several challenges, of both scientific and engineering nature. In this paper we address some of those challenges. We describe an intermediate representation that is tailored to binary code analysis; unlike some other IRs it is still useable in system code analysis. To achieve this, we take into account the low-level specifics of how CPUs work; on the IR level this mostly pertains to modeling main memory in that accesses can fail, and addresses can alias. Further, we propose an infrastructure for carrying out abstract interpretation on top of the IR. The user needs to implement the abstract state and the transfer functions, and the infrastructure handles the rest: two executors are currently implemented, one for analysis of a single path, and one for fixed point analysis. Both executors handle interprocedural analysis internally, via inlining or using summaries, so the interpretations only consider only procedure at a time, which greatly simplifies implementation. The IR and the abstract interpretation framework are used together to define a model pipeline for a target instruction set architecture, consisting of a fetch stage, a decode stage, and an execute stage. A distinct fetch stage allows to model delay slots, hardware loops, etc. We currently have limited implementations for RISC-V and x86. The x86 implementation is evaluated in two experiments where concolic execution is used to automatically analyze a «crackme» program, both in dynamic (execution trace) and static (executable image) setting. In conclusion, we outline the future directions of our project.

The processes of globalization, the emergence and active development of cyberspace have led to the need to protect information transmitted in the framework of information exchange. Existing approaches to information protection, in particular its encryption, steganography, etc. from the point of view of information exchange have a number of unmasking features that, despite the undoubted reliability of these approaches, significantly reduce the secrecy of information transmission. The proposed article considers an approach that allows for the hidden transmission of protected information over open communication channels, by masking the transmitted information. The development of the proposed approach was carried out in stages. at the first stage, a method for masking the transmitted information was developed and patented. At the next stage, on the basis of the developed method, a functional model of client and server applications of the hidden information transmission complex is created. The transfer of masked information is proposed to be carried out using the developed protocol of hidden information transfer. The block diagram of the package of the proposed Protocol for transmitting hidden information, the implementation and use of the Protocol at the application level are presented in this paper. At the final stage, a software implementation of the proposed approach was developed and modeling of information exchange at different offset Windows was performed. the paper presents a functional model of the developed complex, a scheme of interaction of functional modules, and a block diagram of the proposed approach to masking the transmitted information. Increasing the secrecy of information transmission is provided by the procedure for converting a carrier message into a marker message by forming an offset window, as well as using an array of digital records to select the carrier message. The proposed approach allows you to use a smaller carrier message when increasing the window size and using a sliding window depending on the size of the information message, you can choose the optimal size of the carrier message and the offset window.

Topic modeling is an important and widely used method in the analysis of a large collection of documents. It allows us to digest the content of documents by examination of the selected topics. It has drawbacks such as a need to specify the number of topics. The topics can become too local or too global, depending on that number. Also, it does not provide a relation between local and global topics.  Here we present an algorithm and a computer program for the hierarchical rubrication of text documents. The program solves these problems by creating a hierarchy of automatically selected topics in which local topics are connected of the global topics. The program processes PDF documents split them into text segments, builds vector representations using word2vec model and stores them in a database. The vector embeddings are structured in the form of a hierarchy of automatically constructed categories.  Each category is identified by automatically selected keywords. The result is visualized in an interactive map. Traversing the hierarchy of topics is done by zooming the map. An analysis of the constructed hierarchy of categories allows us to evaluate the minimum and maximum depth of the hierarchy corresponding to a minimum and a maximum number of different topics contained in the collection of documents. The program was tested on documents on deep nuclear waste disposal.

This survey is dedicated to the task of network traffic classification, particularly to the use of machine learning algorithms in this task. The survey begins with the description of the task, its variations and possible uses in real-world problems. It then proceeds to the description of the methods used historically to solve this task, their limitations and evolution of traffic making machine learning the main way to solve the problem. Then the most popular machine learning algorithms used in this task are described, with the examples of research papers, providing the insight into their advantages and disadvantages in relation to this field. The task of feature selection is discussed, followed by the more global problem of acquiring the suitable dataset to use in the research; some examples of such popular datasets and their descriptions are provided. The paper concludes with the outline of the current problems in this research area to be solved.

Timed-Arcs Petri nets (TaPN-nets) are a time extension of Petri nets that allows assigning clocks to tokens. System of dynamic points on a metric graph (DP-systems) is another dynamical model that is studied in discrete geometry dynamics and motivated by study of localized Gaussian wave packets scattering on thin structures; as well, DP-systems could be utilized to overapproximate the dynamics of messages scattering in distributed systems. In the latter case, time-temporal properties of DP-systems become a matter of interest. However, there are no tools that enable us to analyse them. In this work, we provide a new approach to automated analysis of DP-systems using the translation of a DP-system into a TaPN-net which is implemented as a TAPAAL plugin. The translation let us use the comprehensive tool support for TaPN-nets (TAPAAL/UPPAAL) to analyze DP-systems dynamical characteristics expressed in TCTL language. We demonstrated how to express some of them and verify time-temporal properties of a DP-system using the suggested approach, and performed experiments to obtain empirical estimates of the tool performance.

The paper considers modeling of technical problems and problems of applied mathematics, their algorithms and programming. The characteristics of the numerical modeling of technical problems and applied mathematics are given: physical and technical experiments, energy, ballistic and seismic methods of I.V. Kurchatov, starting with mathematical methods of the 17-20th centuries, the first computers and computers. The analysis of the first technical problems and problems of applied mathematics, their modeling, algorithmization and programming using the A.A. Lyapunov graph-schematic language, address language and programming languages is given. Numerical methods are presented, implemented under the guidance of A.A. Dorodnitsyn, A.A. Samarsky, O.M. Belotserkovsky and other scientists on modern supercomputers. Examples of mathematical modeling of the biological problem of eye treatment and the subject of «Computational geometry» on the Internet are given.

In this paper, we compare two approaches to describe the dynamics of flows on mountain slopes using the depth-averaged equations of continuum mechanics and using the complete, not depth-averaged, equations of continuum mechanics for three-dimensional modeling. Using these two approaches, a simulation of an experimental slush flow in the tank and the interaction of the flow with dam barrier protection was carried out. Numerical solutions are compared with experimental data. Also, both approaches are applied to the calculation of an avalanche in the 22nd avalanche cite of Mount Yukspor (Khibiny). Avalanche run-out distance and the shape of the avalanche deposits are compared with field data obtained from the measurement of a real avalanche. In the course of a numerical experiment, distributions of such quantities as flow velocity, depth, density, molecular and turbulent viscosity, values of the density of turbulent kinetic energy, dissipation of turbulent kinetic energy, and shear stress at the bottom of the flow were obtained. Using the obtained data a mathematical model is developed to describe the entrainment of the underlying material by the flow during slope erosion and the deposition of the flow material on the slope. To implement the obtained mathematical model, the architecture of the multiphaseEulerChangeFoam solver was developed, which implements a three-phase multi-velocity model with phase exchange between the material of the underlying surface and the material of the flow. The classic solver multiphaseEulerFoam from the OpenFOAM package is taken as a basis for the developed solver.

Tidal forcing excites internal waves in the bulk of the ocean. Deep ocean is an example of a system with continuous stratification subject to large-scale periodic forcing. Owing to specific dispersion relation of internal waves, the domains bounded by sloping boundaries may support wave patterns with wave rays converging to closed trajectories (geometric attractors) as result of iterative focusing reflections. Previously the behavior of kinetic energy in wave attractors has been investigated in two-dimensional domain with comparable depth and length. As the geometric aspect ratio of the domain increases, the dynamic pattern of energy focusing may significantly evolve both in laminar and turbulent regimes. The present paper shows that the energy density in domains with large aspect ratio can significantly increase. In numerical simulations the input forcing has been introduced at global scale by prescribing small-amplitude deformations of the upper bound of the liquid domain. The evolution of internal wave motion in such system has been computed numerically for different values of the forcing amplitude. The behavior of the large-aspect-ratio system has been compared to the well-studied case of the system with depth-to-length ratio of order unity. A number of most typical situations has been analysed in terms of behavior of integral mechanical quantities such as total dissipation, mean kinetic energy and energy fluctuations in laminar and turbulent cases.