RUS  ENG
Full version
JOURNALS // Modelirovanie i Analiz Informatsionnykh Sistem // Archive

Model. Anal. Inform. Sist., 2018 Volume 25, Number 5, Pages 481–490 (Mi mais643)

Program Verification

On methods in the verification and elaboration of development programs for agricultural territories

J. Vega Vice, V. Yu. Mikhailov

Kazan (Volga region) Federal University, 18 Kremlyovskaya str., Kazan 420008, Russia

Abstract: Nowadays, the methods of program-targeted management for the development of various socio-economic systems of complex structure, such as agricultural areas, have become universal. Therefore, the current tasks at hand are the verification of already created development programs and the development of "proper" programs for the development of such systems, by analogy with the verification and development of proper computer programs through developed disciplines in theoretical programming. In this paper, in order to solve the problem of verification of development programs for agricultural territories, a structural scheme of the program is first constructed, through which the axiomatic theory is created, using Hoare's algorithmic logic system. The main problem in the construction of the axiomatic theory is the development of the axioms of the theory reflecting the preconditions and effects of the implementation of meaningful actions indicated in the text of the development program. The verification of the development program corresponds to the probability of some Hoare triplet, according to the initial and target conditions of the program. For the task of elaboration of the right development programs, the mechanism for constructing a domain model using the PDDL family description languages is described. The description of a specific model is purely declarative in nature and consists of descriptions of predicates and actions of the chosen subject area. In this paper, it is shown how on the described model with the help of intelligent planners, including temporal planners such as OPTIC, solutions to the targets of development programs can be automatically built. Based on expert knowledge and activity standards, a model of an agricultural territory is constructed, a brief description of which is given in the work. The conducted experiments showed the effectiveness of the proposed approach for the development of proper development programs.

Keywords: development programs, verification of development programs, development of proper development programs, Hoare's logic, PDDL language, intelligent planners, model of agricultural territories.

UDC: 517.9

Received: 20.07.2018

DOI: 10.18255/1818-1015-481-490



© Steklov Math. Inst. of RAS, 2024