An approach to construction and verification of PLC-programs for discrete tasks is proposed. For the specification of a program behavior we use the linear-time temporal logic LTL. Programming is carried out in the ST-language according to an LTL-specification. The correctness analysis of an LTL-specification is carried out by the symbolic model checking tool Cadence SMV. A new approach to programming and verification of PLCprograms is shown by an example. For a discrete problem we give a ST-program, its LTL-specification and an SMV-model.

A purpose of the article is to describe an approach to programming PLC, which would provide a possibility of PLC-program correctness analysis by the model checking method.

Under the proposed approach the change of the value of each program variable is described by a pair of LTL-formulas. The first LTL-formula describes situations that increase the value of the corresponding variable, the second LTL-formula specifies conditions leading to a decrease of the variable value. The LTL-formulas (used for specification of the corresponding variable behavior) are constructive in the sense that they construct the PLC-program, which satisfies temporal properties expressed by these formulas. Thus, the programming of PLC is reduced to the construction of LTL-specification of the behavior of each program variable. In addition, an SMV-model of a PLC-program is constructed according to LTL-specification. Then, the SMV-model is analysed by the symbolic model checking tool Cadence SMV.

In this work, we consider the modeling of workflow systems with Petri nets. A resource workflow net (RWF-net) is a workflow net supplied with an additional set of initially marked resource places. Resources can be consumed and/or produced by transitions. We constrain neither the intermediate nor final resource markings, hence a net can have an infinite number of different reachable states. An initially marked RWF-net is called sound if it properly terminates its work and, moreover, an increase of the initial resource does not violate its proper termination. An unmarked RWF-net is sound if it is sound for some initial resource. In this paper, we prove the decidability of both marked and unmarked soundness for a restricted class of RWF-nets with a single unbounded resource place (1-dim RWF-nets). We present an algorithm for computing the minimal sound resource for a given sound 1-dim RWF-net.

The paper considers automation problems of the interface formation between a table and a relational database. The task description is formalized and the description of the existing approaches to formation of data representations on an example of widely widespread CASE-tools is submitted. The definition of intermediate data representation as a ”join table” is offered, which is used for maintenance of correctness of data representation formation, and also is necessary for direct and inverse data transformations. On the basis of lossless join property and realized dependencies, the concept and a way of context formation of the application and restrictions is introduced. The considered material is further used for constructing an inverse data transformation from tabular presentation into a relational one. On the basis of relationships properties on a database scheme, the partial order on the relations is established, and the restriction of acyclic databases schemes is introduced. The received results are further used at the analysis of principles of formation of inverse data transformation, and the basic details of such a transformation algorithm are considered.

The paper presents an (n, t)-threshold proxy signature scheme with an Arbitrator which enables an original signer to delegate the signature authority to sign a message on behalf of the original signer to proxy group P of n members. The original signer distributes the proxy key among the proxy group members in such a way that not less then t proxy signers and the Arbitrator can cooperatively sign messages on behalf of the original signer. Thus, for signing the document it is necessary to have agreements of not less then t members. The Arbitrator is a trusted third party. It receives the information from the t members and completes the calculation of the digital signature. A verifier can identify the original signer and the members of the proxy group P. The main feature is that n members of the proxy group can not calculate the proxy key and the original signer’s secret key.

In 1929 B.N. Delaunay obtained the complete classification of all possible combinatorial coincidence types of parallelohedra at their faces of codimension 3. It appeared that every such coincidence is dual to one of the following five three-dimensional polytopes: a tetrahedron, a quadrangular pyramid, an octahedron, a triangular prism, or a parallelepiped. The present paper contains a new combinatorial proof of this result based on Euler formula. Using the classification, we have obtained several further properties of faces of codimension 3 in parallelohedral tilings. For instance, we showed that the Dimension Conjecture holds for faces of codimension 3, i.e. if we take the affine hull of centers of all parallelohedra containing a particular face of codimension 3, this affine hull is three-dimensional. Finally, we proved that the set of centers of all parallelohedra sharing a face of codimension 3 spans a three-dimensional sublattice of index one.

The paper presents an agent substitution algorithm for a dataflow network implemented on the Smart-M3 platform. Such a substitution allows to transfer control and computational context from an unexpectedly disconnected agent to a programmable substitute agent for the period of absence of the first agent in the network. It also guarantees integrity of the information flow, i.e. the functioning of all dependent services is not disrupted after the agent disconnection. When the agent returns to the network the reverse substitution occurs also with keeping integrity of the information flow. The paper gives a description of the dataflow network implementation and substitution mechanism structure on the Smart-M3 platform. The detailed description of the substitution algorithm including initialization, registration, and bidirectional substitution phases is given. The proposed substitution algorithm was implemented by the authors in the substitution mechanism as a part of the RedSIB semantic information broker on the Smart-M3 platform.

In this paper, we propose a novel approach to many-to-many user authentication in heterogeneous information systems. The described solution is based on the use of wireless keys – special devices that identify the user by transmitting the requested key information over a wireless network. The key feature of the proposed approach is noninteractive operating mode that allows to use a special encryption algorithm instead of two-way authentication. The algorithm is built on the basis of existing cryptographic primitives that prevents unauthorized system participants from getting access to the data of other users, even with physical access to the memory of the key. This approach does not require computational power or the battery on the key side and does not involve the user in the authentication process that allows implementing a method on passive NFC tags. To proof the concept, software implementation of the described system was developed and a qualitative comparison of the resulting solutions with existing analogues was conducted.

The objects of this study were the properties of time-bound electromagnetic waves (wave packets) from rotating in space vectors of polarization with a constant angular velocity. It is shown that the formal condition of function orthogonality on some interval of their argument, which is an integrated energy characteristics of their mutual influence, can be extended to a system of time-wave packets with the specified polarization characteristics. It is designed an adjustable threshold criterion level, which defines the boundaries of signals orthogonality in a two-dimensional space of frequency-difference parameters. It has been demonstrated that with an increase in the duration of these packages there is a tendency to extend the set of frequency parameters that satisfy the criteria specified level of orthogonality.

The authors of the article focus on the concept of a software defined network. In the beginning, the brief historical account is given concerning software defined networks as a scientific concept, its formation and technological and scientific meaning. The software defined network concept is treated in the article not as the final state-of-the-art in networking, but rather as a possible step and direction in the development of a networking paradigm. The article touches on pros and cons as well of the software defined networking and gives an account of possible stages of development of this technology in the context of other technologies, considering its hybrid with MPLS, as an example. OpenFlow protocol constitutes the main part of the article. The authors further discuss various kinds of existing libraries realizing programmable management routines for a software defined network using OpenFlow. All of these libraries provide API for building modular applications for software defined network management. Touching on practical side of implementation the results of comparative tests of throughput and latency, achieved with these libraries are shown.

This paper reports basic approaches to constructive creation of an open resource named ”Domain-specified thesaurus of poetics”, which is one of the levels of an information-analytical system of the Russian poetry (IAS RP). The poetics is a group of disciplines focused on a comprehensive theoretical and historical study of poetry. IAS RP will be used as a tool for a wide range of studies allowing to determine the characteristic features of the analyzed works of poetry. Consequently, the thesaurus is the knowledge base from which one can borrow input data for training the system. The aim of our research requires a specific approach to formating the knowledge base. Thesaurus is a web-based resource which includes a domain-specific directory, information retrieval tools and tools for further analyzes. The study of glossary consisting of three thousand terms and a set of semantic fields is reviewed in this paper. Rdf-graph of the domain-specified thesaurus of poetics is presented, containing 9 types of objects and different kinds of relationships among them. Wiki-tecnologies are used for implementing a resource which allows to store data in Semantic Web formats.

One of the main trends of recent years in software design is a shift to a Software as a Service (SaaS) paradigm which brings a number of advantages for both software developers and end users. However, along with these benefits this transition brings new architectural challenges. One of such challenges is the implementation of a data storage that would meet the needs of a service-provider, at the same time providing a fairly simple application programming interface for software developers. In order to develop effective solutions in this area, the architectural features of cloud-based applications should be taken into account. Among others, such key features are the need for scalability and quick adaptation to changing conditions. This paper provides a brief analysis of the problems in the field of cloud data storage systems based on the relational model and it proposes the concept of database cluster designed for applications with a multi-tenant architecture. Besides, the article describes a simulation model of such a cluster, as well as the main stages of its development and the main principles forming its foundation.