Preprints of IIS SB RAS, 2007

Preprint 148
Z.V. Apanovich
From graph drawing towards information visualization

Last years methods of Information Visualization are getting more and more popular in such areas as biological sciences, artificial intelligence, business analytics, etc. Information Visualization is a process of transformation of large and complex abstract forms of information into visual form, strengthening user's cognitive abilities and allowing them to take the most optimal decisions. Graphs and trees are widely used for abstract information representation. The aim of this paper is to show evolution of graph drawing methods with respect to Information Visualization needs.

Preprint 147
V.A. Nepomniaschy, E.V. Bodin, S.O. Veretnov
Distributed systems specification language Dynamic-REAL

The present paper describes a distributed systems specification language Dynamic-REAL (dREAL) which extends the language Basic-REAL developed previously by dynamic constructs for generating and removing process instances. The dREAL language includes sublanguages of executable and logic specifications. Syntax and formal semantics of the dREAL language are represented in this paper. As an example, a protocol for control of a booking terminals net is considered.

Preprint 146
E.G. Tumurov
The technology of specification of communication protocols

The work presents the technology of communication protocol specification. Several communication protocols are considered for the following aspects of communication: blocked or non-blocked receiving/sending, reliable or unreliable communication. This paper can be considered as an introduction to problems of communication protocols.

Some communication and data transfer patterns are described. The following communication protocol components are defined: nodes, channels, messages, input and output streams, events, timers, etc. Techniques of reliable transfer over unreliable channels such as retransmission, check summing, reception of acknowledgment, etc. are described. Additional properties of protocol specifications set are given. They are correctness, safety and liveness properties. They are usually expressed in some language of temporal logic.

Preprint 145
V.I. Shelekhov
The model of program correctness for the language of computable predicates

The calculus of computable predicates is a mathematical model of programs whose specification is a predicate. A program on the calculus language is the closed set of recursive definitions of predicates. The specification of each defined predicate consists of the precondition and postcondition. Program correctness definition is considered as the concretization of the general law of the correspondence between a program and its specification. Two rule systems of program correctness proof are introduced. In first rule system, the postcondition is proved from the right part of the predicate definition. In the second rule system, for single-valued predicates, the right part is derived from the precondition and postcondition.

Preprint 143
V.I. Shelekhov
The calculus of computable predicates

The calculus of computable predicates is defined by a collection of basic predicates and the following six computable formulas: superposition, alteration, parallel composition, predicate generation, predicate application, and array constructor. The collection of basic predicates defines a data type system. The calculus is a mathematical model of the class of programs whose specification may be written as a formula of the higher-order predicate calculus. The calculus of computable predicates may be used to construct pure functional programming languages.

Preprint 142
V.A. Nepomniaschy, E.V. Bodin, S.O. Veretnov, M.V. Tyuryushkin
Simulation and verification of static SDL specifications of distributed systems by help of the intermediate language REAL

The present paper describes system SRPV (SDL/REAL Protocol Verifier) for modelling, analysis and verification of static SDL-specifications of communication protocols. This system is based on translation of SDL language to Basic-REAL (bREAL) language. This system includes: translator from SDL language to bREAL language, converter from properties description language for SDLspecifications to logical specifications sublanguage of bREAL, modelling system for bREAL-specifications, and verification system for these specifications. As an illustrative example, an application of the SRPV system to analysis and verification of "Passenger and Slot-Machine" protocol is described.

You are reporting a typo in the following text:
Simply click the "Send typo report" button to complete the report. You can also include a comment.