№ 4 (2025)

This paper formulates an asymptotic method for investigating vector electromagnetic fields of waveguide modes in the adiabatic approximation. The asymptotic method in the zero approximation is reduced to the symbolic investigation of a homogeneous system of ordinary differential equations; higher approximations correspond to inhomogeneous systems of ordinary differential equations with a similar matrix of coefficients. Using the asymptotic method, symbolic solutions in the zero and first approximations are obtained.

In this paper, the problem of the distributed network survivability is investigated. A distributed system is modeled by a finite connected undirected graph whose nodes are divided into two types: hosts and switches. Hosts perform computational functions, while switches are utilized for providing the message delivery between hosts. The system survivability is considered as the system ability to perform the main functions of message transmission after graph edges’ failures. The solution for the system survivability is provided by duplicating the paths for message transmitting. The main condition for the correct solution is the absence of message looping in the network for any set of selected paths. The four-path theorem is proved for the case of two recipient hosts: if for each recipient host there are two paths from the sending host and the edge sets traversed by these paths are disjoint, then there is no message looping for this set of the paths.

Algebraic data types allow representing complex data structures, thus classical verification methods relying on inductive invariant inference are not applicable to programs with such types. The main problem with classical methods is the weakness of the first-order logic language used to represent inductive invariants. In this paper, synchronous automata over trees are considered as an alternative to classical representations of invariants using first-order logic. A method for automatic inductive invariant inference represented by synchronous automata over trees is proposed. The method uses finite-model finding. The implementation of the proposed method finds 65% more invariants than a first-order logic based tool, which is an annual winner of an international verifier competition, on an existing benchmark.

In the context of the development of the modern economy, the scope of application of Big Data (databases, performance computing, high-speed network channels) and automated methods of work in this area (design of data systems, management and monitoring) is rapidly expanding. Artificial Intelligence systems are becoming especially popular as methods for automating all of the above points. In our country, serious problems are being solved in these areas of computer science. Despite a number of systemic problems, in Russia a distributed network of Supercomputer Centers for Collective Use is being formed, which is designed to solve the problem of rational use of supercomputer systems. There are also advances in the work to create technologies for writing and translating parallel Software. The article provides a brief overview of the software solutions used in the Plan 9 Operating System. In particular, the 9P file system network protocol is reviewed and its brief comparison with NFS (at the moment) is given. Based on this protocol, the author proposed a software architecture for the Rapid Access for Multi Processing and Learning for intermediate calculations, which is necessary in the optimization of numerical methods and machine learning within distributed computing systems. Also, the author proposes to use the protocol’s capabilities to organize monitoring of remote hosts, as well as manage processes and devices on it. The article outlines the tasks for improving the 9P network protocol. Some comments are made about the features of using the protocol in its modern form. It is concluded that there is great potential for using technologies based on it.

The paper considers the task of automated design of graphical user interfaces (GUI). A system based on the constraint programming paradigm takes the rules for the arrangement of controls, the controls themselves, and determines some number of arrangements that satisfy the rules. The system is implemented as a web application and allows one to get responses gradually, within a reasonable time.

Fault-proneness is a measure that indicates the possibility of programming errors occurring within a software system. On the other hand, change-proneness refers to the potential for modifications to be made to the software. Both of these measures are crucial indicators of software maintainability, as they influence internal software metrics such as size, inheritance, and coupling, particularly when numerous changes are made to the system. In the literature, research has predicted change- and fault-proneness using internal software metrics. That research is almost a decade old. However, given the continuous evolution of software systems, it is essential to revisit and update our understanding of these relationships. Therefore, we have conducted an empirical investigation to revisit the relationship among various internal software metrics and change-proneness, and faultproneness, aiming to provide current and relevant insights. In our study, we identified 25 internal software metrics along with the measures of change-proneness and fault-proneness within the well-known opensource systems belonging to the Apache and Eclipse ecosystems. Next, we analyzed the relationships between these metrics using statistical correlation methods. Our results revealed that most of the metrics have little to no correlation with fault-proneness. However, metrics related to inheritance, coupling, and comments showed a moderate to high correlation with change-proneness. These findings will help developers to minimize the higher correlated software metrics to enhance maintainability in terms of change- and fault-proneness. Additionally, these insights can guide researchers in developing new approaches for predicting changes and faults by incorporating the metrics that have been shown to have stronger correlations.

The verification of software properties using formal verification tools is one of the current research directions in the field of information flow control. Security conditions of information flows in software under various information noninterferrence schemes are naturally described by so-called hyper-properties in well-known extensions of linear temporal logic and computation tree logic. In practice, verifying such properties for large projects is a non-trivial task. In this work, the authors translate the idea of dynamic type checking to detect prohibited information flows into the realm of computation verification using model-checking tools. Computations over security labels (safe types) are described by the abstract semantics of information flows. Transitioning from concrete computational semantics to abstract semantics of information flows allows formulating these security properties as state properties. In this case, proven tools in large industrial projects such as TLA+ and TLC can be used for the description and verification of real computer systems.