The article is devoted to the task of the sentiment detection towards an aspect of economic and social development in Russian sentences. The aspect, the attitude to which is determined, can be either explicitly mentioned or implied. The authors investigated possibilities of using neural network classifiers and proposed an algorithm for determining the sentiment towards an aspect based on semantic rules implemented with the use of constituency trees. The sentiment towards an aspect is determined in two stages. At the first stage, aspect terms (explicitly mentioned events or phenomena associated with the aspect) are found in the sentence. At the second stage, the sentiment towards an aspect is calculated as the sentiment towards the aspect term that is most closely associated with the aspect. The paper proposes several methods for searching the aspect terms. The performance was assessed on a corpus of 468 sentences extracted from election campaign materials. The best result for neural network classifiers was obtained using the BERT-SPC neural network pretrained on the task of identifying the sentiment towards an explicitly mentioned aspect, the macro F-score was 0.74. The best result for the semantic rule-based algorithm was obtained using the method of aspect term searching based on semantic similarity, the macro-F-score was 0.63. When combining BERT-SPC and the rule-based algorithm into an ensemble, the macro-F-score was 0.79, which is the best result obtained in this work.

Process-oriented programming is an approach to developing control software in which a program is defined as a set of interacting processes. PoST is a process-oriented language, which is an extension of the ST language from the IEC 61131-3 standard. In the field of control software development, formal verification plays an important role due to the need to ensure high reliability of such software. Deductive verification is a formal verification method in which a program and its requirements are represented as logical formulas, and logical inference is used to prove that the program satisfies the requirements. Control software often has temporal requirements. We formalize such requirements for process-oriented programs as control loop invariants. However, control loop invariants that represent requirements are not sufficient to prove the correctness of the program. Therefore, we add extra invariants containing auxiliary information. This paper considers the problem of automating deductive verification of process-oriented programs. An approach is proposed in which temporal requirements are specified using requirement patterns which are constructed from basic patterns. For each requirement pattern, a corresponding extra invariant pattern and lemmas are defined. In this paper, the proposed approach and schemes of basic and derived requirement patterns are described. The schemes of basic extra invariant patterns, schemes of lemmas defined for basic patterns, and a set of basic patterns and lemmas for them are considered. The scheme of derived extra invariant patterns and schemes of lemmas defined for derived patterns are defined. The algorithms for constructing derived extra invariant patterns and lemmas for them, as well as methods for proving these lemmas are presented. The schemes of proving verification conditions are considered. The proposed approach is demonstrated with an example. The analysis of related works has also been carried out.

In this paper we focus on regular expressions with acyclic backreferences and treat them as a semiring satisfying certain theorems of Kleene algebra. Using these theorems as term rewriting rules, we introduce an algorithm for memory disambiguation of regular expressions. Furthermore, we demonstrate that the class of regexes with acyclic backreferences is closed under language reversal, in contrast to the generic backref-regexes, and provide the reversal algorithm, based on the disambiguation procedure. The results of our experiments revealed that, in certain cases, the matching time was significantly reduced when using the reversed expressions compared to the initial ones.

Interacting in open networks carries certain risks. To ensure the information security of network interaction participants, cryptographic protocols (CrP) are used. High levels of security can be achieved through their formal verification. A common formal method for verifying CrP is model checking.

In this work, we propose using the TLA+/TLC toolset to check models of CrP. This toolset is widely applied in various practical fields. The protocol model is defined in the TLA+ specification language, as well as the required security properties in the form of invariants. The model of a protocol describes its behavior as a transition system containing all possible states of the protocol model and transitions between them. The TLC model checker is employed to automatically verify that the model meets the required properties.
The task of verifying CrP has its specifics. This study proposes three modeling techniques that take into account the specifics of both the task and the TLA+/TLC toolset being used. The first technique involves replacing a system consisting of an arbitrary number of agents with a three-agent system. This simplifies the model and reduces its state space. The second technique is related to representing transmitted messages as a hierarchical structure, allowing encrypted messages to be nested within others. The third technique consists of optimizing the model to improve the performance of the TLC model checker by defining a function that generates only those elements leading to transitions between states in the model. These techniques simplify the model and reduce verification time.
We demonstrate the application of these results on a simple protocol example — the Needham-Schroeder public key authentication protocol. After detecting a known vulnerability in the original protocol by using TLC, we model and verify an improved version. Verification results show that the new version of the protocol does not have this vulnerability.

This paper uses the model checking method for an exact schedulability test of real-time systems running on multiprocessor platforms. To use this method, we formally describe real-time systems with an abstract scheduler as Kripke models. This formalization provides terms sufficient to specialize the abstract scheduler. We illustrate our approach by explicitly defining schedulers that take into account preemption/non-preemption of tasks and global fixed or earliest-deadline-first priority in various combinations. The safety (schedulability) property of real-time systems is formulated using linear temporal logic LTL. Formalizing real-time systems as Kripke models and specifying the safety (schedulability) property as an LTL formula allows us to reduce the exact schedulability test of such systems to a model checking problem. We validate this approach to an exact schedulability test by implementing our formalization of real-time systems with non-preemptive global fixed-priority (NP-GFP), preemptive global fixed-priority (P-GFP), non-preemptive earliest-deadline-first priority (NP-EDF), and preemptive earliest-deadline-first priority (P-EDF) schedulers in Promela, the input language of the model checking tool SPIN. We conduct experiments in SPIN to prove/disprove the safety (schedulability) property to evaluate the effectiveness of our approach. We propose a heuristic assessment of the schedulability of a real-time system based on the provability of unsafety and unprovability of safety of a real-time system executed on multiprocessor platforms with the number of processors differing by one.