Computer Science, № 26, 2007

A new class of transition systems, ontological transition systems is presented. They enrich transition systems with ontological entities. In the framework of development of a language of ontological transition systems OTSL, a sublanguage of formulas is defined. Formulas are used to specify ontological entities of ontological transition systems.

Ontological transition systems are a method of specification of computer systems which integrates operational and ontological approaches to specification of these systems. In the framework of development of a language of ontological transition systems OTSL, a sublanguage of actions is defined. Actions are used to specify transitions in ontological transition...

We address a problem of efficiency of verification condition generation for unstructured non-deterministic imperative programs. Importance of the study is based upon two arguments:

• industrial programming is very often unstructural (e.g., extensive use of “go to” in C-programs);
• program analysis techniques (like abstraction) introduce unstructural and non-deterministic control flow to...

The paper describes an approach to visualization of solution spaces in computer modeling problems. The advantage of the approach is that it is applicable to visualization of solution spaces of arbitrary spatial structure (e.g. consisting of multiple components, containing cuts, accumulation points, etc.) An implementation of the approach is built...

It is well known that parameterization is a powerful tool for creation and reuse of models. It allows us to construct models with predefined features, as well as to form new models by modification of parameters of already existing models. These opportunities are crucial for engineers and other CAD users...

The transitive closure (or reachability) problem in a directed graph consists in finding whether there is a path between any two vertices. In this paper, we first study the problem of parallelization of Italiano's algorithm for dynamic updating the transitive closure after inserting a new arc into the graph represented...

This paper introduces the notion of decomposability in an extension and relative decomposability for first-order theories. We describe several basic facts connected with these notions and formulate a criterion of relative decomposability.

The evolution of formal methods allowed us to overcome many obstacles in verification of procedural programs. However, wide spreading of object-oriented languages has brought new challenges, even in the case of sequential programs. These problems were thoroughly examined by ESC/Java and Spec# teams in their papers [10, 12], though in...

The paper presents an approach to document analysis adaptable to a certain genre of the document and subject domain. The approach is intended for updating a database of an information system by means of information obtained by automated analysis of electronic documents. This approach implies using linguistic knowledge about the...

Methods for analysis of texts and separate sentences in a natural language are under discussion. Their main application is to study a written speech with the help of mathematical logic, syntactic rules and the morphology of the modern Russian literary language. Various algorithms for matching predicates and formulas of first...