Ontological transition systems
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.
A language of actions in 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...
Effective generation of verification conditions for non-deterministic unstructured programs
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...
Correct visualization of solution spaces in the UniCalc system
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...
Spanning-tree modeling method for geometric constraint satisfaction problem
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...
Associative version of Italiano's incremental algorithm for dynamic updating the transitive closure
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...
Generalized decomposability notions for first-order theories
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 C#-light project: solution of some verification challenges
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...
Ontology-based approach to text analysis
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...
Logical analysis of texts in a natural language and a sense representation
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...