A critical factor in ensuring the quality of software written in current and next-generation programming languages is the ability to rely on a formal operational semantics of the language. This gives developers a systematic, well-founded way to address reliability, performance, and security in the target software. We introduce a new formal framework where operational semantics can be developed and used not as a traditional non-executable abstract system, but as runnable code. That brings several advantages: easier modification, the ability to run across different execution environments, testing and debugging, version control, and more. We illustrate our approach using a practically relevant subset of the widely used C programming language. The strengths of our semantics framework are demonstrated by comparing it against the most popular current approaches across a set of practically relevant criteria. The paper presents the Attribute-Based Modeling Language (ABML) — a new domain-specific language designed for ontological modeling of programs and for defining their operational semantics in executable form. We describe the proposed method for building executable operational semantics with ABML. A worked example shows how our approach applies to a practically relevant subset of C. We then build an enriched ontology of C by adding semantic attributes, define algorithms for computing those attributes in ABML, and discuss how the enriched ontology influences the development of operational semantics. A detailed review of related work lets us compare our approach to state-of-the-art frameworks in terms of meeting current requirements for operational semantics development.

Process-oriented programming is an approach to developing control software where a program is structured as a set of processes. PoST is a process-oriented extension of ST language from the IEC 61131-3 standard. Since control systems often have high reliability requirements, formal verification of their software plays an important role. One formal verification method is deductive verification, which involves building a formal specification, generating verification conditions, and proving them. We use the Isabelle/HOL theorem prover for the proof step. Only the generation of verification conditions is fully automated. Deductive verification itself is labor-intensive, so automating it as much as possible is desirable. Control software involves temporal requirements, which in deductive verification of process-oriented programs are expressed as control loop invariants. However, these requirements are insufficient invariants, making it necessary to introduce extra invariants that carry auxiliary information about the program. An earlier approach to proving verification conditions used patterns for both the requirements and the extra invariants, with pattern-specific lemmas satisfying predefined schemas used in the proofs. This paper looks at automating the proof of both the verification conditions and the lemmas used in those proofs. We describe the previously proposed approach to automating deductive verification and give an introduction to Isabelle/HOL. Revised schemas for patterns and lemmas are presented, along with an algorithm for generating lemma proofs. We discuss the implementation of this algorithm and of the previously developed algorithm for generating verification condition proofs. The proposed approach is demonstrated with an example. A review of related work is provided.

Declarative process models are widely used in process mining to describe flexible process behavior through sets of constraints. However, models discovered automatically from event logs may contain inconsistent constraints, which can make them difficult to interpret and unusable for execution, conformance checking, or further analysis. Existing methods for consistency analysis either rely on automata-based constructions with high worst-case time complexity or use heuristics based on MIS (minimal inconsistent subsets) that do not provide a full formal characterization of the inconsistency patterns they detect. In this paper, we propose a graph-based approach to the inconsistency analysis for a restricted fragment of Declare process modeling language. We represent dependencies between constraints through the task entailment graph and characterize inconsistency by means of three structural witness types. Based on this characterization, we first detect candidate inconsistent subsets and then verify whether a candidate is a minimal inconsistent subset by dedicated verification procedures. In contrast to automata-based approaches, the proposed method avoids explicit automata products and relies instead on graph-based analysis and constructive trace arguments. We implement the proposed approach and evaluate it on real-life event logs, showing that it is practically feasible and achieves competitive runtime.

This article addresses the problem of mathematical modeling of square wave noise in electromagnetic signals, particularly in eddy current defectograms, to generate high-quality synthetic samples for training machine learning algorithms to detect and suppress square wave noise in data. A comprehensive study of naive models is conducted: a deterministic square wave signal, a square wave signal with white noise, and a telegraph process with white noise. The telegraph process with white noise serves as the central object of the study. For this model, stationary characteristics are analytically derived: the limiting probability density function and the autocorrelation function. To estimate the model parameters, a fully Bayesian approach is proposed and implemented for the first time, utilizing Gibbs sampling and the Forward Filtering Backward Sampling (FFBS) algorithm to efficiently marginalize the hidden Markov states. The parameter estimation algorithm converges rapidly, reaching an overall variance of $1e{-}6$ value by the 1500th iteration. It is established that classical models possess fundamental limitations due to the unrealistic assumption of a strictly constant period and duty cycle. It is shown that while the telegraph process resolves the issue of stochastic pulse durations, ignoring the continuity of transition fronts leads to a mathematical artifact — a shift in the modes of the theoretical limiting distribution compared to the empirical one. Furthermore, it is demonstrated that the absence of a low-pass filtering mechanism deprives the model's autocorrelation function of its characteristic oscillating component. The experimental confirmation of the significance of these factors justifies the direction for further research: the development of modified stochastic models integrating smooth state-switching mechanisms for the adequate simulation of square wave noise. Eddy current rail defectograms served as the empirical base for testing the models. Nevertheless, the developed mathematical framework can be successfully applied to model square wave noise in other types of electromagnetic signals, such as in ECG and magnetotelluric sounding.

This paper addresses the problem of reliability assessment for a tethered high-altitude unmanned telecommunication platform using the risk tree analysis method. The aim of the study is to develop and test a methodology for the quantitative estimation of the probability of risk events and the associated material damage during long-term platform operation. A disruption in the provision of broadband wireless communication services by the platform is considered as the resulting risk event. A detailed technical description of the tethered platform “Albatros" is provided, which serves as the basis for identifying risk events. The general theory and methodology for constructing and analyzing a risk tree are presented, including the parameterization of the model with probabilistic and cost characteristics. Using the tethered high-altitude unmanned telecommunication platform as a case study, a comprehensive numerical investigation is carried out. Within this investigation, a sensitivity analysis of key output indicators — namely, the reliability function, quantiles, mean time to failure, and expected damage — is conducted with respect to the statistical properties of failure times, specifically the coefficient of variation and the distribution shape.The practical conclusions derived from the study demonstrate that the use of adequate probabilistic models (as opposed to simplified exponential ones) is critical for obtaining realistic forecasts. The most dangerous risk evolution scenarios are identified, and the contribution of factors influencing the occurrence of these events is quantitatively assessed. The proposed methodology is universal and can be applied to a wide range of complex technical systems, including other tethered platforms whose architectures allow decomposition into key components with established logical relationships between their failures. The obtained results can be used for the evidence-based design of such systems, the planning of scheduled maintenance, and the optimization of technical support strategies.

The dynamics of large non-periodic chains with advective connections between elements is considered. The main assumption is that the number $N$ of chain elements is sufficiently large, so a small parameter $\varepsilon=N^{-1}$ naturally arises. This assumption allows us to move from a system of $N$ delayed equations to the study of a spatially distributed integro-differential equation containing a small parameter and use asymptotic methods to investigate the dynamic properties of this equation. The connections between the chain elements are a difference approximation of the advection operator, which is why they are called advective. Another assumption is that the chains are not circular, i.e., the boundary conditions for the systems under consideration do not have periodic properties. Non-classical boundary conditions are considered, which lead to the emergence of new dynamic effects. Critical cases in the problem of equilibrium stability are identified, and it is shown that they have infinite dimension in the sense that an infinite number of roots of the characteristic equation approach the imaginary axis as a small parameter approaches zero. In this situation, the known research methods based on the use of invariant integral manifolds and normal forms are not directly applicable. We use methods of quasi-normal forms, whose non-local dynamics determine the local behavior of the solutions of the considered chains. The main results consist in constructing quasi-normal forms using special asymptotic methods. This allows us to obtain the main approximations of the solutions of the original chain with respect to the parameter $\varepsilon$.

This paper studies the problem of ranking SQL query execution plans by execution time. We propose a method in which structural encoding of the plan tree is replaced with a textual description of the plan, which is then converted into a vector representation using a vector representation model. A compact prediction model is trained on top of this representation and used to rank plans. Three approaches are compared: the prediction model from Bao, which relies on structural encoding of the plan tree, the cost estimate produced by the PostgreSQL optimizer, and the proposed method based on textual plan descriptions and vector representation models. In addition, several vector representation models and two variants of textual plan description are investigated: the raw plan text and a normalized description. Experiments are conducted on the CEB benchmark built on IMDb data under two evaluation settings: random splits and query-template splits. Quality is evaluated using pairwise accuracy and Spearman correlation. The results show that under random splits, the best configuration based on jina-code-embeddings-0.5b outperforms both the Bao model and the optimizer cost estimate on both ranking metrics. For all considered models, the raw textual plan description is more informative than the normalization scheme used in this work. Under query-template splits, the quality of all learned approaches decreases; in this setting, the best model based on vector representations and the Bao model remain comparable to each other, but both are outperformed by the optimizer cost estimate. These results indicate that textual plan descriptions and vector representation models can serve as a basis for predictive plan-ranking methods, although robust generalization to previously unseen query templates remains an open problem.