Insertion Semantics of VHDL as Electronic Design Languge

Cybernetics and Systems Analysis - The paper considers the problem of insertion semantics of hardware specifications, in particular, the VHDL language. The creation of semantics is necessary to...     

Fuzz Testing Technique and its Use in Cybersecurity Tasks

The paper considers the technology of fuzz testing, which is testing software systems by feeding critical or unexpected input data to them. An overview of the current problem state is made and the main systems of fuzz testing are presented. An approach to the fuzz testing technology with the use of algebraic methods, in particular, symbolic modeling, is considered. The lightweight algorithm, which is designed to reduce test generation time, is considered. The algorithm is implemented in the environment of an insertion modeling system and tested in older system versions developed in Linux.

     

Trapezoid method for solving systems of linear inequalities and its implementation in insertion modeling

A new method for solving systems of linear inequalities (trapezoid method) is developed. The method involves constructing canonical forms of a system of linear inequalities. Canonical forms represent a partition of the convex polyhedron of solutions of the system into a union of disjoint trapezoids. The result of using this method is a set of basis vectors of the polyhedron of solutions. An insertion model of the algorithm is presented.     

Algorithm and Tools for Constructing Canonical Forms of Linear Semi-Algebraic Formulas

The results of testing formula simplification tools are presented in the first part of this paper. In the second part, an algorithm for constructing canonical forms of linear semi-algebraic formulas is described. The main result of the study is the definition of the canonical form of a linear semi-algebraic formula that has the property of uniqueness and other useful properties. An algorithm for constructing such a formula is described.     

Approach to behavior scenarios debugging

The paper presents two approaches to debugging of application model behavior scenarios: semi-automatic and automatic. The first approach allows the user to automate the process of finding a place in a concrete symbolic behavioral scenario that caused an error. The second approach allows to find together with places the cause of multiple errors in some set of generated behavior scenarios in a single analysis cycle.     

Modern Methods and Software Systems of Molecular Modeling and Application of Behavior Algebra

Cybernetics and Systems Analysis - The main methods of molecular modeling and specialized software for the development and analysis of molecular models are considered. In particular, the article...     

Properties of a predicate transformer of the VRS system

Models specified in the language of basic protocols are considered. These models are attribute transition systems, and their states are defined by formulas of multisort first-order predicate calculus over system attributes. Attributes of simple numeric and symbolic types, functional types, and queues are allowed. Assignment operators, queue update operators, and arbitrary formulas are used in postconditions of basic protocols. To pass from one state to another, a predicate transformer is constructed as a function of formula transformation. The following main property of the predicate transformer is proved: it calculates the strongest postcondition for symbolic states.     

An approach to creating concretized test scenarios within test automation technology for industrial software projects

The paper describes an approach for creation of effective test automation technology for industrial software projects based on a formal model of the system under test, performing its automatic symbolic verification of the model and generation of symbolic traces, then their automatic concretization, generation and execution of test suites. The technology includes means for test results analysis and tests correction and update. High quality of software products is ensured by a balance between static (verification) and dynamic (testing) analysis techniques starting from the earlier development phases and through automation of all phases of software development. Special emphasis is made on presentation of the algorithm of concretization and configuring test scenarios.