RUS  ENG
Полная версия
ЖУРНАЛЫ // Моделирование и анализ информационных систем // Архив

Модел. и анализ информ. систем, 2018, том 25, номер 5, страницы 481–490 (Mi mais643)

Верификация программ

О методах верификации и разработки программ развития сельскохозяйственных территорий

Х. Л. Вега Висе, В. Ю. Михайлов

Казанский (Приволжский) федеральный университет, ул. Кремлёвская, 18, г. Казань, 420008 Россия

Аннотация: В настоящее время повсеместными стали методы программно-целевого управления развитием различных социально-экономических систем сложной структуры, например, таких как территории сельскохозяйственного назначения. Поэтому актуальными задачами являются верификация уже созданных программ развития и разработка «правильных» программ развития таких систем, по аналогии с верификацией и разработкой правильных компьютерных программ — развитыми дисциплинами в теоретическом программировании. В данной работе для решения задачи верификации программ развития сельскохозяйственных территорий сначала строится структурная схема программы, по которой создается аксиоматическая теория, использующая аппарат алгоритмических логик Хоара. Основной проблемой при построении аксиоматической теории является разработка аксиом теории, отражающих предусловия и эффекты выполнения содержательных действий, указанных в тексте программы развития. Верификация программы развития соответствует проверке доказуемости некоторой тройки Хоара, соответствующей начальным и целевым условиям программы. Для задачи разработки правильных программ развития описывается механизм построения модели предметной области с использованием языков описания моделей семейства PDDL. Описание конкретной модели имеет чисто декларативный характер и представляет собой набор описаний предикатов и действий выбранной предметной области. Показывается, как на описанной модели с помощью интеллектуальных планировщиков, включая темпоральные планировщики типа OPTIC, автоматически строить решения целевых задач программ развития. На основе экспертных знаний и отраслевых стандартов построена модель сельскохозяйственной территории, краткое описание которой приводится в работе. Проведенные эксперименты показали эффективность предлагаемого подхода к разработке правильных программ развития.

Ключевые слова: программы развития, верификация программ развития, разработка правильных программ развития, логики Хоара, язык PDDL, интеллектуальные планировщики, модель сельскохозяйственной территории.

УДК: 517.9

Поступила в редакцию: 20.07.2018

DOI: 10.18255/1818-1015-481-490



© МИАН, 2024