Today's number

Download

Resources and tools for teaching the Semantic Web methods

In recent years, both scientific and commercial organizations have generated a significant amount of structured data. On the basis of this data, numerous applications are being developed, which makes it necessary for modern IT specialists to get acquainted with this trend. This paper discusses the important aspects of the Semantic Web evolution and the experience of teaching the methods and tools of the Semantic Web.
Download

Optimizing transformations in the predicate programming system

The following optimizing transformations: variable gluing, replacement of the tail recursion by a loop, in-line substitution, reduction - are described. Effective imperative program is the result of transformation application. Dataflow analysis of a program is applied to perform transformations.
Download

SoRuCom-2017: International Conference on the History of Informatics

The article presents the results of the 4th International Conference “The development of computer technology in Russia and in the former USSR: history and prospects” (SoRuCom-2017) Zelenograd, Moscow, 3-5 October 2017. Our Institute was among the most active organizers of the Conference. The conference was supported by the Russian Foundation for Basic Research, Grant 17-07-20538, Computer History Museum (USA, CA), and Russian citizen Vladimir Kurlyandchik.
Download

Logical-probabilistic method for controlling modular robots

This work presents a logical-probabilistic method for adaptive control of modular systems based on the use of the modules functional similarity and the logical-probabilistic algorithm of the guided search of rules. The proposed method is based on the joint learning of the control modules, starting with finding the common control rules for all modules and finishing with their subsequent specification in accordance with the ideas of the probabilistic inference. With an interactive 3D simulator, a number of successful experiments were carried out to train four virtual models of robots. Experimental studies have shown that the proposed approach is quite effective and can be used to manage modular systems with many degrees of freedom.
Download

An ontology-based information retrieval method

This paper presents a method of information retrieval based on the ontology of scientific activity. This method makes use of general-purpose search engines to retrieve links to relevant Internet resources using the search queries generated on the basis of the ontology concepts and thesaurus. Search results that do not contain information about scientific activity are filtered using ontology.
Download

Development of automated evaluating systems for programming tasks

The article considers the twenty-year history and experience of creating automated systems for testing knowledge and skills in programming at the Novosibirsk State University. An analysis of the effectiveness or ineffectiveness of methods and means in the knowledge testing systems in use is given. The modern state of the architecture of the NSUts system is described.
Download
Many variants of the communication sliding window protocol were specified and verified using various techniques like theorem proving, model checking and their combinations. In this paper we consider a specification of the Sliding window protocol as a multi-agent affine model. Temporal and epistemic properties of the protocol are expressed in Logic of Knowledge and Time.
Download
This paper presents the approach to creation of computational platforms in the basics of UGENE Workflow Designer. This platform is based on the internal programming language. It demonstrates a method of keeping the system consistent and handy to maintain and develop if you follow the concepts of the platform internal model and the concepts of the programming language syntax. UGENE Workflow Designer is designed to solve the bioinformatics tasks; and the UWL language is the DSL of bioinformatics. The paper describes the feature of how to reuse the basics of the platform in some other application areas.
Download
During the semicentennial history of Computer Science and Information Technologies, several thousands of computer languages have been created. The computer language universe includes languages for different purposes (programming, specification, modeling, etc.). In each of these branches of computer languages it is possible to track several approaches (imperative, declarative, object-oriented, etc.), disciplines of processing (sequential, non-deterministic, distributed, etc.), and formalized models, such as Turing machines or logic inference machines. The listed arguments justify the importance of of an adequate classification for computer languages. Computer language paradigms are the basis for the classification of the computer languages. They are based on joint attributes which allow us to differentiate branches in the computer language universe. We present our computer-aided approach to the problem of computer language classification and paradigm identification. The basic idea consists in the development of a specialized knowledge portal for automatic search and updating, providing free access to information about computer languages. The primary aims of our project are the research of the ontology of computer languages and assistance in the search for appropriate languages for computer system designers and developers. The paper presents our vision of the classification problem, basic ideas of our approach to the problem, current state and challenges of the project, and design of query language.
Download
Maximal employment of formal and sound methods is one of the distinctive features of C-light project. This concerns not only the fundamental verification bases, like Plotkin's operational semantics or Hoare's logics, but also implementation aspects. The localization of possible errors is one of them. In the majority of known verification systems such localization is simply coded by developers as a part of system functionality without any formal basis for it. The recent reinforcement of the C-light project by the semantical labeling technique and the choice of LLVM/Clang for the system input block allowed us to obtain some new results, which are surveyed in this paper.
Download
The article presents a strip-method of linear pre-distortion of signals and images using multiple types of transformation matrices. Matrices that are good enough to minimize the amplitude of the noise were determined. The dependence of the quality of data recovery on the location and size of the noise were investigated. Also we found the possibility of using the strip-method in combination with image compression and developed an algorithm that implements this approach.
Download
The authors discuss an intelligent access to information resources. An analysis of information systems which support textual or ontology-based data representation is provided. The authors propose an approach to develop an information system that would support both of the aforementioned ways to represent knowledge. A possible architecture and database schema for such a system are described.
Download
Java bytecode decompilation is a process of reverse translation that restores Java source code by the corresponding bytecode. Java bytecode is an intermediate representation based on abstract stack machine. It may have arbitrary control flow graph, whereas the Java language contains control structures that always form a strict hierarchy. Decompilation aims at restoring all control structures, including Java exception handling blocks. In the Excelsior RVM (Java Virtual Machine with a static compiler), bytecode is decompiled in a structural intermediate representation for further optimization. When building exception handling blocks, the Excelsior RVM’s compiler assumes that the bytecode must be emitted by the standard Java source to bytecode compiler and uses a few heuristics to make reverse transformation. However, it is not always possible if the bytecode is produced by other instruments. This paper presents a decompilation algorithm that produces exception handling blocks given any correct bytecode. The algorithm has been implemented, integrated into the Excelsior RVM and tested on real-world applications.
Download
This paper presents some popular classical methods used for time series analysis and prediction. At first relatively simple models of averaging and smoothing are described, then autoregressive and moving average models, and a “mixed” autoregressive-moving-average model as a result of crossing of the latter two mentioned models. At last an autoregressive integrated moving average model is described.
Download
Before RNA transcription starts, special segments of DNA form a complex of regulatory proteins called transcription factors. This complex allows RNA polymerase to be bound to DNA and to start reading RNA. It is a difficult problem to search binding sites on DNA because of many factors influencing the binding. In particular, other sites in the vicinity of a given site may influence binding. To reveal those dependencies the authors introduce histograms of density distribution of binding sites, called genomic profiles. The software package developed in the scope of this work allows building genomic profiles using the prediction of binding sites by a weight matrices algorithm for different implementations: for multicore CPU’s or NVidia GPU’s using CUDA. In addition, the software allows clustering genomic profiles using K-means clustering and hierarchical clustering. The algorithm allows to build samples – random transcription factors hierarchies based on the existing experimental structural classification to estimate the correspondence between genomic profiles construction and the existing classification. The analysis of correspondence of genomic profiles with biological classification of transcription factors was developed using the sampling algorithm.
Download
The contribution of the paper is to clarify connections between real-time models of concurrency. In particular, we defined a category of timed causal trees and investigated how it relates to other categories of timed models. Moreover, using a larger model called timed event trees, we constructed an adjunction from the category of timed causal trees to the category of timed event structures. Thereby we showed that timed causal trees are more trivial than timed event structures because they reflect only one aspect of true concurrency, causality, and they apply causality without a notion of event. On the other hand, the first model is more expressive than the latter in that possible runs of a timed causal tree can be defined in terms of a tree without restrictions, but the set of the possible runs of any event structure must be closed under the shuffling of concurrent transitions.
Download
This article examines the issue of storage of digital archives of newspapers. Technology is proposed covering scanning-preparation-publication cycle, and as the key challenges presented: presenting online of editions of newspapers and search for articles by keywords.
Download
The paper considers the problems of information collection for thematic intelligent scientific internet resources providing the systematization and integration of scientific knowledge, information resources, related to certain area of knowledge, and methods of intelligent processing of data contained in them as well as the content-based access to them. The approach to automatization of information collection combining metasearch and knowledge extraction methods based on using ontology and thesaurus of the modeled area of knowledge is proposed.
Download
The language and implementation of string objects are defined. Strings are coded via arrays of chars in the style the C and C++ languages. List constructs are accessible for strings. The list language has been revised to be proper for strings. The paper presents some part of the program library for strings.
Download
Automata-based software engineering is intended to development of simple, reliable, and efficient programs for reactive systems. An automata-based program implements the finite state machine in the form of the hypergraph of control states. A production rule language used to declare the use case requirements is proposed as the specification language for automata-based programs. Methods of program development are presented as the collection of golden rules defining true balance of integration of automata-based, predicate, and object-oriented programming. Methods are illustrated on the example programs.
Download
This paper provides comparison of “Discovery” software system versus Microsoft Association Rules, Decision Trees and Neural Network embedded in Microsoft SQL Server Analysis Services. It is shown that system «Discovery», firstly, has theoretical advantages over these algorithms, secondly, practically works better on the data, where these advantages appear explicitly, and thirdly, well-behaved shows on data taken from a known repository UCI. These results demonstrate the advantages of the Discovery over the methods embedded into Microsoft SQL Server Analysis Services.
Download
This paper pursues the problems of scalability of parallel graph-marking algorithms in the context of garbage collection systems. The authors give a set of constraints inherent to any graph-marking approach and attempt to construct a scalable marking algorithm following these constraints. The resulting algorithm has been implemented in a Java Virtual Machine and evaluated on real-world Java applications. The obtained results indicate a substantial acceleration of marking in most cases.
Download
A new formalism for description of ontologies of systems and their changes - conceptual transition systems - is presented. The basic definitions of the theory of conceptual transition systems are given. These systems were demonstrated to allow to specify both typical and new kinds of ontological elements constituting ontologies. The classification of ontological elements based on such systems is described.
Download
The language CTSL of specification of conceptual transition systems which are a formalism for description of dynamic discrete systems on the basis of their conceptual structure is proposed. The basic kinds of conceptual transition systems are considered. The basic predefined elements and operations of the CTSL language are defined.
Download
The paper presents the materials of the Summer School of Young Programmers held in 2014. The School was started in 1976, on the initiative of Andrei Ershov, an outstanding advocate of programming and computer science development. During the years of its existence, the Summer School has varied the forms and methodical specifics of conducting classes. The number of participants differed from year to year as did the equipment and technology employed. Originally, classes were held for large groups of beginners and "advanced" schoolchildren; consultants from Novosibirsk Academgorodok were involved. The next step was workshops. It took 40 years to go from a few minutes of practice on the BESM- 6 to the many hours of programming on personal computers. However, the most important aspect of the project – the atmosphere of cooperation aimed at creating a sustainable commitment to self-education, assistance in vocational guidance based on practical experience, providing a glimpse of the chosen profession, a conscious choice of way of life, creativity, and socialization – has been carefully preserved. The participants of the Summer School of Young Programmers share not only their profession but also their way of thinking.
Download
There is a gap between program languages theoreticians and practical programmers: the former are strong in science of Abstract Algebra and Formal Logic, the later – in the craft of software development. The paper sketches a very simple approach to algebraic and logic foundations of formal program semantics classification, an approach that should fit practical programmers just with rudimental experience in logic and algebra. In particular, paper presents operational, denotational, axiomatic and second-order semantics for a toy language (that just looks like a programming language).
Download
The paper describes a mathematical model of submission documents. The model includes a description of different types of segments, which are defined in the text using markers. An algorithm for segmenting the document text is given for this model.
Download
We discuss the possibility of studying processes based on their representation as development spirals. The geometric concepts related to the spiral are introduced. This allows modeling the development by projections of processes trajectories on different planes of the space factors.
Download
Subdefinite Models is one of the methods to solve Constraint Satisfaction Problem. The base notion of the method is Sudefiniteness, which defines the set representation of inaccurate values. The paper contains formal definitions of different kinds of Sudefinitness, their comparisons, and descriptions of their properties.
Download
An approach to analyze the compatibility of real-time multi-task applications with various combinations of scheduling modes and protocols of access to shared resources when run on multi-core platforms. The approach is based on the recently introduced notion of application density derived from estimation of application feasibility for various values of the processor performance. The software architecture of a relatively simple simulation tool for estimation of the task response time (and therefore, application feasibility) is described, which provides more exact data compared to the known analytical methods when they are applicable. Results of running this tool on a number of benchmarks, including balanced Liu-Layland configurations, are presented along with their analysis and interpretation. The suggested approach allows to indentify an optimal combination of the scheduling mode and access protocol for the given application structure.
Download
This article presents a method for the analysis and verification of Use Case Maps (UCM) models with scenario control structures – protected components and failure handling constructs. UCM models are analyzed and verified with the help of coloured Petri nets (CPN) and the SPIN model checker. An algorithm for translating UCM scenario control structures into CPN is described. The presented algorithm and the verification process are illustrated by the case study of a network protocol.
Download
Extended Finite State Machines (EFSMs) are widely used when deriving tests for checking whether a software implementation meets functional requirements. These tests usually are derived keeping in mind appropriate test purposes such as covering paths, variables, etc. of the specification EFSM. However, it is well known that such tests do not detect many functional faults in an EFSM implementation. In this paper, we propose an approach for increasing the fault coverage of test suites initially derived against the specification EFSM. For this reason, the behavior of the specification EFSM is implemented in Java using a template that is very close to the EFSM description. At the next step, the fault coverage of an initial test suite derived against the specification EFSM is calculated with respect to faults generated by µJava tool. Since the EFSM software implementation is template based, each undetected fault can be easily mapped into a mutant EFSM of the specification machine. Thus, a distinguishing sequence can be derived not for two programs that is very complex but for two machines and there are efficient methods for deriving such a distinguishing sequence for Finite State Machine (FSM) abstractions of EFSMs. As an FSM abstraction, an l-equivalent of an EFSM can be considered that in fact, is a subtree of the successor tree of height l that describes the EFSM behavior under input sequences of length up to l. Such l-equivalents are classical FSMs and if l is not large then a distinguishing sequence can be derived simply enough. The initial test suite augmented with such distinguishing sequences detects much more functional faults in software implementations of a system described by the specification EFSM.
Download
Finite state transducers over semigroups can be regarded as a formal model of sequential reactive programs. In some cases verification of such programs can be reduced to minimization and equivalence checking problems for this model of computation. To solve efficiently these problems certain requirements are imposed on a semigroup these transducers operate on. Minimization of a transducer over a semigroup is performed in three stages: at first the greatest common left-divisors are computed for all states of a transducer, next a transducer is brought to a reduced form by pulling all such divisors ''upstream'', and finally a minimization algorithm for finite state automata is applied to the reduced transducer. As a byproduct of this minimization technique we obtain an equivalence checking procedure for transducers operating on certain classes of semigroups.
Download
This paper presents three approaches to solve the problem of improving sentiment classification for dynamically updating text collections. The paper describes three methods essentially differing from each other. In this case the supervised machine learning and unsupervised machine learning were applied for sentiment classification. The results of methods along with cases, which method is most applicable are shown in the paper. All the experiments were set and the results were obtained on sufficiently representative text collections.
Download
A closed information system is an information system such that its environment does not change it, and there is an information transfer from it to its environment and from its environment to it. In this paper two formalisms (information query systems and conceptual configuration systems) for abstract unified modelling of the artifacts (concept sketches and models) of the conceptual design of closed information systems, early phase of information systems design process, are proposed. Information query systems defines the abstract unified information model for the artifacts, based on such general concepts as state, information query and answer. Conceptual configuration systems are a formalism for conceptual modelling of information query systems. They defines the abstract unified conceptual model for the artifacts. The basic definitions of the theory of conceptual configuration systems are given. These systems were demonstrated to allow to model both typical and new kinds of ontological elements. The classification of ontological elements based on such systems is described. A language of conceptual configuration systems is defined.
Download
In the paper we describe a verification method for families of distributed systems generated by context-sensitive network grammar of a special kind. The method is based on model checking technique and abstraction. A representative model depends on a specification grammar for family of systems. This model simulates a behavior of the systems in such a way that properties which hold for the representative model are satisfied for all these systems. We show using this method for verification of some properties of multiagent system for resolution of context-dependent ambiguities in ontology population.
Download
Today the common practice of industrial automation is characterized by the following: generally the testing of control algorithms starts only when you run the software on a new facility. As a result the testing of the algorithm is postponed until the start-and-adjustment works begin. The readiness of the algorithm up to this moment is unknown. In the article the concept of virtual plant (VP) was put forward to reduce the risks. To ensure that the control algorithm satisfies necessary requirements the model checking verification method is used.
Download
Developing temporal requirements to distributed program systems an engineer should determine and systemize event sequences caused by system processes interleaving. A number of such sequences grow exponentially that makes the requirement development procedure nontrivial. This is why engineers prefer not to construct or construct elementary formal requirements. As result powerful formal verification methods become unavailable or some important properties of distributed systems leaved unexpressed. While it is well-known, that development of formal requirement even without verification improves an quality of a distributed system structure and functions. In this paper we suggest a method for formal temporal systems development which is easy-to-use. The method is based on scalable patterns of linear temporal logic formulas. Using this method we developed formal temporal requirements to a practical program control system (a vehicle power supply control system). Verifying the requirements with the model checking method we found 3 critical errors that were missed by developers of the vehicle power supply control system during design and testing.
Download
In this paper we consider a procedure of parallel composition construction of Timed Finite State Machines (TFSMs) using BALM-II and suggest different ways of getting linear functions that describe a set of output delays. Our research consists of three steps: at first step we consider composition of TFSMs when an output delay may be a natural number or zero; at second – we add transitions under timeouts; at third we consider composition of TFSMs in general case (when output delays are described as sets of linear functions). This paper is devoted only to the first step of the research.
Download
The paper is dedicated to the specification of the structure and the behavior of software libraries. It describes the existing problems of libraries specifications. A brief overview of the research field concerned with formalizing the specification of libraries and library functions is presented. The requirements imposed on the formalism designed are established; the formalism based on these requirements allows specifying all the properties of the libraries needed for automating several classes of problems: detection of defects in the software, migration of applications into a new environment, generation of software documentation. The conclusion defines potential directions for further research.
Download
A class of information systems considered in this paper is defined as follows: a system belongs to the class if its change can be caused by both its environment and factors inside the system, and there is an information transfer from it to its environment and from its environment to it. Two formalisms (information transition systems and conceptual transition systems) for abstract unified modelling of the artifacts (concept sketches and models) of the conceptual design of information systems of the class, early phase of information systems design process, are proposed. Information transition defines the abstract unified information model for the artifacts, based on such general concepts as state, information query, answer and transition. Conceptual transition systems are a formalism for conceptual modelling of information transition systems. They defines the abstract unified conceptual model for the artifacts. The basic definitions of the theory of conceptual transition systems are given. A language of conceptual transition systems is defined.
Download
The relations of compatibility, consistency and identity are used to describe the semantics of the predicate programming language P. Recursive types are defined with the smallest fixed point. A generic type is described by a set of constraints. For expressions of duck type, the rules to define variable types are introduced. Algorithms for checking of recursion correctness, for determining the language construct types, and for checking the semantic correctness of constructs are developed.
Download
The AVL-tree operators are usually presented in functional languages in compact and elegant stile. However functional programs for insertion and removal operators are ineffective. They implement the construction of new tree but not the modification of the source tree. The paper describes the predicate programs for two algorithms of insertions into an AVL-tree. The predicate program can be automatically transformed to effective imperative programs.
Download
A review of the works that form the theoretical foundations of computation on Sleptsov nets and represent peculiarities of the drawing, compilation and linking of programs in the Sleptsov nets language, as well as massively parallel computing memory architectures for implementation of Sleptsov net processors is presented. The Petri net runs exponentially slower and represents a special case of the Sleptsov net. A universal Sleptsov net containing 13 places and 26 transitions is considered, which is a prototype of the Sleptsov net processor. Examples of programs in the Sleptsov nets language for efficient multiplication, RSA encryption / decryption, calculation of a fuzzy logic function, and solution of the Laplace equation are shown. The advantages of computations on Sleptsov nets are: visual graphical language, preserving the natural parallelism of domain, fine granulation of parallel computations, formal methods for parallel programs verification, and fast massively parallel architectures that implement the computation model.
Download
In the predicate programming compiler, optimizing transformations of the list and tree operations are described. The set of rules for replacement of the original operation to its image in the target imperative language has been developed. The translated imperative program is as effective as if it would be written manually.
Download
The paper presents an approach to the ontology-controlled organization of the process of information extraction from texts of clinical trials protocols. Individual components of the knowledge model, such as semantic vocabulary, text genre model, clinical trials ontology, are considered. Typical situations to be extracted are described and exemplified.
Download
The article describes the structure of the ontology of specification patterns from the texts of technical documentation. This ontology combines patterns of known classifications of requirements with new patterns. The ontology allows the recording of Boolean pattern combinations of the following types: qualitative, real and branching time, with combined events, quantitative characteristics of events and patterns, and simple statements about the data. Examples of the requirement patterns for the real vacuum control system of the Large Solar Vacuum Telescope are given. The scheme of intellectual support system for formal verification of distributed program systems is outlined.
Download
In the paper the notion of the conceptual model of a programming language is proposed. This formalism represents types of the programming language, values, exceptions, states and executable constructs of the abstract machine of the language, and the constraints for these entities at the conceptual level. The new definition of conceptual transition systems oriented to specification of conceptual models of programming languages is presented, the language of redefined conceptual transition systems CTSL is described, and the technique of the use of CTSL as a domain-specific language of specification of conceptual models of programming languages is proposed. The conceptual models for the family of sample programming languages illustrate this technique.
Download
In the paper the notion of the conceptual operational semantics of a programming language is proposed. This formalism represents operational semantics of a programming language in terms of its conceptual model based on conceptual transition systems. The special kind of conceptual transition systems, operational conceptual transition systems, oriented to specification of conceptual operational semantics of programming languages is defined, the extension of the language of conceptual transition systems CTSL for operational conceptual transition systems is described, and the technique of the use of the extended CTSL as a domain-specific language of specification of conceptual operational semantics of programming languages is proposed. The conceptual operational semantics for the family of sample programming languages illustrate this technique.
Download
The paper is devoted to studying the (‘gedanken’) experiments with input/output automata. We propose how to derive proper input sequences for identifying the final (current) state of the machine under experiment, namely synchronizing and homing sequences. The machine is non-initialized and its alphabet of actions is divided into disjoint sets of inputs and outputs. In this paper, we consider a specific class of such machines for which at each state the transitions only under inputs or under outputs are defined, and the machine transition diagram does not contain cycles labeled by outputs, i.e. the language of the machine does not contain traces with infinite postfix of outputs. Moreover, for each state where the transitions under inputs are defined, the machine has a loop under a special quiescence output. For such class of input/output automata, we define the preset synchronizing and homing experiments, establish necessary and sufficient conditions for their existence and propose techniques for their derivation. The procedures for deriving the corresponding (‘gedanken’) experiments for input/output automata are based on the well-studied solutions to these problems for Finite State Machines.
Download
The paper concerns recent advances in reaching the goal of industrial operating system (OS) verification. By industrial OS we mean a system actively used in some industrial domain, elaborated and maintained for a significant time, not a proof-of-concept OS developed with mostly research intentions. We consider decomposition of this goal into tasks related with various functional components of OS and various properties under verification, and application of different verification methods to those tasks. This is a trial to explicate and summarize the experience of several projects on various OS components and different OS features verification conducted in ISP RAS.
Download
Store-and-forward buffering of packets is traditionally used in modern network devices such as switches and routers. But sometimes it is a significant obstacle to the quality of service improvement because the minimal packet delivery time is limited by the multiplier of the number of intermediate nodes by the packet transmission time in the channel. The cut-through transmission of packets removes this limitation, because it uses only the head of packet, which contains the destination address, for the forwarding decision. Thus, the cut-through technology of packets transmission has considerable opportunities for the quality of service improving. Models for the computing grid with the cut-through forwarding have been developed in the form of colored Petri nets. The model is composed of packet switching nodes and generators of traffic; it can be supplied with malefactor models in the form of traffic guns disguised under regular multimedia traffic. The present work is the further development of methods of the rectangular communication grids analysis for nodes performing the cut-through switching. The methods are intended for application in the design of computing grids, in the development of new telecommunications devices, and in intelligent defense systems. Preliminary estimations show that the cut-through technology inherits some of the negative effects, which are associated with the traditional store-and-forward delivery of packets. A series of simulations revealed conditions of blocking a grid with its regular traffic. The results are applicable in the intellectual detection of intrusions and counter-measures planning.
Download
The paper covers design and developing software for hardware plant for water purification, the architecture for it, received automaton diagrams of water preparing and normalization based on customer specifications and requirements. Discussing the components of the system, layers of abstractions, verification points, issues to build it. The way of developing well-qualified suchlike systems based on specifications is given.
Download
Null pointer dereferencing remains one of the major issues in modern object-oriented languages. An obvious addition of keywords to distinguish between never null and possibly null references appears to be insufficient during object initialization when some fields declared as never null may be temporary null before the initialization completes. The proposed solution avoids explicit encoding of these intermediate states in program texts in favor of statically checked validity rules that do not depend on special conditionally non-null types. Object initialization examples suggested earlier are reviewed and new ones are presented to compare applicability of different approaches. Usability of the proposed scheme is assessed on open-source libraries with a million lines of code that were converted to satisfy the rules.
Download
This work represents the further development of the method for definite iteration verification. It extends the mixed axiomatic semantics method suggested for C-light program verification. This extension includes a verification method for definite iteration over unchangeable arrays with a loop exit in C-light programs. The method includes an inference rule for the iteration without invariants, which uses a special function that expresses loop body. This rule was implemented in verification conditions generator, which is the part of our C-light verification system. To prove generated verification conditions an induction is applied which is a challenge for SMT-solvers. At proof stage the SMT-solver Z3 is used in our verification system. To overcome mentioned difficulty a rewriting strategy for verification conditions is suggested. It allows to verify the definite iteration automatically using Z3. Also the paper describes the application of the theorem prover PVS for automatic proving of such verification conditions. An example, which illustrates the application of these methods, is considered.
Download
The purpose of the study is to demonstrate the feasibility of automated code migration to a new set of programming libraries. Code migration is a common task in modern software projects. For example, it may arise when a project should be ported to a new library or to a new platform. The developed method and tool are based on the previously created by the authors formalism for describing libraries semantics. The formalism specifies a library behavior using a system of extended finite state machines (EFSM). The mentioned EFSMs are a foundation of the code migration method. This paper outlines the metamodel designed to specify library descriptions and proposes easy to use domain-specific language (DSL), which can be used to define models for particular libraries. The mentioned metamodel directly forms the code migration method which is also described in the paper. A process of migration splits into five steps, and for each step the algorithm was developed. Models and algorithms were implemented in the prototype of an automated code migration tool. The prototype was tested on both artificial code examples and several real-world open source projects. Results of the experiment indicate that code migration can be successfully automated with developed tool acting as the proof of concept. Models and methods designed form a basis for more powerful migration methods and full-featured automated code migration tools.
Download
Static verification of source code correctness is a major milestone towards software reliability. The dynamic type system of the Jolie programming language, at the moment, allows avoidable run-time errors. A static type system for the language has been exhaustively and formally defined on paper, but still lacks an implementation. In this paper, we describe our steps toward a prototypical implementation of a static type checker for Jolie, which employs a technique based on a SMT solver.
Download
In recent years, both scientific and commercial organizations have generated a significant amount of structured data. On the basis of this data, numerous applications are being developed, which makes it necessary for modern IT specialists to get acquainted with this trend. This paper discusses the important aspects of the Semantic Web evolution and the experience of teaching the methods and tools of the Semantic Web.
Download
The following optimizing transformations: variable gluing, replacement of the tail recursion by a loop, in-line substitution, reduction - are described. Effective imperative program is the result of transformation application. Dataflow analysis of a program is applied to perform transformations.
Download
The article presents the results of the 4th International Conference “The development of computer technology in Russia and in the former USSR: history and prospects” (SoRuCom-2017) Zelenograd, Moscow, 3-5 October 2017. Our Institute was among the most active organizers of the Conference. The conference was supported by the Russian Foundation for Basic Research, Grant 17-07-20538, Computer History Museum (USA, CA), and Russian citizen Vladimir Kurlyandchik.
Download
This work presents a logical-probabilistic method for adaptive control of modular systems based on the use of the modules functional similarity and the logical-probabilistic algorithm of the guided search of rules. The proposed method is based on the joint learning of the control modules, starting with finding the common control rules for all modules and finishing with their subsequent specification in accordance with the ideas of the probabilistic inference. With an interactive 3D simulator, a number of successful experiments were carried out to train four virtual models of robots. Experimental studies have shown that the proposed approach is quite effective and can be used to manage modular systems with many degrees of freedom.
Download
This paper presents a method of information retrieval based on the ontology of scientific activity. This method makes use of general-purpose search engines to retrieve links to relevant Internet resources using the search queries generated on the basis of the ontology concepts and thesaurus. Search results that do not contain information about scientific activity are filtered using ontology.
Download
The article considers the twenty-year history and experience of creating automated systems for testing knowledge and skills in programming at the Novosibirsk State University. An analysis of the effectiveness or ineffectiveness of methods and means in the knowledge testing systems in use is given. The modern state of the architecture of the NSUts system is described.