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.

anureev_1.pdf141.79 KB

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...

anureev_2.pdf154.84 KB

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...
anueev_rbodin_shilov.pdf242.46 KB

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...

promsky.pdf195.47 KB

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...

sidorova.pdf224.26 KB