Tolerant parsing is a form of syntax analysis aimed at capturing the structure of certain points of interest presented in a source code. While these points should be well-described in the corresponding language grammar, other parts of the program are allowed to be not presented in the grammar or to be described coarse-grained, thereby parser remains tolerant to the possible inconsistencies in the irrelevant area. Island grammars are one of the basic tolerant parsing techniques. “Island” is used as the relevant code alias, while the irrelevant code is called “water”. In the paper, a modified LL(1) parsing algorithm with built-in “Any” symbol processing is described. The “Any” symbol matches implicitly defined token sequences. The use of the algorithm for island grammars allows one to reduce irrelevant code description as well as to simplify patterns for relevant code matching. Our “Any” implementation is more accurate and less restrictive in comparison with the closest analogues implemented in Coco/R and LightParse parser generators. It also has potentially lower overhead than the “bounded seas” concept implemented in PetitParser. As shown in the experimental section, the tolerant parser generated by the C# island grammar is proven to be applicable for large-scale software projects analysis.

Specialization is a program optimization approach that implies the use of a priori information about values of some variables. Specialization methods are being developed since 1970s (mixed computations, partial evaluation, supercompilation). However, it is surprising, that even after three decades, these promising methods have not been put into the wide programming practice. One may wonder: What is the reason? Our hypothesis is that the task of specialization requires much greater human involvement into the specialization process, the analysis of its results and conducting computer experiments than in the case of common program optimization in compilers. Hence, specializers should be embedded into integrated development environments (IDE) familiar to programmers and appropriate interactive tools should be developed. In this paper we provide a work-in-progress report on results of development of an interactive specializer based on partial evaluation for a subset of the Java programming language. The specializer has been implemented within the popular Eclipse IDE. Scenarios of the human-machine dialogue with the specializer and interactive tools to compose the specialization task and to control the process of specialization are under development. An example of application of the current version of the specializer is shown. The residual program runs several times faster than the source one.

Embedded platforms with heterogeneous architecture, considered in this paper, consist of one primary and one or more secondary processors. Development of software systems for these platforms poses substantial difficulties, requiring a distinct set of tools for each constituent of the heterogeneous system. It also makes achieving high efficiency the more difficult task. Moreover, many use cases of embedded systems require runtime configuration, that cannot be easily achieved with usual approaches. This work presents a C-like metaprogramming DSL and a library that provides a unified interface for programming secondary processors of heterogeneous systems with this DSL. Together they help to resolve aforementioned problems. The DSL is embedded in C++ and allows to freely manipulate its expressions and thus embodies the idea of generative programming, when the expressive power of high-level C++ language is used to compose pieces of low-level DSL code. Together with other features, such as generic DSL functions, it makes the DSL a flexible and powerful tool for dynamic code generation. The approach behind the library is dynamic compilation: the DSL is translated to LLVM IR and then compiled to native executable code at runtime. It opens a possibility of dynamic code optimizations, e.g. runtime function specialization for specific parameters known only at runtime. Flexible library architecture allows simple extensibility to any target platform supported by LLVM. At the end of the paper a system approbation on different platforms and a demonstration of dynamic optimizations capability are presented.

Nowadays there is an actual problem in aviation industry - how to make the development of complex safety-critical systems certifiable according to international and domestic standards and regulations like DO-178C, DO-254, ARP 4754A, ARP 4761 etc. In the article configuration management process from the development lifecycle of DO-178C is considered as the main source of criteria for the development tool selection. Selected criteria can be applied to software tool, which supports entire development lifecycle of aviation software, as well as to software tools supporting some individual lifecycle processes. The activities of configuration management process provide work with all project lifecycle data, its storage, integrity, security, manageability and information support for data exchange between the remaining lifecycle processes, maintenance of the history of changes etc. Compliance with the principles of the configuration management process allows project managers to control development, ensure the required quality and reliability of the product; also, its certifiability and the necessary level of confidence in security, reduce financial and time development costs. As example of using criteria one of the most widely known in industry software tool for requirements development and management was analyzed for compliance with the chosen criteria.

Cyber security standards are often used to ensure the security of industrial control systems. Nowadays, these systems are becoming more decentralized, making them more vulnerable to cyber attacks. One of the challenges of implementing cyber security standards for industrial control systems is the inability to verify early that they are compliant with the relevant standards. Cyber security standard compliance is also only validated and not formally verified, often not providing strong proofs of correct use of cyber security standard. In this paper, we propose an approach that uses formal analysis to achieve this. We formally define building blocks necessary to define the system formally in order to enable formal modeling of the system and carry out the analysis using the Alloy Analyzer. Our approach can be used at an early design stage, where problems are less expensive to correct, to ensure that the system has the desired security properties. We show the applicability of our approach by modeling two distinct cyber attacks and mitigations strategies used to defend against these attacks and also evaluate our approach based on its flexibility to handle and combine different aspects of the cyber security standards. We discuss the future directions of our research.

When developing programs in high-level languages, developers have to make assumptions about the correctness of the compiler. However, this may be unacceptable for critical systems. As long as there are no full-fledged formally verified compilers, the author proposes to solve this problem by proving the correctness of the generated machine code by deductive verification. To achieve this goal, it is required to combine the pre- and postcondition specifications with the machine code behavior model. The paper presents an approach how to combine them for the case of C functions without loops. The essence of the approach is to build models, both machine code and its specifications in a single logical language, and use target processor ABI to bind machine registers with the parameters of the high-level function. For the successful implementation of this approach, you have to take a number of measures to ensure the compatibility of the high-level specification model with the machine code behavior model. Such measures include the use of a register type in the high-level specifications and the translation of the pre- and postconditions into the abstract predicates. Also in the paper the choice of logical language for building models is made and justified, the most suitable tools for implementing the approach of merging specifications are selected and the evaluation of the system of deductive verification of machine code built on the basis of the proposed approach is made using test examples obtained by compiling C programs without loops.

The verification and analysis of distributed systems is a task of utmost importance, especially in today’s world where many critical services are completely supported by different computer systems. Among the solutions for system modelling and verification, it is particularly useful to combine the usage of different analysis techniques. This also allows the application of the best formalism or technique to different components of a system. The combination of Colored Petri Nets (CPNs) and Automata Theory has proved to be a successful formal technique in the modelling and verification of different distributed systems. In this context, this paper presents Prosega/CPN ( Protocol Sequence Generator and Analyzer ), an extension of CPN Tools for supporting automata-based analysis and verification. The tool implements several operations such as the generation of a minimized deterministic finite-state automaton (FSA) from a CPN’s occurrence graph, language generation, and FSA comparison. The solution is supported by the Simulator Extensions feature whose development has been driven by the need of integrating CPN with other formal methods. Prosega/CPN is intended to support a formal verification methodology of communication protocols; however, it may be used in the verification of other systems whose analysis involves the comparison of models at different levels of abstraction. For example, business strategy and business processes. An insightful use case is provided where Prosega/CPN has been used to analyze part of the IEEE 802.16 MAC connection management service specification.

The paper presents an approach to verification of commutation components of Systems-on-Chip. The core idea is to verify bus controllers and supporting interface parts connected to a reference model at unit-level. The reference model in the approach is suggested to be written in SystemC so that to be easily adjusted to the required bus parameters. The in-house prototype implementing the approach has been applied to the verification of a Verilog model of Wishbone controller. There is a possibility to extend the approach to support other busses and protocols by development of the interface library.

FSM (Finite State Machines) are widely used for deriving tests with guaranteed fault coverage for control systems. Distinguishing sequences (DS) are used in FSM based testing for state identification and can significantly reduce the size of a returned complete test suite. In some cases, length of distinguishing sequence can be exponential with respect to the size of the FSM specification. Moreover, DS can be even longer for non-deterministic FSMs, which are used for the specification optionality description when deriving tests for real systems. Unfortunately, DS not always exist for deterministic and non-deterministic FSMs. Adaptive DS (or corresponding distinguishing test cases (DTC)) are known to exist more often and be much shorter than the preset ones that makes adaptive DS attractive for test derivation. In this paper, we investigate the properties of adaptive DS and propose an approach for optimizing the procedure for the adaptive DS derivation. For this purpose, we propose to limit the height of a DTC and correspondingly to reduce the size of a distinguishing FSM that is used for the DTC derivation in the original procedure. The efficiency of a proposed optimized procedure is evaluated by computer experiments for randomly generated FSMs up to 100 states. We also present the experimental results on checking the percentage of randomly generated FSMs when a DTC exists.

Electronic voting systems are a future alternative to traditional methods of voting. It is important to verify the main algorithms on which system security is based. This paper analyzes the security of the cryptographic protocol at the registration stage, which is used in the electronic voting system based on blind intermediaries created by the authors. The registration protocol is described, the messages transmitted between the parties are shown and their content is explained. The Dolev-Yao threat model is used during protocols modeling. The Avispa tool is used for analyzing the security of the selected protocol. The protocol is described in CAS+ and subsequently translated into the HLPSL (High-Level Protocol Specification Language) special language with which Avispa work. The description of the protocol includes roles, data, encryption keys, the order of transmitted messages between parties, parties’ knowledge include attacker, the purpose of verification. The verification goals of the cryptographic protocol for resistance to attacks on authentication, secrecy and replay attacks are set. The data that a potential attacker may possess is detected. The security analysis of the registration protocol was made. The analysis showed that the objectives of the audit were put forward. A detailed diagram of the messages transmission and their contents is displayed in the presence of an attacker who performs a MITM-attack (Man in the middle). The effectiveness of protocol protection from the attacker actions is shown.

This article describes our ongoing research on auto-calibration and synchronization of camera and MEMS-sensors. The research is applicable on any system that consists of camera and MEMS-sensors, such as gyroscope. The main task of our research is to find such parameters as the focal length of camera and the time offset between sensor timestamps and frame timestamps, which is caused by frame processing and encoding. This auto-calibration makes possible to scale computer vision algorithms (video stabilization, 3D reconstruction, video compression, augmented reality), which use frames and sensor’s data, to a wider range of devices equipped with a camera and MEMS-sensors. In addition, auto-calibration allows completely abstracting from the characteristics of a particular device and developing algorithms that work on different platforms (mobile platforms, embedded systems, action cameras) independently of concrete device’s characteristics as well. The article describes the general mathematical model needed to implement such a functionality using computer vision techniques and MEMS-sensors readings. The authors present a review and comparison of existing approaches to auto-calibration and propose own improvements for these methods, which increase the quality of previous works and applicable for a general model of video stabilization algorithm with MEMS-sensors.

Extracting various valuable medical information from head MRI and CT series is one of the most important and challenging tasks in the area of medical image analysis. Due to the lack of automation for many of these tasks, they require meticulous preprocessing from the medical experts. Nevertheless, some of these problems may have semi-automatic solutions, but they are still dependent on the person's competence. The main goal of our research project is to create an instrument that maximizes series processing automation degree. Our project consists of two parts: a set of algorithms for medical image processing and tools for its results interpretation. In this paper we present an overview of the best existing approaches in this field, as well the description of our own algorithms developed for similar tissue segmentation problems such as eye bony orbit and brain tumor segmentation based on convolutional neural networks. The investigation of performance of different neural network models for both tasks as well as neural ensembles applied to brain tumor segmentation is presented. We also introduce our software named "MISO Tool" which is created specifically for this type of problems. It allows tissues segmentation using pre-trained neural networks, DICOM pixel data manipulation and 3D reconstruction of segmented areas.

The article explores the possibility of using an associative-semantic preprocessor for special text processing in natural language. The use of associations allow to abstract from the direct meaning of a word and to replace it with a set of other words. This has also the opposite effect: by typing words (associations) a person is able to restore the search word, which allows to form a query in a natural language without knowing the keywords or terms of a particular domain but at the same time to receive the required result, in contrast to systems oriented to frequency occurrences of words. In the semantic processing of text using associations, the order of words and their number are not important, which allows a person to communicate with the machine without formulating phrases in a special way, since the interactive dialog system itself will process the request clearing everything else. The use of a special text preprocessor based on the associative-semantic processing of text allows interactive systems to be able to understand the topic of the machine's dialogue with the user, improve interaction by communicating in a natural language, and also to simplify the process of system creation and development.

In this survey, online algorithms for such packing problems as Bin Packing, Strip Packing and their generalizations, such as Multidimensional Bin Packing, Multiple Strip Packing and packing into strips of different width were considered. For the latter problem only worst-case analysis was described, for all other problems, both worst-case and average case (probabilistic analysis) asymptotical ratios were considered. Both lower and upper bonds were described. Basic algorithms and methods for their analysis were considered. For worst-case analysis of the Bin Packing Problem it was shown that for any online algorithm R^∞≥1.540, and an algorithm with R^∞≤1.589 was obtained. Both approaches for analyzing the algorithm and obtaining the lower bonds were discussed. Also it was shown that First Fit algorithm for Bin Packing has asymptotical competitive ratio of 17/10. For average case analysis in the case when object’s sizes have a uniform distribution on [0,1] in open-end analysis a construction for obtaining both lower bound of W_ ^n= Ω(√(n ln⁡n )) and algorithm with W_ ^n= θ(√(n ln⁡n )) was shown. In the case of closed-end analysis an algorithm with W_ ^n= θ(√n) was described. For Multidimensional Bin Packing with d dimensions an algorithm with R_ ^∞=(П_∞ )^d, where П_∞≈1.691, was obtained. For average case analysis an algorithm with W_A^n=O(n^((d+1)/(d+2))) was shown. For worst-case analysis of Strip Packing Problem and Multiple Strip Packing Problem algorithms with R^∞≤1.589 were also obtained. For the closed-end average case analysis algorithms with W_ ^n= θ(√n ln⁡n) were described. For the open-end average case analysis of Strip Packing Problem an algorithm with W_ ^n= O(n^(2/3) ) was considered. For generalization of Multiple Strip Packing Problem, where strips have different widths, an online algorithm with R_ ^∞≤2e/r for any r<1, where e=2.718…, was described.