• A
  • A
  • A
  • ABC
  • ABC
  • ABC
  • А
  • А
  • А
  • А
  • А
Regular version of the site
Of all publications in the section: 114
Sort:
by name
by year
Article
Хорошилов А. В., Щепетков И. Труды Института системного программирования РАН. 2017. Т. 29. № 3. С. 43-56.
Added: Aug 28, 2017
Article
Semenkovich S. A., Kolekonova O. I., Degtiarev K. Y. Proceedings of the Institute for System Programming of the RAS. 2017. Vol. 29. No. 5. P. 19-38.

Several known methods allow to estimate the overall effort(s) to be used up for the software development. The approach based on story points is preferable and quite common in the context of Sсrum agile development methodology. However, it might be rather challenging for people, who are new to this methodology or to a specific Scrum team to estimate the amount of work with story points. The proposed approach involves estimation of features on the basis of linguistic terms that are both habitual and clear for everyone. The presented fuzzy inference system (Mamdani’s model) makes it possible to calculate story points using people’s opinions expressed as sentences in natural language – the study shows empirically that beginners to Scrum methodology consider the proposed approach to be more convenient and easier in use than the ‘plain’ story points estimation. Also, four groups of people with different levels of qualification in Scrum were asked to estimate several features of a certain project using the developed approach and common story points approach to prove the relevance of the approach – it was shown that the results of basic story points estimation for Scrum experts differ slightly from the results revealed by proposed approach, while for Scrum beginners such difference is significant.To the opinion of authors, the proposed approach may allow to adapt to Scrum more smoothly, with better understanding of what is implied by story points, grasping the general idea and learning faster their use in practice.

Added: Oct 20, 2018
Article
Avdoshin S. M., Beresneva E. Proceedings of the Institute for System Programming of the RAS. 2018. Vol. 30. No. 3. P. 233-250.

Vehicle Routing Problem (VRP) is one of the most widely known questions in a class of combinatorial optimization problems. It is concerned with the optimal design of routes to be used by a fleet of vehicles to serve a set of customers. In this study we analyze Capacitated Vehicle Routing Problem (CVRP) – a subcase of VRP, where the vehicles have a limited capacity. CVRP is mostly aimed at savings in the global transportation costs. The problem is NP-hard, therefore heuristic algorithms which provide near-optimal polynomial-time solutions will be considered instead of the exact ones. The aim of this article is to make a survey on mathematical formulations of CVRP and on methods for solving each type of this problem. The first part presents a general information about the problem and restrictions of this work. In the second part, the classical mathematical formulations of CVRP are described. In the third part, a classification of most popular subcases of CVRP is given, including description of additional constraints with their math formulations. This section also includes most perspective methods that can be applied for solving special types of CVRP. The forth part contains an important note about the most powerful algorithm LKH-3. Finally, the fourth part consists of table with solving techniques for each subproblem and of scheme with basic problems of the CVRP class and their interconnections. 

Added: Jul 10, 2018
Article
Tatarnikov A., Kamkin A., Проценко А. С. Proceedings of the Institute for System Programming of the RAS. 2015. Vol. 27. No. 3. P. 125-138.
A memory subsystem is one of the key components of a microprocessors. It consists of a number of storage devices (instruction buffers, address translation buffers, multilevel cache memory, main memory, and others) organized into a complex hierarchical structure. Huge state space of a memory subsystem makes its functional verification extremely labor consuming. Nowadays, the main approach to functional verification of microprocessors at a system level is simulation with the use of automatically generated test programs. In this paper, a method for generating test programs for functional verification of microprocessors’ memory management units is proposed. The approach is based on formal specification of memory access instructions, namely load and store instructions, and formal specification of memory devices, such as cache units and address translation buffers. The use of formal specifications allows automating development of test program generators and makes functional verification systematic due to clear definition of testing goals. In the suggested approach, test programs are constructed by using combinatorial techniques, which means that stimuli (sequences of loads and stores) are created by enumerating all feasible combinations of instructions, situations (instruction execution paths) and dependencies (sets of conflicts between instructions). It is of importance that test situations and dependencies are automatically extracted from the formal specifications. The approach was used in several industrial projects on verification of MIPS microprocessors and allowed to discover critical bugs in the memory management mechanisms.
Added: Dec 10, 2017
Article
Shugurov I., Mitsyuk A. A. Proceedings of the Institute for System Programming of the RAS. 2016. Vol. 28. No. 3. P. 103-122.

Process mining is a relatively new research field, offering methods of business processes analysis and improvement, which are based on studying their execution history (event logs). Conformance checking is one of the main sub-fields of process mining. Conformance checking algorithms are aimed to assess how well a given process model, typically represented by a Petri net, and a corresponding event log fit each other. Alignment-based conformance checking is the most advanced and frequently used type of such algorithms.  This paper deals with the problem of high computational complexity of the alignment-based conformance checking algorithm. Currently, alignment-based conformance checking is quite inefficient in terms of memory consumption and time required for computations. Solving this particular problem is of high importance for checking conformance between real-life business process models and event logs, which might be quite problematic using existing approaches. MapReduce is a popular model of parallel computing which allows for simple implementation of efficient and scalable distributed calculations. In this paper, a MapReduce version of the alignment-based conformance checking algorithm is described and evaluated. We show that conformance checking can be distributed using MapReduce and can benefit from it. Moreover, it is demonstrated that computation time scales linearly with the growth of event log size.

Added: Sep 12, 2016
Article
Gordenko M., Beresneva E. Proceedings of the Institute for System Programming of the RAS. 2018. Vol. 30. No. 3. P. 251-270.

This article presents the results of applying various methods of system analysis (CATWOE, Rich Picture, AHP, Fuzzy AHP) to evaluation of teaching assistants. The soft and hard methods were applied. Methods of system analysis are considered as an example at the Higher School of Economics (HSE) in program “Teaching assistant”. The article shows the process of interaction of teaching assistants with students and faculty in the form of Rich Picture. Selection and analysis of criteria for the evaluation of training assistants are carried out. Three groups of criteria were defined: professional skills, communicating skills, personal qualities. Each group has some subcriteria, which were defined in brainstorm. Its own method was determined, which immediately allow drop some assistants. In addition, the application of the methods AHP and Fuzzy AHP type-2 to evaluate teaching assistants is considered. The strengths and weaknesses of each method are revealed. It is also shown that, despite the power of the methods of system analysis, it is necessary to use common sense and logic. Do not rely only on the numbers obtained by the methods of system analysis. In the process of work, the best teaching assistant is selected, and the group of the best teaching assistants is defined. 

Added: Jul 10, 2018
Article
Pavlov V., Novikov B. Proceedings of the Institute for System Programming of the RAS. 2018. Vol. 30. No. 1. P. 137-160.

After huge amount of big scientific data, which needed to be stored and processed, has emerged, the problem of large multidimensional arrays support gained close attention in the database world. Devising special database engines with support of array data model became an issue. Development of a well-organized database management system which stands on completely uncommon data model required performing the following tasks: formally defining a data model, building a formal algebra operating on objects from the data model, devising optimization rules on logical level and then on the physical one. Those tasks has already been completed by creators of different array databases. In this paper array formalization, core algebra and optimization techniques are revised using examples of AML, RasDaMan, SciDB – developed array database management systems with different algebras and optimization approaches.

Added: Mar 15, 2019
Article
Burdonov I. B., Kossatcheva A. S., Kuliamin V. et al. Proceedings of the Institute for System Programming of the RAS. 2018. Vol. 30. No. 1. P. 69-88.

The paper provides a review of distributed graph algorithms research conducted by authors. We consider an asynchronous distributed system model represented by a strongly connected directed rooted graph with bounded edge capacity (in a sense that only a bounded number of messages can be sent through an edge in a given time interval). A graph can be static or dynamic, i.e. changing. For a static graph we propose a spanning (in- and out-) tree construction algorithm of time complexity O(n/k+d)O(n/k+d), requiring O(ndlogΔ+)O(ndlog⁡Δ+)message size and the same size of memory of each computing agent located in graph vertex, where nn is the number of vertices of the graph, kk is the capacity of an edge, dd is the maximum length of simple path in the graph, Δ+Δ+ is the maximum outdegree of the vertices. The spanning trees constructed can be used in distributed computation of a function of the multiset of values assigned to graph vertices in a time not greater than 3d3d. In a dynamic graph we suppose that k=1k=1 and an edge can appear, disappear, or change its end. We propose a dynamic graph monitoring algorithm than delivers information on any change to the root of the graph in O(n)O(n) or O(d)O(d) after the changes are stopped. We also propose graph exploration and marking algorithm with time complexity O(n)O(n). The marking provided by it is used in distributed computation of a function of the multiset of values assigned to dynamic graph vertices, which can be performed in time O(n2)O(n2)with messages of size O(logn)O(log⁡n) or in time O(n)O(n) with messages of size O(nlogn)O(nlog⁡n).

Added: Aug 11, 2018
Article
Samokhvalov D., Dworzanski L. W. Proceedings of the Institute for System Programming of the RAS. 2016. Vol. 28. No. 3. P. 65-84.

Nested Petri net formalisms is an extension of coloured Petri net formalism that uses Petri Nets as tokens. The formalism allows creating comprehensive models of multi-agent systems, simulating, verifying and analyzing them in a formal and rigorous way. Multi-agent systems are found in many different fields — from safety critical systems to everyday networks of personal computational devices; and, their presence in the real world in increasing with the increasing number of mobile computational devices. While several methods and tools were developed for modelling and analysis of NP-nets models, the synthesis part of multi-agent systems development via NP-nets is still under active development. The widely used method of automatic generation of target system code from designed and verified formal models ensures obtaining correct systems from correct models. In this paper, we demonstrate how Nested Petri net formalism can be applied to model search-and-rescue coordination systems and automatically generate implementation in the form of the executable code for event-driven systems based on the Telegram platform. We augment the NP-nets models with Action Language annotation, which enables us to link transition firings on the model level to Telegram Bot API calls on the implementation level. The suggested approach is illustrated by the example annotated model of a search and rescue coordination system

Added: Sep 15, 2016
Article
Avdoshin S.M., Lazarenko A.V. Proceedings of the Institute for System Programming of the RAS. 2018. Vol. 30. No. 1. P. 89-101.

Bitcoin is the most popular cryptocurrency on the planet. It relies on strong cryptography and peer-to-peer network. Bitcoin is gaining more and more popularity in criminal society. That is why Bitcoin is often used as money laundering tool or payment method for illegal products and services. In this paper we explore various methods for Bitcoin users deanonimization, which is an important task in anti-money laundering process and cybercrime investigation.

Added: Mar 25, 2018
Article
Fedotov A. N., Kaushan V. V., Gaysaryan S. S. et al. Proceedings of the Institute for System Programming of the RAS. 2017. Vol. 29. No. 6. P. 151-162.

Approaches for code execution using program vulnerabilities are considered in this paper. Particularly, ways of code execution using buffer overflow on stack and on heap, using use-after-free vulnerabilities and format string vulnerabilities are examined in section 2. Methods for automatic generation input data, leading to code execution are described in section 3. This methods are based on dynamic symbolic execution. Dynamic symbolic execution allows to gain input data, which leads program along the path of triggering vulnerability. The security predicate is an extra set of symbolic formulas, describing program's state in which code execution is possible. To get input data, leading to code execution, path and security predicates need to be united, and then the whole system should be solved. Security predicates for pointer overwrite, function pointer overwrite and format string vulnerability, that leads to stack buffer overflow are presented in the paper. Represented security predicates were used in method for software defect severity estimation. The method was applied to several binaries from Darpa Cyber Grand Challenge. Testing security predicate for format string vulnerability, that leads to buffer overflow was conducted on vulnerable version of Ollydbg. As a result of testing it was possible to obtain input data that leads to code execution.

Added: Aug 10, 2018
Article
N. Nikitina, A. Mitsyuk. Proceedings of the Institute for System Programming of the RAS. 2015. Vol. 27. No. 3. P. 219-236.

Process models and graphs are commonly used for modeling and visualization of processes. They may represent sets of objects or events linked with each other in some way. Wide use of models in such languages engenders necessity of tools for creating and editing them. This paper describes the model editor which allows for dealing with classical graphs, Petri nets, finite-state machines and their systems. Additionally, the tool has a list of features like simulation of Petri nets, import and export of models in different storage formats. Carassius is a modular tool which can be extended with, for example, new formalisms.  In the paper one can find a detailed description of a couple of layout algorithms that can be used for visualizing Petri nets and graphs. Carassius might be useful for educational and research purposes because of its simplicity, range of features and variety of supported notations.

Added: Aug 18, 2015
Article
Ivanov S. Y., Kalenkova A. A. Proceedings of the Institute for System Programming of the RAS. 2015. Vol. 27. No. 3. P. 255-266.

Comparing business process models is one of the most significant challenges for business and systems analysts. The complexity of the problem is explained by the fact there is a lack of tools that can be used for comparing business process models. Also there is no universally accepted standard for modeling them. EPC, YAWL, BPEL, XPDL and BPMN are only a small fraction of available notations that have found acceptance among developers. Every process modeling standard has its advantages and disadvantages, but almost all of them comprise an XML schema, which defines process serialization rules. Due to the fact that XML naturally represents hierarchical and reference structure of business process models, these models can be compared using their XML representations. In this paper we propose a generic comparison approach, which is applicable to XML representations of business process models. Using this approach we have developed a tool, which currently supports BPMN 2.0 [1] (one of the most popular business process modeling notations), but can be extended to support other business process modeling standards.

Added: Sep 17, 2015
Article
Зеленов С. В., Карнов А. Труды Института системного программирования РАН. 2017. Т. 29. № 4. С. 191-202.
Added: Nov 8, 2017
Article
Avdoshin S.M., Lazarenko A.V. Proceedings of the Institute for System Programming of the RAS. 2016. Vol. 28. No. 3. P. 21-34.
Added: Aug 31, 2016
Article
Mallachiev K., Pakulin N. V., Khoroshilov A. V. Proceedings of the Institute for System Programming of the RAS. 2016. Vol. 28. No. 2. P. 181-192.

Modern airliners such as Airbus A320, Boeing 787, and Russian MS-21 use so called Integrated Modular Avionics (IMA) architecture for airborne systems. This architecture is based on interconnection of devices and on-board computers by means of uniform real-time network. It allows significant reduction of cable usage, thus leading to reducing of takeoff weight of and airplane. IMA separates functions of collecting information (sensors), action (actuators), and avionics logic implemented by applied avionics software in on-board computers. International standard ARINC 653 defines constraints on the underlying real-time operation system and programming interfaces between operating system and associated applications. The standard regulates space and time partitioning of applied IMA-related tasks. Most existing operating systems with ARINC 653 support are commercial and proprietary software. In this paper, we present JetOS, an open source real-time operating system with complete support of ARINC 653 part 1 rev 3. JetOS originates from the open source project POK, created by French researchers. At that time POK was the only one open source OS with at least partial support for ARINC 653. Despite this, POK was not feasible for practical usage: POK failed to meet a number of fundamental requirements and was executable in emulator only. During JetOS development POK code was significantly redesigned. The paper discusses disadvantages of POK and shows how we solved those problems and what changes we have made in POK kernel and individual subsystems. In particular we fully rewrote real-time scheduler, network stack and memory management. Also we have added some new features to the OS. One of the most important features is system partitions. System partition is a specialized application with extended capabilities, such as access to hardware (network card, PCI controller etc.) Introduction of system partitions allowed us moving large subsystems out of the kernel and limiting the kernel to the minimal functionality: context switching, scheduling and message pass. In particular, we have moved network subsystem to system partition. This moving reduces kernel size and potentially reduces probability on having bug in kernel and simplifies verification process. 

Added: Aug 11, 2018
Article
Asryan S. A., Gaysaryan S. S., Kurmangaleev S. F. et al. Proceedings of the Institute for System Programming of the RAS. 2018. Vol. 30. No. 3. P. 7-20.

The article describes new method of use after free bug detection using program dynamic analysis. In memory-unsafe programming languages such as C/C++ this class of bugs mainly accurse when program tries to access specific area of dynamically allocated memory that has been already freed. This method is based on combination of two basic components. The first component tracks all memory operations through dynamic binary instrumentation and searches for inappropriate memory access. It preserves two sets of memory address for all allocation and free instructions. Using both sets this component checks whether current memory is accessible through its address or it has been already freed. It is based on dynamic symbolic execution and code coverage algorithm. It is used to maximize the number of execution paths of the program. Using initial input, it starts symbolic execution of the target program and gathers input constraints from conditional statements. The new inputs are generated by systematically solving saved constraints using constraint solver and then sorted by number of basic blocks they cover. Proposed method detects use after free bugs by applying first component each time when second one was able to open new path of the program. It was tested on our synthetic tests that were created based on well-known use after free bug patterns. The method was also tested on couple of real projects by injecting bugs on different levels of execution.

Added: Aug 10, 2018
Article
Nurmukhametov A. R., Zhabotinskiy E. A., Kurmangaleev S. F. et al. Proceedings of the Institute for System Programming of the RAS. 2017. Vol. 29. No. 6. P. 163-182.

Program vulnerabilities are a serious security threat. It is important to develop defenses preventing their exploitation, especially with a rapid increase of ROP attacks. State of the art defenses have some drawbacks that can be used by attackers. In this paper we propose fine-grained address space layout randomization on program load that is able to protect from such kind of attacks. During the static linking stage executable and library files are supplemented with information about function boundaries and relocations. A system dynamic linker/loader uses this information to perform functions permutation. The proposed method was implemented for 64-bit programs on CentOS 7 operating system. The implemented method has shown good resistance to ROP attacks based on two metrics: the number of survived gadgets and the exploitability estimation of ROP chain examples. The implementation presented in this article is applicable across the entire operating system and has shown 1.5 % time overhead. The working capacity of proposed approach was demonstrated on real programs. The further research can cover forking randomization and finer granularity than on the function level. It also makes sense to implement the randomization of short functions placement, taking into account the relationships between them. The close arrangement of functions that often call each other can improve the performance of individual programs.

Added: Aug 10, 2018
Article
Turdakov D., Aleksiyants A., Borisenko O. et al. Proceedings of the Institute for System Programming of the RAS. 2015. Vol. 27. No. 5. P. 35-48.

In this paper the problem of creating virtual clusters in clouds for big data analysis with Apache Hadoop and Apache Spark is discussed. Both clouds and MapReduce models are popular nowadays for a bunch of reasons: cheapness and efficient big data analysis respectively. For these thoughts, having an open source solution for building clusters is important. The article gives an overview on existing methods for Apache Spark cluster creation in clouds. We consider two open source cloud engines OpenStack and Eucalyptus and the most popular proprietary cloud service Amazon Web Services and examine cloud related features presented by these systems. Afterwards, we regard possible ways of creating virtual clusters for big data processing in OpenStack and describe their pros and cons. In the second part we describe in details one of these solutions that uses service Sahara. Sahara represents a cluster management system for OpenStack and it is used for setting up virtual clusters and executing MapReduce jobs. Sahara did not support contemporary versions of Apache Spark. The article introduces the results of our work that led to a Sahara modification, describes its idea and implementation details. By virtue of our modification, Sahara is able to create and use virtual clusters with contemporary versions of Apache Spark in OpenStack clouds.

Added: Sep 13, 2016
Article
I. Shugurov, A. Mitsyuk. Proceedings of the Institute for System Programming of the RAS. 2015. Vol. 27. No. 3. P. 237-254.

This paper is dedicated to a tool whose aim is to facilitate process mining experiments and evaluation of the repair algorithms. Process mining is a set of approaches which provides solutions and algorithms for discovery and analysis of business process models based on event logs. Process mining has three main areas of interest: model discovery, conformance checking and enhancement. The paper focuses on the latter. The goal of enhancement process is to refine an existing process model in order to make it adhere event logs. The particular approach of enhancement considered in the paper is called decomposed model repair. Although the paper is devoted to the implementation part of the approach, theoretical preliminaries essential for domain understanding are provided. Moreover, a typical use case of the tool is shown as well as guides to extending the tool and enriching it with extra algorithms and functionality. Finally, other solutions which can be used for implementation of repair schemes are considered, pros and cons of using them are mentioned.

Added: Aug 18, 2015
Article
Tatarnikov A. Proceedings of the Institute for System Programming of the RAS. 2016. Vol. 28. No. 4. P. 77-98.

Test program generation and simulation is the most widely used approach to functional verification of microprocessors. High complexity of modern hardware designs creates a demand for automated tools that are able to generate test programs covering non-trivial situations in microprocessor functioning. The majority of such tools use test program templates that describe scenarios to be covered in an abstract way. This provides verification engineers with a flexible way to describe a wide range of test generation tasks with minimum effort. Test program templates are developed in special domain-specific languages. These languages must fulfill the following requirements: (1) be simple enough to be used by verification engineers with no sufficient programming skills; (2) be applicable to various microprocessor architectures and (3) be easy to extend with facilities for describing new types of test generation tasks. The present work discusses the test program template description language used in the reconfigurable and extensible test program generation framework MicroTESK being developed at ISP RAS. It is a flexible Ruby-based domain-specific language that allows describing a wide range of test generation tasks in terms of hardware abstractions. The tool and the language have been applied in industrial projects dedicated to verification of MIPS and ARM microprocessors.

Added: Nov 26, 2017