Preview

Modeling and Analysis of Information Systems

Advanced search
Vol 14, No 1 (2007)

Articles

3-10 407
Abstract
It is proved that the minimal norm On of a projection in linear interpolation on the n-dimensional cube On = [0,1]n satisfies the condition On = 0(n1/2), n G N. With the previous results of the author it means that On ~ n1/2. The upper estimates are provided by the projection with knots of interpolation in vertices of а largest simplex in On.
11-18 434
Abstract
This article presents a model of automaton program that satisfies synchronous model requirements. A formal automaton program model lets to use an existing technologies and tools of synchronous programs verification for checking automaton programs. An Esterel language and an Esterel Technologies Inc. toolbox will be used to build a program verifier.
27-30 428
Abstract
We prove exact relations between K-functionals of pairs (C,Cl) and best uniform piecewice polynomial approximations of functions from C.
31-43 484
Abstract
In the paper one of approaches to modelling, specification and verification of automaton programs are considered. The automata programming technology is effective enough in design and verification (the analysis of correctness) software for reactive and controlling systems. This technology, besides other methods of software construction "without errors", is much more constructive, as it allows to begin "struggling against errors" at the algorithmization stage. However, in spite of the fact that the idea of automata programming is directed on the construction of reliable programs, the problem of the program correctness analysis still remains actual.
From the point of view of modelling and analysing program systems the automata approach to programming has a number of advantages in comparison with the traditional approach. When constructing a model for a program written in the traditional style, there is a serious problem of the adequacy of this program model to the initial program. The model can be unable to take into account a number of program properties or can generate nonexisting properties. Under the automata programming such a problem is excluded, as a collection of communicating automata, describing the logic of the program, is already an adequate program model. This fact is an indisputable advantage of the automata technology. Moreover, the model has a finite set of states, that is, in practice, a necessary condition for successful automatic verification by the model checking method. Besides, properties of automata programs are naturally and clearly formulated and specified. These properties obviously correspond with communicating automata representing the logic of an automata program.
The practical result of the work is an application of the tool SPIN and the temporal logic LTL for specification and verification of hierarchical automaton programs.
44-47 469
Abstract
In the paper is formulated series of functions in a set of pairs of black-and-white digital images. Series of functions are either distance or distance analogue. This functions allows, on the one hand, to solve a problem of discerning images, and on the other hand, to measure similarity. Applications of this approach to textures are examined.
48-53 395
Abstract
Construction principles of service - oriented architecture as a means of achieving adaptability and flexibility of distributed information system's infrastructure are suggested. Different variants of constructing of this architecture, it's main elements, their interoperability, methods of working with them are considered. The suggested architecture is based on the definition of the semantic service-oriented architecture style and provides semantic means of distributed components interaction thus providing new level of decision of information systems integration problem.
54-56 456
Abstract
A automorphism of transitions system is an isomorphism of a system oneself. In the article are showed, that every finite group may be embedded in a group of automorphisms of a certain transition system.


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