Preview

Modeling and Analysis of Information Systems

Advanced search
Vol 21, No 2 (2014)

Articles

5-14 852
Abstract
The article suggests the method of anti-virus protection of mobile devices based on the usage of proxy digital signatures and an (n;t)-threshold proxy signature scheme with an arbitrator. The unique feature of the suggested method is in the absence of necessity to install anti-virus software in a mobile device. It will be enough only to have the software verifying digital signatures and the Internet. The method is used on the base of public keys infrastructure /PKI/, thus minimizing implementation expenses.
15-25 860
Abstract
The paper describes software components to support recursive-parallel programming for the .NET Framework. They are dynamic link libraries providing the necessary functionality for developing and debugging applications for parallel execution on a local network. Communication module library classes provide user-friendly software tools to establish ”each with each” network connection and reliable asynchronous transmission for serializable objects. Classes of the recursive-parallel programming library provide representation of parallel computation branches as migratory processes, their initial distribution over the network, the transmission parameters and return results with the necessary synchronization, dynamic reallocation of work for load balancing and also sharing data processing. By this example it also describes some variants of the recursive-parallel algorithm to solve the problem of finding a maximum clique in a non-oriented graph and the results of testing the considered components.
26-38 1145
Abstract

An approach to the construction and verification of PLC IL-programs for discrete problems is proposed. For the specification of the program behavior, we use the linear-time temporal logic LTL. Programming is carried out in the IL-language (Instruction List) 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 PLC IL-programs is shown by an example. For a discrete problem, we give an IL-program and its LTL-specification.

The purpose of the article is to describe an approach to programming PLC, which would provide a possibility of IL-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 which 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 speci- fication of the corresponding variable behavior) are constructive in the sense that they construct the PLC-program (IL-program), which satisfies temporal properties expressed by these formulas. Thus, the programming of PLC is reduced to the construction of LTLspecification of the behavior of each program variable. In addition, an SMV-model of a PLC IL-program is constructed according to LTL-specification. Then, the SMV-model is analysed by the symbolic model checking tool Cadence SMV.

50-55 945
Abstract
The generalization of one classical Seksenbaev theorem for polycyclic groups is obtained. Seksenbaev proved that if G is a polycyclic group which is residually finite p-group for infinitely many primes p, it is nilpotent. Recall that a group G is said to be a residually finite p-group if for every nonidentity element a of G there exists a homomorphism of the group G onto a finite p-group such that the image of the element a differs from 1. One of the generalizations of the notation of a polycyclic group is the notation of a finite rank group. Recall that a group G is said to be a group of finite rank if there exists a positive integer r such that every finitely generated subgroup in G is generated by at most r elements. We prove the following generalization of Seksenbaev theorem: if G is a group of finite rank which is a residually finite p-group for infinitely many primes p, it is nilpotent. Moreover, we prove that if for every set π of almost all primes the group G of finite rank is a residually finite nilpotent π-group, it is nilpotent. For nilpotent groups of finite rank the necessary and sufficient condition to be a residually finite π-group is obtained, where π is a set of primes.
56-70 773
Abstract

Algebraic program models with procedures are designed to analyze program semantic properties on their models called program schemes. Liberisation and equivalence problems are stated for program models with procedures. A subclass of program models with procedures called special gateway models is investigated. A better complexity algorithm for the liberisation in such models is proposed. Primitive program schemes are defined as a subclass of special gateway models. It is shown that the equivalence problem in such models is decidable if the equivalence problem is decidable in special program models without procedures. For some cases of decidability the complexity is evaluated.

71-89 884
Abstract

A modification of the well-known FitzHugh–Nagumo model from neuroscience is proposed. This model is a singularly perturbed system of ordinary differential equations with a fast variable and a slow one. The existence and stability of a nonclassical relaxation cycle in this system are studied. The slow component of the cycle is asymptotically close to a discontinuous function, while the fast component is a δ-like function. A onedimensional circle of unidirectionally coupled neurons is considered. It is shown the existence of an arbitrarily large number of traveling waves for this chain. In order to illustrate the increasing of the number of stable traveling waves numerical methods were involved.

90-96 795
Abstract
We prove the reducibility of the moduli space Mref(2; −1, 4, 2) of stable rank 2 re- flexive sheaves with Chern classes c₁ = −1, c₂ = 4, c₃ = 2 on projective space P³. This gives the first example of a reducible space in the series of moduli spaces of stable rank 2 reflexive sheaves with Chern classes c₁= −1, c₂ = 4, c₃ = 2m, m = 1, 2, 3, 4, 5, 6, 8. We find two components of the expected dimension 27 of this space and give their geometric description via the Serre construction.


Creative Commons License
This work is licensed under a Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)