Search

The research relevance is determined by the need to improve the processes of measurement of objects size in hard-to-reach conditions. In the modern industrial environment, where high measurement accuracy is critical for ensuring safety and maximizing the efficiency of production processes, the study of this topic is relevant in the context of rapid technological development and increased requirements for production quality. The study aims to evaluate the possibilities of using modern computer vision methods for measuring and reconstructing objects in difficult technical conditions, such as the enclosure of a water-water power reactor. The study employed 3D photogrammetry methods, including Depth from Stereo and Multi-View Stereo, as well as Structure from Motion methods. The study determined that modern computer vision methods, in particular machine learning methods, can be successfully used for measuring and reconstructing objects in hard-to-reach conditions. The study showed that the measurement accuracy can reach values close to 1 mm under ideal conditions and at a distance of 1.5 from the measuring device to the object. At the same time, the Multi-View Stereo method revealed greater uniformity of the spatial distribution of errors compared to the Depth from the Stereo method. In practice, in the conditions of real photos, the Multi-View Stereo method turned out to be more demanding to accurately determine the position of the camera. Due to its low demand for the exact coordinates of the cameras, the Depth from the Stereo method showed better results, showing less error in the measurements. The study highlighted the possibility of using the proposed method to distinguish fluctuations in the height of the surface of the object, which is important for further applications in the field of reactor maintenance and other areas of industry. The practical value of this research lies in the development and validation of methods for measuring and reconstructing objects in conditions where traditional methods become limited or impractical

Renewable energy and other methods of minimizing emissions into the atmosphere should be a priority for each country. This approach should be extended to Antarctica scientific stations. The study main objective was to obtain the necessary estimates of the wind energy potential of the Galindez Island territory to estimate the feasibility of installing wind turbines on the territory of the Akademik Vernadsky station. The study of the wind properties over the territory was based on the British Antarctic Survey archive of meteorological parameter average annual values (1950–2020), 3-h wind speed and direction data, registered by the Akademik Vernadsky station (2011–2020), and average daily data from meteorological observations (2014–2018). The Hellman parameter was calculated from satellite data. A number of statistical methods were used to analyze the vertical wind profile, particularly the method of minimizing the arithmetic mean relative modeling error. To assess the amount of generation, the wind speed data at the height of the anemometer sensor were recalculated to the height of the wind turbine axis. Using the wind power characteristics provided by the developers, average annual wind power generation was avaluated. For calculations of wind energy potential, we chose the technique developed by the Department of Wind Power of the Institute of Renewable Energy of the National Academy of Sciences of Ukraine. The analysis of the wind conditions showed a high average daily wind speed (3.9 m/s) and the prevailing wind direction (NNE 24%). The results support the hypothesis about the expediency of installing wind turbines on the territory of the Akademik Vernadsky station. The wind turbine was selected for further wind power calculations based on the other countries experience of using wind turbines in Antarctica and considering the specifics of installation and operation in conditions of high wind speeds, low temperatures and high relative humidity. Based on information on fuel consumption at the Akademik Vernadsky station, it was estimated that the installation of 10 wind turbines SD6 would meet 28.4% of the station's yearly electricity needs.

Abstract. Current trends in the globalization economy, especially in the context of economic crises caused by hybrid war, COVID-19, lead to a constant search for new methods of enterprise management that could ensure its effective functioning. The purpose of the study is to substantiate the theoretical and methodological aspect of determining the level of instability of the external environment of the enterprise. When forming an enterprise development strategy, it is necessary to take into account all components and criteria, including factors of variability and complexity of assessing the external impact on the level of enterprise instability, and their differentiation for enterprises in different sectors of the economy. Identification of the level of instability of the external environment is the analytical basis for the predictability of its changes, which affects the choice of management methods and directions (strategies) of its development. The article proposes a methodological approach to comprehensive assessment of the level of instability of environmental factors of enterprises, which, unlike others, involves the detection of instability in terms of seven components (socio-demographic, economic, technological, environmental, political, legal, ethical) on four criteria: complexity, interdependence, variability and uncertainty of factors, which makes it possible to determine their sources and nature, and thus form an effective response of the enterprise to change. The offered methodical approach concerning activity of the gas transport enterprises of Ukraine which are the most unstable in the conditions of the crisis phenomena is tested. The obtained results are the basis for the development of scientifically sound management decisions, forecasting the behavior of the enterprise in close connection with its external environment, which will avoid crises and ensure the sustainability of their operation and development. The current challenges of enterprises in connection with the emergence of various manifestations of hybrid warfare in the country are prompting business units to create and implement new methods of managing such structures. Keywords: environmental factors, level of instability, methodological approach, management, economy, hybrid war. JEL Classification M12, M14, I10 Formulas: 7; fig.: 3; tabl.: 4; bibl.: 18.

The paper presents recent results on the way towards accurate and complete verification of industrial operating systems (OS). We consider here OSes, either of general purpose or actively used in some industrial domain, elaborated and maintained for a significant time, and not touching research-related OSes usually developed as a proof-of-concept. In spite of the fact that the stated goal of accurate and complete verification of industrial OS is still unreachable, we consider its decomposition into tasks of verification of various functional OS components and various their properties. The paper shows that many of these tasks can be solved with the help of various modern verification techniques and their combinations. Proposed methods can be lately integrated into an approach to the final goal. The paper summarizes the experience of various OS component and features verification from the projects conducted in ISP RAS in the last years.

Functional programming plays the big role in the modern computer science and its importance is growing. This is not accidential: this approach helps to create better and more reliable software that is easy to reason about (both manually and automatically). However, these techniques are hardly used in the field of tools helping designing and modeling mission-critical systems. In this paper, we are trying to apply some nice techniques of functional programming to create a modeling system, in particular a simulation system for analysis of temporal behavioural properties of mission-critical systems. As a first step, we designed a representation of simulation time in terms of abstractions used in functional programming and tried to study its compositionability properties.

Formation of Informatics and aspects of computer software development, in particular, operating systems and information systems since the period of appearance of the first computers of 1948-1990 is considered. The program of informatization of Russia in 1992 and the development of the fundamentals of modern computer science or informatics and the intellectualization of the development of various types of software systems.

An operating system (OS) kernel is a critical software regarding to reliability and efficiency. Quality of a modern OSs kernel is high enough. Another situation is with kernel modules, e.g. device drivers, which due to various reasons have a significantly lower level of quality. One of the most critical and widespread bugs in kernel modules are violations of rules of correct usage of a kernel API. One can identify all such the violations in modules or prove their correctness with help of static verification tools which needs contract specifications describing formally obligations of a kernel and modules with respect to each other. The paper considers existing methods and toolsets for static verification of kernel modules of different OSs. It suggests a new method for static verification of Linux kernel modules that allows to configure checking at each of its stages. The paper shows how this method can be adapted for checking kernel components of other OSs. It describes an architecture of a configurable toolset for static verification of Linux kernel modules, which implements the proposed method, and demonstrates results of its practical application. Directions of further development are considered in conclusion

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.

Complex software systems always exist for a long time, sometimes changing, and this leads to a variety of versions of such a system. In additional complex software systems usually have different (sometimes a lot) configurations due to different hardware and software environments, where they are intended to operate, or due to different user types with specific requirements. So, a complex software system can be regarded more correctly as a software system family or a software product line. Taking software families in consideration helps to increase reuse of their components and other software development artifacts. In difference with earlier works on software reuse, mostly focused on code or design reuse, software system family development tries to expand reuse on all kinds of development artifacts and activities, including documentation, verification, operation support, deployment, etc. One of the software system family development activities is modeling of family variability. This paper considers modern methods and approaches to such modeling, especially focusing on modeling of operating systems families variability. The research, which results are presented in this paper, is supported by RFBR.

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 paper regards problems of analysis and verification of complex modern operating systems, which should take into account variability and configurability of those systems. The main problems of current interest are related with conditional compilation as variability mechanism widely used in system software domain. It makes impossible fruitful analysis of separate pieces of code combined into system variants, because most of these pieces of code has no interface and behavior. From the other side, analysis of all separate variants is also impossible due to their enormous number. The paper provides an overview of analysis methods that are able to cope with the stated problems, distinguishing two classes of such approaches: analysis of variants sampling based on some variants coverage criteria and variation-aware analysis processing many variants simultaneously and using similarities between them to minimize resources required. For future development we choose the most scalable technics, sampling analysis based on code coverage and on coverage of feature combinations and variation-aware analysis using counterexample guided abstraction refinement approach.

In this work the problem of high quality verification techniques applicable for operating systems is formulated. A perspective approach to solve this problem is integration of various verification methods. The solution technique can be considered successful if it allows to check the whole operating system and to verify in more accurate way the most important functions and components of the system, using more strict and formal methods for it. Based on the ISP RAS experience in operating system verification projects conducted using various verification techniques we determine development artefacts, that can be suitable integration point candidates for integration of formal specification based static and dynamic verification techniques for operating systems.

UniTESK (UNIfied TEsting and Specification toolKit) is a testing technology based on formal models (or specifications) of requirements to behavior of software or hardware components. It was created with experience gained during development of the framework for automated testing of a real-time operating system kernel during 1994-2000. Software contracts were the main kind of models in the first version of the technology. Automata models were also implemented to support generation of complicated test sequences. UniTESK was first used in 2000 in the development of the test suite for IPv6 implementation. It was the first experience of using contract specifications in testing of implementations of telecommunication protocols. This project demonstrated that contract specifications in combination with the technique of testing software systems with asynchronous interface developed within UniTESK are very effective. Applications of UniTESK to testing software components in Java include the project on testing of implementation of standard library for Java runtime support and the project on testing of infrastructure of information system for one of large mobile operators in Russia. The most significant application of UniTESK happened in 2005-2007 in the Open Linux Verification project. Formal specifications and tests for interfaces of the Linux Standard Base were created during the project. These results then were used in development of the test suite for Russian avionics real-time operating system. Positive lessons learned during development and using UniTESK include effective application of model based testing methods in large industrial projects, high level of test coverage achieved by the generated tests, applicability of model based testing to critical systems and applications. Negative lessons include the lack of well-defined and detailed models and specifications, extra development expenses caused by creation of test specific models, problems with introduction of model based testing technologies using bilingual test generation systems and specific notations.

Linux driver verification is a large application area for software verification methods, in particular, for functional, safety, and security verification. Linux driver software is industrial production code — IT infrastructures rely on its stability, and thus, there are strong requirements for correctness and reliability. Linux driver software is complex, low-level systems code, and its characteristics make it necessary to bring to bear techniques from program analysis, SMT solvers, model checking, and other areas of software verification. These areas have recently made a significant progress in terms of precision and performance, and the complex task of verifying Linux driver software can be successful if the conceptual state-of-the-art becomes available in tool implementations.The paper is based on experience of the research groups led by authors in verification of industrial software. It is important to develop verification tools that are efficient and effective enough to successfully check software components that are as complex as device drivers. In this area verifiers/researchers and Linux society find mutual benefits in cooperation because: for the society it is important to get such crucial software verified; for the verification community it is important to get realistic verification tasks in order to tune and further develop the technology. The paper provides an overview of the state-of-the-art and pointed out research directions in which further progress is essential. In particularly the paper considers most promising verification techniques and tools, including predicate abstraction, counter example generation, explicit-state verification, termination and concurrency analysis. One of main topic of Linux driver verification research is combination of verification techniques.

The last decade has seen the rapid development of digital information technology, the intellectualization of control systems, the increase in the number and capacity of mobile and computer devices, and the accumulation of large amounts of data and its processing through machine learning algorithms, which inevitably leads to new opportunities for economic development. Rapid digitalization and its penetration into various spheres of public life contributed to increasing the level of transparency of public administration, strengthening public control, and reducing the bureaucratization of society. Hence, digital technologies can serve as tools to fight corruption and create conditions for intensive economic growth. Therefore, the topic based on the study of transmission effects in the chain "corruption-digitization-economic growth" is relevant. The work aims to develop methodological tools for assessing the transmission effects between digitalization, corruption level decrease, and economic growth. The following methods were used for the study: Levin-Lin-Chu, Hadri, Pesaran, and Chin tests, Dickey-Fuller tests - to check stationary variables; statistical criterion Kao - to check the existence of cointegration relationship between variables; modified least-squares method - to estimate regression coefficients based on panel data; coefficient of determination and Jarque-Bera test – to verify the adequacy of the econometric model. An empirical study confirmed the hypothesis of the presence of transmission effects between indicators that characterize the level of corruption in the economy, digitalization, and economic growth. It has been proven that the reduction of corruption and the growth of digitalization in studied countries contributes to economic growth. [ABSTRACT FROM AUTHOR]