Полиномиально вычислимые -спецификации иерархизированных моделей реагирующих систем
Автор: Глушкова В. Н., Коровина К. С.
Журнал: Вестник Донского государственного технического университета @vestnik-donstu
Рубрика: Информатика, вычислительная техника и управление
Статья в выпуске: 4 т.20, 2020 года.
Бесплатный доступ
Введение. Пакеты верификации проектируют и анализируют корректность параллельных и распределенных систем в рамках различных классов темпоральных логик линейного и ветвящегося времени. В статье рассматривается полиномиально реализуемый класс ∆0T-формул, интерпретируемый на многосортных моделях с иерархическими надстройками. Структура надстройки описывается произвольной контекстно-свободной (КС) грамматикой. Предикаты и функции сигнатуры модели интерпретируются на исходном КС-списке, достраиваемом в процессе интерпретации.Материалы и методы. Для теорий из ∆0T-квазитождеств, обладающих свойствами нётеровости и конфлюент-ности, строится константная модель. Рассматриваются формулы многосортного языка исчисления предикатов (ИП) 1-го порядка с переменными сорта «список», интерпретируемые на моделях с иерархизированной надстройкой. Теория интерпретируется на деревьях вывода грамматики, описывающих поведение специфицируемой системы. Правила КС-грамматики иерархизируют пространство действий моделируемой системы. Отмечено, что для моделирования систем реального времени недостаточно выразительных возможностей Д0 T-формул. Поэтому для спецификации используются выражения с неограниченным квантором всеобщности V, известные как ПТ-формулы.Результаты исследования. В качестве примера приводится логическая спецификация автоматизированного комплекса, который состоит из манипулятора, обрабатывающего детали. Положение позиций фиксируется датчиками. Описывается цикл работы манипулятора. Спецификация его функционирования состоит в иерархиза-ции действий правилами КС-грамматики и их описании формулами ИП 1-го порядка с учетом значений времени.Обсуждение и заключения. В статье показано, что класс рассмотренных формул можно использовать для моделирования систем реального времени. Приводится пример логической спецификации управляющего устройства поведением манипулятора.
Логическая спецификация, модель теории, реагирующая система, кс-грамматика, формула ип 1-го порядка
Короткий адрес: https://sciup.org/142225519
IDR: 142225519 | DOI: 10.23947/2687-1653-2020-20-4-422-429
Список литературы Полиномиально вычислимые -спецификации иерархизированных моделей реагирующих систем
- Goguen, J. A. Models and equality for logical programming / J. A. Goguen, J. Meseguer // Lecture Notes in Computer Science. - 1987. - Vol. 250. - P. 1-22.
- Kowalski, R. Logic for Problem Solving, Revisited / R. Kowalski. London: Imperial College, 2014. - P. 321.
- Кларк, Э. М. Верификация моделей программ / Э. М. Кларк, О. Грамберг мл., Д. Пелед // Москва: Изд-во Московского центра непрерывного математического образования, 2002. - 416 с.
- Reps, T. Automating Abstract Interpretation / T. Reps, A. Thakur // In: 17th International Conference, VMCAI 2016, on Verification, Model Checking and Abstract Interpretation. St. Petersburg, FL, USA, January 17-19, 2016. - Paris: Springer, 2016. - P. 3-40.
- Bloem, R. SAT-Based Synthesis Methods for Safety Specs / R. Bloem, R. Konighofer, M. Seidl // In: 15th International Conference, VMCAI 2014, on Verification, Model Checking and Abstract Interpretation. San Diego, CA, USA, January 2014. - San Diego: Springer, 2014. - P. 1-20.
- Beyer, D. Reuse of Verification Results / D. Beyer, Ph. Wendler // In: 20th International Symposium, SPIN 2013, on Model Checking Software. Stony Brook, July 8-9, 2013. - Stony Brook: Springer, 2013. - P. 1-15.
- Alur, R. Model-cheking for real-time system / R. Alur, C. Courcoubetis, D. L. Dill // Information and Computation. - 1993. - Vol. 104 (1). - P. 2-34.
- Morbe, G. Fully Symbolic TCTL Model Checking for Incomplete Timed Systems // G. Morbe, Ch. Scholl // In: Proceedings of the Automated Verification of Critical Systems (AVoCS 2013). - 2013. - Vol. 66. - P. 1-9.
- D'Silva, V. Independence Abstractions and Models of Concurrency / V. D'Silva, D. Kroening, M. Sousa // In: 18th International Conference, VMCAI 2017, on Verification, Model Checking and Abstract Interpretation. Paris, France, January 15-17, 2017. - Paris: Springer, 2017. - P. 149-168.
- Goncharov, S. S. Theoretical aspects of S-programming / S. S. Goncharov, D. I. Sviridenko //: In: Proc. of the International Spring School, April 1985, on Mathematical Methods of Specification and Synthesis of Software Systems' 85. Berlin; Heidelberg: Springer-Verlag, 1985. - P. 169-179.
- Гончаров, С. С. Модели данных и языки их описаний / С. С. Гончаров // Вычислительные системы. Логико-математические основы проблемы МОЗ. - 1985. - Вып. 107. - С. 52-70.
- Мальцев, А. И. Алгебраические системы. Москва: Наука, 1976. - С. 392.
- Глушкова, В. Н. Оценка сложности реализации логических спецификаций на основе контекстносвободных грамматик / В. Н. Глушкова // Кибернетика и системный анализ. - 1996. - № 4. - С. 50-58.
- Горбатов, В. А. Логическое управление распределенными системами / В. А. Горбатов, М. И. Смирнов, И. С. Хлытчиев. - Москва: Энергоатомиздат, 1991. - 288 с.
