Verification-Oriented Process Ontology

Аннотация

This paper presents the ontology of the concurrent processes close to Hoare communicating sequential processes. It is a part of an intellectual system for supporting verification of behavioral properties of such processes. Our ontological representation of the processes is oriented both to the application of formal verification methods and to the extraction of information from technical documentation (by our previously developed system of information extraction from a natural language text). We describe the ontology classes and domains that define communicating concurrent processes. These processes are characterized by sets of local and shared variables, a list of actions on these variables which change their values, a list of channels for the process communication (which, in turn, are characterized by the type of reading messages, capacity, modes of writing and reading, and reliability), and also a list of communication actions for sending messages. In addition to the formal mathematical definition of classes and domains of the ontology, examples of descriptions of some ontological classes, as well as typical properties and axioms for them, are specified in the editor Protégé in the OWL language with the use of the inference rules in the SWRL language. We define the formal operational semantics of communicating processes for their ontological representation. This semantics is a labeled transition system. It is reduced to the local operational semantics of separate process instances in the interleaving model. We specialize several types of processes from the subject domain of automatic control systems that model the typical functional elements of the automatic control system (sensors, comparators and regulators), as well as their combinations. The concepts of the specialized ontology are illustrated by the example of a control part of a bottle-filling system.