The paper presents the basic principles of UniTESK technology intended for test construction based on formal models. It also summarizes experience of using UniTESK in large test development projects for software and hardware systems, including telecommunication protocols, basic and standard interfaces of operating systems, microprocessor units. The paper provides a vision of the future technology development for higher scalability of test suites constructed

The paper covers theoretical and practical works on conformance testing performed in ISP RAS since 1994 till now. The conformance theory development was done in various directions and, in the whole, was characterized by generalization of the interaction semantics, models and conformances in use. The necessity of such generalization was imposed, first of all, by requirements of testing practice. It is true for such system properties as nondeterminism, partial specified, asynchronous behavior, diversity of test stimuli and observations of the implementation behavior etc. It was always focused on testing effectiveness defined both by optimization of tests suites and by test generation algorithms including on-the-fly. We consider the main milestones on this way in a brief and informal discussion, paying attention not to details, but to the main problems and their solutions trying to reveal the common tendency of the development

An operating system is a base stone of any computer system. Failures and bugs in operating system impact the functionality of the system as a whole, that is why correctness and reliability of operating systems are so important. A variety of circumstances make verification and testing of operating systems a complicated issue. The list includes high dependence of operating systems on hardware, their massive internal concurrency, huge number of configuration options, required tolerance to aggressive actions of counteragents and hardware faults, a need for long continuous work without reboot, etc. The paper discusses influence of all the circumstances on testing, describes testing tools and techniques developed in ISPRAS and presents our experience of testing of various components of Linux as well as a few other real-time operating systems.

This article summarizes the experience gained while developing test suites for conformance testing of implementations of Internet protocols. The projects described in this article used the UniTESK technology as a base for constructing tests. During the development of test suites we identified certain features of the protocols that make it difficult to apply UniTESK unmodified to protocol conformance testing, as well as some limitations of UniTESK toolkits. Nevertheless all these obstacles were successfully overcome without going beyond UniTESK concepts.

Ensuring the correctness of microprocessors and other microelectronic equipment is a fundamental problem. To deal with it, various tools for functional verification are used. Unlike bugs in software programs which are relatively easy to fix (it does not apply to their consequences), defects in integrated circuits (both design and manufacturing ones) cannot be removed. In spite of continuous development of computer-aided design (CAD) systems, test generation tools and approaches to analysis of circuits, verification remains the bottleneck of the microprocessor design cycle (it accounts for approximately 70 percent of total design resources). The article gives a brief overview of microprocessor verification tools, describes issues that commonly occur in industrial practice and analyzes possible ways to solve them. The main part of the article is dedicated to research in the field of hardware verification conducted at ISPRAS. It summarizes the outcomes of accomplished projects, describes the present works and formulates the directions of further research.

Growth of modern avionics systems makes design of such systems impossible without involvement of automation. Nowadays an area of such tools is represented by both the proprietary tools developed by the major aircraft manufacturers like Boeing and Airbus, and a number of open or partially open international projects varying in maturity, availability of source code and documentation. The paper presents a toolset for design of modern avionics systems developed by ISPRAS in collaboration with GosNIIAS. The toolset provides both a generic platform for design and analysis of architecture models and a specialized solution for the particular domain of avionics systems.

This paper describes Svace, a tool for static program analysis developed in ISP RAS. This tool allows to find defects and potential vulnerabilities in source code of programs written in C/C++ languages. Main features of the tool are simplicity of usage, wide variety of supported warning types, scalability up to programs of millions lines of code and acceptable quality of analysis (30-80% of true positive warnings).

This paper presents methods and tools for binary code analysis that have been developed in ISP RAS and their applications in fields of algorithm and data format recovery. The analysis subject is executable code of various general purpose CPU architectures. The analysis is carried out in lack of source code, debug records, and without specific OS version requirements. The approach consists of collecting a detailed machine instruction level execution trace; method for successive presentation level increase; extraction of code belonging to the algorithm followed by structuring of both code and data formats it processes. Important results have been achieved: an intermediate representation has been developed, that allows for carrying out most of the preliminary processing tasks and algorithm code extraction without having to focus on specifics of a given machine; and a method and software tool have been developed for automated recovery of network message and file formats. The tools have been incorporated into a unified analysis platform that supports their combined use. The architecture behind the platform is also described in the paper. Examples of its application to real programs are given.

The article presents the experience of using software emulators as a tool for dynamic analysis of binary code: as a machine instruction tracer, and as a smart interactive debugger. We provide a description of deterministic replay implemented in the QEMU emulator to supply the stated functionalities.

The paper is dedicated to performance improvement of JavaScript programs. In this work we examine the specifics of dynamic optimizations in JIT-compiler for JavaScript, and how the performance of such optimizations can be improved. Also we propose a method for ahead-of-time (AOT) compilation of JavaScript programs, and for saving them as a bytecode. This method allows reducing startup time of applications by moving the optimizations to AOT phase. The proposed methods were implemented in open-source WebKit library, and resulted in significant performance gain for popular JavaScript benchmarks on ARM platform.

The paper describes two-stage compilation approach for C/C++ languages that allows deploying application in the LLVM intermediate representation. The LLVM modifications for optimizing code generation time are presented as well as the developed profile-based optimizations. The specialized application cloud storage architecture is also suggested.

The paper describes the methods for obfuscating C/C++ programs to prevent applying static analyzers to them. The methods are implemented within the well-known LLVM compiler infrastructure. Experimental results presenting resulting program slowdown and used memory growth are given.

The paper describes the workflow for optimizing programs for performance targeting the fixed hardware architecture with static compilation using GCC and LLVM compilers as examples. We present some of the optimizations performed and the corresponding evaluation results. We also describe TACT, a tool for automatic compiler tuning for the given application, and its example use cases both for an application developer and a compiler engineer. We give the sample of TACT optimization results.

The article proposes methods for supporting development of efficient programs for modern parallel architectures, including hybrid systems. Specialized profiling methods designed for programmers tasked with parallelizing existing code are proposed. The problem of automatic parallel code generation for hybrid architectures is discussed. In cases where achieving high efficiency on hybrid systems requires significant rework of data structures or algorithms, one can employ auto-tuning to specialize for specific input data and hardware at run time. This is demonstrated on the problem of optimizing sparse matrix-vector multiplication for GPUs and its use for accelerating linear system solving in OpenFOAM CFD package.

This paper describes the principles of program dynamic analysis for defect detection using input data generation. Techniques of program transformation allowing execution trace extraction, data flow tracing and input data generation for execution path coverage approaches are considered. We clarify in what way such an approach allows us to perform fully automatic analysis using executable or interpretable code. This paper also presents dynamic analysis tools developed at Institute for System Programming RAS---Avalanche (Valgrind-based tool) and a prototype tool for Java applications. The paper concludes with an evaluation of practical results of applying Avalanche tool to a set of open source projects as well as results of applying Java analysis tool to detect concurrency defects.

Refactoring is one of the most popular and successful techniques in improving source code. It is an integral part of agile development methods. However, we still lack effective tools for source code automatic refactoring for C/C++. This article focuses on one of approaches to developing a tool for such refactoring. It is worth mentioning that possibility of applying refactoring only on one translation unit is significant a limitation for any refactoring tool. Hence, an important aspect of this article is a detailed description of transition from refactoring on one translation unit scheme to refactoring on the whole project. Besides, special attention is paid here to refactoring «Rename» as it is one of the most widely used refactorings on the whole project.

A web-laboratory is a web based software platform to support scientific collaboration, research, and education. It has unique combination of capabilities that allows to conduct numerical experiments, discussion of results in workshops and meetings, planning activities, to prepare reports and articles, to support the educational processes (training courses, workshops, labs, etc.). It lets researchers and engineers: run simulation tools; upload and share datasets, documents and other materials; work together in a private space, send messages to one another; ask questions and post responses; work collaboratively on the source code of their simulation programs and share those programs with the community. Web laboratory implementation is related with need to enable dispatching of different remote computational resources (supercomputers , high performance clusters , including accelerators computing, development of 2D and 3D visualization , servers, storage and processing of large data sets , etc.) and software in a way that is completely transparent to users. It is also necessary to provide scalability, reliability and security. Modern method to solve this problem is to use a cloud computing model. In this model computational resources are provided to user as remotely set of elastic services with on demand access. The paper describes an architecture of web laboratory developed in scope of the cloud model. The UniHUB platform implementation based on this architecture is represented. The UniHUB is as an extension of the OpenStack platform.

The paper presents a framework for fast text analytics developed during the Texterra project. Texterra delivers a scalable solution for text processing based on novel methods that exploit knowledge extracted from the Web and text documents. This paper describes details of the project, use-cases and results of evaluation for all developed tools.

The paper describes the basic components of ISPRAS technology stack for social network data analysis. Particular attention is given to tasks, methods, and applications of network (social connections between users) and textual (user messages and profiles) data analysis: demographic attribute detection, event detection in messages corpora, user identity resolution, community detection, and influence measurement. Means for input data acquisition are also considered: collecting real data through web-interfaces of social services and generating random social graphs. For each of the developed tools we describe its functionality, use cases, basic steps of the underlying algorithms, and experimental results.

Effective project management implies the use of advanced planning and scheduling methods that allow to determine the feasible sequences of activities and to complete a project on time and on budget. Traditional scheduling tools like fundamental Critical Path Method (CPM) and various methods for Resource Constrained Project Scheduling Problem (RCPSP) and Time Constrained Project Scheduling Problem (TCPSP) have many shortcomings for the construction projects where spatial factor plays critically important role. Previously taken attempts to interpret space as a specific resource were successful for particular problems of line-of-balance scheduling, space scheduling, dynamic layout planning, horizontal and vertical logic scheduling, workspace congestion mitigating, scheduling multiple projects with movable resources, spatial scheduling of repeated and grouped activities, motion planning. However, none of these methods considers the spatio-temporal requirements in a holistic framework of generic RCPSP problem and provides feasible results accounting for workspace and workflow factors. In the paper we start with the classical RCPSP statement and then present mathematically strong formalization of the extended generalized problem taking into account workspace congestion and workflow disturbance constraints specified in practically meaningful and computationally constructive ways. For the generalized RCPSP problem an effective scheduling method is proposed. The method tends to minimize the project makespan while satisfying timing constraints and precedence relations, not exceeding resource utilization limits, avoiding workspace congestion and keeping workflows continuous. The method reuses so-called serial scheduling scheme and provides for additional computational routines and heuristic priority rules to generate feasible schedules satisfying all the imposed requirements. In order to evaluate the method, benchmark sets are proposed and investigated. Advantages of the method and prospects for its application to industrial needs are outlined in the paper too.

In this paper the problem of scheduling parallel tasks on a group of clusters and formalization of this process as an optimization of packing rectangles in a set of strips of different widths is considered (Multiple Strip Packing). Some modern results concerning this problem and some open problems are presented. Practical aspects of optimization of scheduling parallel tasks process with different criteria of its quality are considered. The description of modeling system developed in the ISP RAS for experimental investigation of scheduling algorithms is presented and its properties are described.