Статьи журнала - Труды Института системного программирования РАН

Все статьи: 115

Experiments on parallel composition of timed finite state machines

Experiments on parallel composition of timed finite state machines

Sotnikov A.P., Shabaldina N.V., Gromov M.L.

Статья научная

In this paper, we continue our work that is devoted to the parallel composition of Timed Finite State Machines (TFSMs). We consider the composition of TFSMs with timeouts and output delays. We held experiments in order to estimate how often parallel composition of nondeterministic TFSMs (with and without timeouts) has infinite sets of output delays. To conduct these experiments we have created two tools: the first one for converting TFSMs into automata (this tool is integrated into BALM-II), the second one for converting the global automaton of the composition into TFSM. As it was suggested in earlier works, we describe the infinite sets of output delays by linear functions, and it is important to know how often these sets of linear functions appear to justify the importance of future investigations of the TFSM parallel compositions (especially for deriving cascade composition). Results of the experiments show significant amount (around 50 %) of TFSMs with infinite number of output delays. We also estimate the size of the global automaton and the composed TFSM. In the experiments, we do not consider global automata with the huge number of states (more then 10000).

Бесплатно

Extracting architectural information from source code of ARINC 653-compatible application software using CEGAR-based approach

Extracting architectural information from source code of ARINC 653-compatible application software using CEGAR-based approach

Lesovoy S.L.

Статья научная

It may be useful to analyze and reuse some components of legacy systems during development of new systems. By using a model-based approach it is possible to build an architecture model from the existing source code of the legacy system. The purpose of using architecture models is to analyze the system's static and dynamic features during the development process. These features may include real-time performance, resources consumption, reliability etc. The architecture models can be used as for system analysis as well as for reusing some components of the legacy system in the new design. In many cases it will allow to avoid creation of a new system from scratch. For creation of the architectural models various modeling languages can be used. In the present work Architecture Analysis & Design Language (AADL) is used. The paper describes an algorithm of extracting architectural information from source code of ARINC 653-compatible application software. ARINC 653 specification defines the requirements for software components of Integrated Modular Avionics (IMA) systems. To access the various services of ARINC 653 based OS an application software uses function calls defined in the APplication/Executive (APEX) interface. Architectural information in source code of application software compliant with ARINC 653 specification includes different objects and their attributes such as processes in each partition, objects for interpartition and intrapartition communications, as well as global variables. To collect the architectural information, it is necessary to extract all APEX calls from source code of application software. The extracted architectural information can be further used for creation the architecture models of the system. For source code analysis an approach based on Counterexample-guided abstraction refinement (CEGAR) algorithm is used. CEGAR algorithm explores possible execution paths of the program using its representation in the form of Abstract Reachability Graph (ARG). In a classical CEGAR algorithm a path in a program to be explored is called a counterexample and it means a path to the error state. In CPAchecker tool the basic predicate-based CEGAR algorithm has been extended for explicit-value analysis. In this paper the extended for explicit-value analysis CEGAR algorithm is applied for the task of extracting architecture information from source code. The main contribution of this paper is the application the ideas of counterexample and path feasibility check for the task of extracting the architectural information from source code.

Бесплатно

In-kernel memory-mapped I/O device emulation

In-kernel memory-mapped I/O device emulation

Cheptsov V.Yu., Khoroshilov A.V.

Статья научная

Device emulation is a common necessity that arises at various steps of the development cycle, hardware migration, or reverse-engineering. While implementing the algorithms behind the device may be a nontrivial task by itself, connecting the emulator to an existing environment, such as drivers intended to work with the actual hardware, may be no less complex. Devices relying on memory-mapped input/output are of a particular interest, because unlike port-mapped input/output there is much less of a chance that the target platform provides a direct interface to intercept the transmissions. A well-known approach used in various virtual machine software is to put the entire operating system under a hypervisor and build the emulator externally. This may not be desirable for reasons like hypervisor complexity, performance loss, and additional requirements for the host hardware. In this paper we extend this approach to the kernel and explain how it may be possible to build the emulator by relying on the existing interfaces provided by an operating system. Given the common availability of an MMU unit as well as memory protection mechanisms, allowing the handling of page or segment traps at read or write access, we presume that a suggested technique of intercepting memory-mapped input/output could be implemented in a broad number of target platforms. To illustrate the specifics and show potential issues we provide the ways to simplify the implementation and optimize it in speed depending on the target capabilities, the protocol emulated, and the project requirements. As a working proof we created a SMC emulator for an x86 target, which makes use of this approach.

Бесплатно

Information retrieval and analysis for a modern organization

Information retrieval and analysis for a modern organization

Topchyan Artyom

Статья научная

With the growing volume and demand for data a major concern for an Organization is to discover what data there actually is, what it contains and how it is being used and by who. The amount of data and the disparate systems used to handle this data increase in their number and complexity every year and unifying these systems becomes more and more complex. In this work we describe an Intelligent search engine system, specifically designed to tackle the problem of information retrieval and sharing in a large multifaceted organization, that already has many systems in place for each Department, which is an integral part of a joint Operational Data Platform(ODP) for data exploration and processing.

Бесплатно

Investigating concurrency in the co-simulation orchestration engine for Into-CPS

Investigating concurrency in the co-simulation orchestration engine for Into-CPS

Thule C., Larsen P.G.

Статья научная

The development of Cyber-Physical Systems often involves cyber elements controlling physical entities, and this interaction is challenging because of the multi-disciplinary nature of such systems. It can be useful to create models of the constituent components and simulate these in what is called a co-simulation, as it can help to identify undesired behaviour. The Functional Mock-up Interface describes a tool-independent standard for constituent components participating in such a co-simulation and can support different formalisms. This paper describes an exploration of whether different concurrency features in Scala (actors, parallel collections, and futures) increase the performance of an existing application called the Co-Simulation Orchestration Engine performing co-simulations. The investigation was conducted by refactoring the existing application to make it suitable for implementing functionality that takes advantage of the concurrency features. In order to compare the different implementations testing was carried out using four test co-simulations. These test co-simulations were executed using the concurrent implementations and the original sequential implementation, verifying the simulation results, and retrieving the execution times of the simulations. The analysis showed that concurrency can be used to increase the performance in terms of execution time in some cases, but in order to achieve optimal performance, it is necessary to combine different strategies. Based on these results, future work tasks has been proposed.

Бесплатно

Language for describing templates for test program generation for microprocessors

Language for describing templates for test program generation for microprocessors

Tatarnikov A.D.

Статья научная

Test program generation and simulation is the most widely used approach to functional verification of microprocessors. High complexity of modern hardware designs creates a demand for automated tools that are able to generate test programs covering non-trivial situations in microprocessor functioning. The majority of such tools use test program templates that describe scenarios to be covered in an abstract way. This provides verification engineers with a flexible way to describe a wide range of test generation tasks with minimum effort. Test program templates are developed in special domain-specific languages. These languages must fulfill the following requirements: (1) be simple enough to be used by verification engineers with no sufficient programming skills; (2) be applicable to various microprocessor architectures and (3) be easy to extend with facilities for describing new types of test generation tasks. The present work discusses the test program template description language used in the reconfigurable and extensible test program generation framework MicroTESK being developed at ISP RAS. It is a flexible Ruby-based domain-specific language that allows describing a wide range of test generation tasks in terms of hardware abstractions. The tool and the language have been applied in industrial projects dedicated to verification of MIPS and ARM microprocessors.

Бесплатно

Language support for generic programming in object-oriented languages: design challenges

Language support for generic programming in object-oriented languages: design challenges

Belyakova Julia

Статья научная

It is generally considered that object-oriented (OO) languages provide weaker support for generic programming (GP) as compared with functional languages such as Haskell or SML. There were several comparative studies which showed this. But many new object-oriented languages have appeared in recent years. Have they improved the support for generic programming? And if not, is there a reason why OO languages yield to functional ones in this respect? In the earlier comparative studies object-oriented languages were usually not treated in any special way. However, the OO features affect language facilities for GP and a style people write generic programs in such languages. In this paper we compare ten modern object-oriented languages and language extensions with respect to their support for generic programming. It has been discovered that every of these languages strictly follows one of the two approaches to constraining type parameters. So the first design challenge we consider is “which approach is better”. It turns out that most of the explored OO languages use the less powerful one. The second thing that has a big impact on the expressive power of a programming language is language support for multiple models. We discuss pros and cons of this feature and its relation to other language facilities for generic programming.

Бесплатно

MHD supersonic flow control: OpenFOAM simulation

MHD supersonic flow control: OpenFOAM simulation

Ryakhovskiy A.I., Schmidt A.A.

Статья научная

MHD flow control is a relevant topic in today’s aerospace engineering. An OpenFOAM density-based solver that is capable of handling MHD supersonic flow problems with constant magnetic field is developed. The proposed solver is based on Balbas-Tadmor central difference schemes. This solver can be applied to studying the potential of MHD flow control systems for atmospheric entry vehicles. A supersonic flow around a spherically blunt cone both with and without MHD interaction is studied. Gases with thermodynamic parameters characteristic for Earth’s and Martian atmospheres are considered. The results show visible effect of magnetic field on surface temperature of the body. The differences between shock standoff distances and general shockwave configurations of MHD and non-MHD flow are also apparent. The solution is stable for Stuart number below 0.2. Conditional instability of the solver can be attributed to the MHD term’s contribution to the local speed of sound and can be avoided by taking it into account. The developed application has proven the suitability of the used schemes for resolving steep gradients in MHD supersonic flow problems. The study itself has shown theoretical possibility of studying the MHD flow control using OpenFOAM. Further research may include an effort to stabilize the solver and to enhance the mathematical model of the flow.

Бесплатно

Memristor-based hardware neural networks modelling review and framework concept

Memristor-based hardware neural networks modelling review and framework concept

Kozhevnikov D.D., Krasilich N.V.

Статья научная

This paper is a report of a study in progress that considers development of a framework and environment for modelling hardware memristor-based neural networks. An extensive review of the domain has been performed and partly reported in this work. Fundamental papers on memristors and memristor related technologies have been given attention. Various physical implementations of memristors have mentioned together with several mathematical models of the metal-dioxide memristor group. One of the latter has been given a closer look in the paper by briefly describing model’s mechanisms and some of the important observations. The paper also considers a recently proposed architecture of memristor-based neural networks and suggests enhancing it by replacing the utilized memristor model with a more accurate one. Based on this review, a number of development requirements was derived and formally specified. Ontological and functional models of the domain at hand have been proposed to foster understanding of the corresponding field from different points of view. Ontological model is supposed to shed light onto the object-oriented structure of memristor-based neural network, whereas the functional model exposes the underlying behavior of network’s components which is described in terms of mathematical equations. Finally, the paper shortly speculates about the development platform for the framework and its prospects.

Бесплатно

Methods of protecting decentralized autonomous organizations from crashes and attacks

Methods of protecting decentralized autonomous organizations from crashes and attacks

Andryukhin A.A.

Статья научная

Field of study: Blockchain technology, decentralized autonomous organizations, smart contract and their resistance to attacks and failures. Theoretical and practical significance: Due to the fact that such a form of organization is experimental, participants often face problems of attacks on the organization, the consequences of incorrectly written rules and of fraud. The task of creating decentralized autonomous organizations that are resistant to failures and attacks, and research on the causes of such problems has become relevant for software developers and architects. Goals and objectives of work: Investigation of attack algorithms and development of methods for ensuring the sustainability of decentralized autonomous organizations for attacks on the basis of analysis of the subprocesses of border events and logs using the methods of Process Mining. The methods to be developed should promptly identify and prevent inconsistencies between the alleged and actual behavior of smart contracts that lead to such errors in the operation, such as the content of spam contracts, empty transactions, increased block processing time, etc.

Бесплатно

Modelling the people recognition pipeline in access control systems

Modelling the people recognition pipeline in access control systems

Gossen F., Margaria T., Gke T.

Статья научная

We present three generations of prototypes for a contactless admission control system that recognizes people from visual features while they walk towards the sensor. The system is meant to require as little interaction as possible to improve the aspect of comfort for its users. Especially for people with impairments, such a system can make a major difference. For data acquisition, we use the Microsoft Kinect 2, a low-cost depth sensor, and its SDK. We extract comprehensible geometric features and apply aggregation methods over a sequence of consecutive frames to obtain a compact and characteristic representation for each individual approaching the sensor. All three prototypes implement a data processing pipeline that transforms the acquired sensor data into a compact and characteristic representation through a sequence of small data transformations. Every single transformation takes one or more of the previously computed representations as input and computes a new representation from them. In the example models presented in this paper, we are focusing on the generation of frontal view images of peoples’ faces, which is part of the processing pipeline of our newest prototype. These frontal view images can be obtained from colour, infrared and depth data by rendering the scene from a changed viewport. This pipeline can be modelled considering the data flow between data transformations only. We show how the prototypes can be modelled using modelling frameworks and tools such as Cinco or the Cinco-Product Dime. The tools allow for modelling the data flow of the data processing pipeline in an intuitive way.

Бесплатно

On the model checking of finite state transducers over semigroups

On the model checking of finite state transducers over semigroups

Gnatenko A.R., Zakharov V.A.

Статья научная

Sequential reactive systems represent programs that interact with the environment by receiving signals or requests and react to these requests by performing operations with data. Such systems simulate various software like computer drivers, real-time systems, control procedures, online protocols etc. In this paper, we study the verification problem for the programs of this kind. We use finite state transducers over semigroups as formal models of reactive systems. We introduce a new specification language LP-CTL* to describe the behavior of transducers. This language is based on the well-known temporal logic CTL* and has two distinguished features: 1) each temporal operator is parameterized with a regular expression over input alphabet of the transducer, and 2) each atomic proposition is specified by a regular expression over the output alphabet of the transducer. We develop a tabular algorithm for model checking of finite state transducers over semigroups against LP-CTL* formulae, prove its correctness, and estimate its complexity. We also consider a special fragment of LP-CTL* language, where temporal operators are parameterized with regular expressions over one-letter alphabet, and show that this fragment may be used to specify usual Kripke structures, while it is more expressive than usual CTL*.

Бесплатно

On the verification of strictly deterministic behavior of timed finite state machines

On the verification of strictly deterministic behavior of timed finite state machines

Vinarskii E.M., Zakharov V.A.

Статья научная

Finite State Machines (FSMs) are widely used as formal models for solving numerous tasks in software engineering, VLSI design, development of telecommunication systems, etc. To describe the behavior of a real-time system one could supply FSM model with clocks - a continuous time parameters with real values. In a Timed FSM (TFSM) inputs and outputs have timestamps, and each transition is equipped with a timed guard and an output delay to indicate time interval when the transition is active and how much time does it take to produce an output. A variety of algorithms for equivalence checking, minimization and test generation were developed for TFSMs in many papers. A distinguishing feature of TFSMs studied in these papers is that the order in which output letters occur in an output timed word does not depend on their timestamps. We think that such behavior of a TFSM is not realistic from the point of view of an outside observer. In this paper we consider a more advanced and adequate TFSM functioning; in our model the order in which outputs become visible to an outsider is determined not only by the order of inputs, but also by de lays required for their processing. When the same sequence of transitions is performed by a TFSM modified in a such way, the same outputs may follow in different order depending on the time when corresponding inputs become available to the machine. A TFSM is called strictly deterministic if every input timed word activates no more than one sequence of transitions (trace) and for any input timed word which activates this trace the letters in the output words always follows in the same order (but, maybe, with different timestamps). We studied the problem of checking whether a behavior of an improved model of TFSM is strictly deterministic. To this end we showed how to verify whether an arbitrary given trace in a TFSM is steady, i.e. preserves the same order of output letters for every input timed word which activates this trace. Further, having the criterion of trace steadiness, we developed an exhaustive algorithm for checking the property of strict determinacy of TFSMs. Exhaustive search in this case can hardly be avoided: we proved that determinacy checking problem for our model of TFSM is co-NP-hard.

Бесплатно

Parallel processing and visualization for results of molecular simulation problems

Parallel processing and visualization for results of molecular simulation problems

Puzyrkov D.V., Podryga V.O., Polyakov S.V.

Статья научная

In this paper authors presents “mmdlab” library for the interpreted programming language Python. This library allows to carry out reading, processing and visualization of the results of numerical calculations in the tasks of molecular simulation. Considering the large volume of data obtained from such simulations, there is a need in parallel realization of algorithms for processing those volumes. Parallel processing should be performed on multicore systems, such as common scientific workstation, and on super-computer systems and clusters, where the MD simulations were held. During the development process we have study the effectiveness of the Python language for such tasks, and we have examined the tools for it’s acceleration. As well, we studied multiprocessing capabilities and tools for cluster computation using this language. Also we have investigated the problems of receiving and processing the data, located on multiple computational nodes. This was prompted by the need to process the data, produced by parallel algorithm, that was executed on multiple computational nodes, and saves its output on each of them. As a tool for scientific visualization was chosen an open-source “Mayavi2” package. The developed ”mmdlab” library was used in the analysis of the results of MD simulation of the gas and metal plate interaction. As a result, we managed to observe the effect of adsorption in details, which is important for many practical applications.

Бесплатно

Practical experience of software and system engineering approaches in requirements management for software development in aviation industry

Practical experience of software and system engineering approaches in requirements management for software development in aviation industry

Koverninskiy I.V., Kan A.V., Volkov V.B., Popov Yu. S., Gorelits N.K.

Статья научная

The article describes the technical world evolution tendencies, which require proper software and system engineering approaches used for complex systems creation, for example for aircrafts creation. The substantiation of the importance and relevance of using requirements management discipline in software development is made. The main basics of software and system engineering approaches and discipline are set out. System engineering is a discipline, which integrates and harmonizes all activities around entire area of systems creation. The article contains description of information systems, which have been created in GosNIIAS and now are actively used in internal and external works: requirements management information system, problem reports management information system, technological environment for test methods preparation and test results registration. Requirements management information system contains special predefined documents and template, required by standards DO-178, DO-254, DO-330, ARP4754, State Standards GOST 51904 and GOST 34. Using of requirements management system in GosNIIAS and external enterprises is described. Problem reports management information system registers and supports the lifecycle of problem reports, which appear during the work process. Technological environment for test methods preparation and test results registration supports different activities such as test methods, test cases, test procedures preparation and testing on the integration stand, test results registration and test protocols preparation. Some perspective directions of software and system engineering approaches applying in GosNIIAS are listed.

Бесплатно

Refinement types in Jolie

Refinement types in Jolie

Tchitchigin Alexander, Safina Larisa, Elwakil Mohamed, Mazzara Manuel, Montesi Fabrizio, Rivera Victor

Статья научная

Jolie is the first language for microservices and it is currently dynamically type checked. This paper considers the opportunity to integrate dynamic and static type checking with the introduction of refinement types, verified via an SMT solver. The integration of the two aspects allows a scenario where the static verification of internal services and the dynamic verification of (potentially malicious) external services cooperate in order to reduce testing effort and enhance security. Refinement types are well-known technique for numeric, array and algebraic data types. They rely on corresponding SMT-theories. Recently SMT solvers got support for a theory of strings and regular expressions. In the paper, we describe possible application of the theory to string refinement types. We use Jolie programming language to illustrate feasibility and usefulness of such extension. First, because Jolie already has syntax extension to support string refinements. We build on top of that extension to provide static type checking. Second, because in the realm of microservices the need for improved checking of string data is much higher as most of external communication goes through text-based protocols. We present simplified but real-world example from the domain of web-development. We intentionally introduce a bug in the example demonstrating how easily it can slip a conventional type system. Proposed solution is feasible, as it do not accept program with the bug. Complete solution will need enhancements in precision and error reporting.

Бесплатно

Scalable sandbox environments for a modern organization

Scalable sandbox environments for a modern organization

Topchyan Artyom

Статья научная

With the growing volume and demand for data, a major concern for an Organization is the creation of collaborative Data-Driven projects. With the amount of data, number of departments and the development of potential use cases, the complexity of creating Multitenant and Collaborative environments for multidisciplinary teams to work and create productive solutions, is becoming more and more important problem. In this work, we describe an approach to building such an environment with scalability, flexibility and productivity in mind. This solution is an integral part of a joint Operational Data Platform for data exploration and processing at large data driven Organizations.

Бесплатно

Simulating behavior of multi-agent systems with acyclic interactions of agents

Simulating behavior of multi-agent systems with acyclic interactions of agents

Nesterov R.A., Mitsyuk A.A., Lomazova I.A.

Статья научная

In this paper, we present an approach to model and simulate models of multi-agent systems (MAS) using Petri nets. A MAS is modeled as a set of workflow nets. The agent-to-agent interactions are described by means of an interface. It is a logical formula over atomic interaction constraints specifying the order of inner agent actions. Our study considers positive and negative interaction rules. In this work, we study interfaces describing acyclic agent interactions. We propose an algorithm for simulating the MAS with respect to a given interface. The algorithm is implemented as a ProM 6 plug-in that allows one to generate a set of event logs. We suggest our approach to be used for evaluating process discovery techniques against the quality of obtained models since this research area is on the rise. The proposed approach can be used for process discovery algorithms concerning internal agent interactions of the MAS.

Бесплатно

Specification-based test program generation for MIPS64 memory management units

Specification-based test program generation for MIPS64 memory management units

Kamkin A.S., Kotsynyak A.M.

Статья научная

In this paper, a tool for automatically generating test programs for MIPS64 memory management units is described. The solution is based on the MicroTESK framework being developed at the Institute for System Programming of the Russian Academy of Sciences. The tool consists of two parts: an architecture-independent test program generation core and MIPS64 memory subsystem specifications. Such separation is not a new principle in the area: it is applied in a number of industrial test program generators, including IBM’s Genesys-Pro. The main distinction is in how specifications are represented, what sort of information is extracted from them, and how that information is exploited. In the suggested approach, specifications comprise descriptions of the memory access instructions, loads and stores, and definition of the memory management mechanisms such as translation lookaside buffers, page tables, table lookup units, and caches. A dedicated problem-oriented language, called mmuSL, is used for the task. The tool analyzes the mmuSL specifications and extracts all possible instruction execution paths as well as all possible inter-path dependencies. The extracted information is used to systematically enumerate test programs for a given user-defined test template and allows exhaustively exercising co-execution of the template instructions, including corner cases. Test data for a particular program are generated by using symbolic execution and constraint solving techniques.

Бесплатно

Static dependency analysis for semantic data validation

Static dependency analysis for semantic data validation

Ilyin D.V., Fokina N.Yu., Semenov V.A.

Статья научная

Modern information systems manipulate data models containing millions of items, and the tendency is to make these models even more complex. One of the most crucial aspects of modern concurrent engineering environments is their reliability. The principles of ACID (atomicity, consistency, isolation, durability) are aimed at providing it, but directly following them leads to serious performance drawbacks on large-scale models, since it is necessary to control the correctness of every performed transaction. In the paper, a method for incremental validation of object-oriented data is presented. Assuming that a submitted transaction is applied to originally consistent data, it is guaranteed that the final data representation is also consistent if only the spot rules are satisfied. To identify data items subject to spot rule validation, a bipartite data-rule dependency graph is formed. To automatically build the dependency graph a static analysis of the model specifications is proposed to apply. In the case of complex object-oriented models defining hundreds and thousands of data types and semantic rules, the static analysis seems to be the only way to realize the incremental validation and to make possible to manage the data in accordance with the ACID principles.

Бесплатно

Журнал