Preprints of IIS SB RAS, 2010

Preprint 159
Yu.G. Platonov
Requirements for an EDM system for enterprises with high level of the responsibility for the final product and analysis of the possibility of use of modern information systems for that purpose

The author of the article considers the problem of the development of the information system ‘Documents Circulation’ as a subsystem of an information complex implemented for enterprises with high level of responsibility for the final product. The subsystem must provide high functionality and high level of data security, therefore it is of interest for the researcher. The author has taken the JSC Information Satellite Systems – Reshetnev Company (Zheleznogorsk), an enterprise involved in design and manufacture of navigation and geodetic satellites, as an example of such an enterprise.

The author describes the requirements for the ‘Documents Circulation’ subsystem, analyzes some modern software products and the possibility of their use as the subsystem (entirely or partially after integration with other products) and draws a conclusion of the necessity of research in order to implement the original program product.

Preprint 158
I.S. Anureev
The Atoment language: standard library

The Atoment language is a domain-specific language of development of program verification methods. It is used in the multilanguage software\linebreak system Spectrum of rapid development and testing of verification methods. The easy-to-use specialized language allows a user of the system to describe verification methods in natural notation, verify algorithms for different object domains, adding new languages for their representations as necessary, share verification methods with other users and combine them. In this paper the standard library of the Atoment language is described. It is presented by a set of execution schemes. Semantics of these schemes is defined. The schemes are illustrated by examples of their use.

Preprint 157
I.S. Anureev
The Atoment language: syntax and semantics

The Atoment language is a domain-specific language of development of program verification methods. It is used in the multilanguage software\linebreak system Spectrum of rapid development and testing of verification methods. The easy-to-use specialized language allows a user of the system to describe verification methods in natural notation, verify algorithms for different object domains, adding new languages for their representations as necessary, share verification methods with other users and combine them. In this paper the syntax and semantics of the Atoment language are described.

Preprint 156
V.A. Nepomniaschy, E.V. Bodin, S.O. Veretnov
Modeling and verification of distributed systems specified in the language SDL with the help of the language Dynamic-REAL

The present paper describes a program complex SRDSV (SDL/REAL Distributed Systems Verifier) for modeling, analysis and verification of SDL-specifications of distributed systems. This complex includes a translator from SDL language into the language Dynamic-REAL (dREAL), a tool for automatic modeling dREAL- specifications and two verifiers of these specifications by model-checking method. One of these verifiers uses the well-known tool SPIN. An application of the complex SRDSV to analysis and verification of a dynamic system for control of booking terminals net is described.

Preprint 155
I.V. Maryasov
Applying the mixed axiomatic semantics of C-kernel language to the verification of topological sorting program

A topological sorting program was verified by applying mixed modified axiomatic semantics of C-kernel language. This language is the kernel of C-light language.

Preprint 154
V.I. Shelekhov
Development of effective programs for the standard functions FLOOR, ISQRT, and ILOG2 under predicate programming technology

Development of effective programs for the standard functions under predicate programming technology is described. The developed functions are integer part of float value, integer square root, and integer part of binary logarithm.

Preprint 153
N. Karnaukhov, D. Perchine, V. Shelekhov
The predicate programming language P

The predicate programming language P is oriented on the development of reliable and efective programs for problems in discrete and calculus mathematics. In comparison with the initial version the language is essentially extended by the means for process descriptions, algebraic types, aggregates, formula description language, and another constructs. For the P language, the syntax, operator set, and other features are very similar to those for the C family languages.




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.