Preview

Advanced Engineering Research

Расширенный поиск

Полиномиально вычислимые Σ-спецификации иерархизированных моделей реагирующих систем

https://doi.org/10.23947/2687-1653-2020-20-4-422-429

Полный текст:

Аннотация

Введение. Пакеты верификации проектируют и анализируют корректность параллельных и распределенных систем в рамках различных классов темпоральных логик линейного и ветвящегося времени. В статье рассматривается полиномиально реализуемый класс ∆0T-формул, интерпретируемый на многосортных моделях с иерархическими надстройками. Структура надстройки описывается произвольной контекстно-свободной (КС) грамматикой. Предикаты и функции сигнатуры модели интерпретируются на исходном КС-списке, достраиваемом в процессе интерпретации.

Материалы и методы. Для теорий из ∆0T-квазитождеств, обладающих свойствами нётеровости и конфлюент-ности, строится константная модель. Рассматриваются формулы многосортного языка исчисления предикатов (ИП) 1-го порядка с переменными сорта «список», интерпретируемые на моделях с иерархизированной надстройкой. Теория интерпретируется на деревьях вывода грамматики, описывающих поведение специфицируемой системы. Правила КС-грамматики иерархизируют пространство действий моделируемой системы. Отмечено, что для моделирования систем реального времени недостаточно выразительных возможностей Д0 T-формул. Поэтому для спецификации используются выражения с неограниченным квантором всеобщности V, известные как ПТ-формулы.

Результаты исследования. В качестве примера приводится логическая спецификация автоматизированного комплекса, который состоит из манипулятора, обрабатывающего детали. Положение позиций фиксируется датчиками. Описывается цикл работы манипулятора. Спецификация его функционирования состоит в иерархиза-ции действий правилами КС-грамматики и их описании формулами ИП 1-го порядка с учетом значений времени.

Обсуждение и заключения. В статье показано, что класс рассмотренных формул можно использовать для моделирования систем реального времени. Приводится пример логической спецификации управляющего устройства поведением манипулятора.

Об авторах

В. Н. Глушкова
ФГБОУ ВО Донской государственный технический университет
Россия

Глушкова Валентина Николаевна - доцент кафедры Математика, кандидат физикоматематических наук, старший научный сотрудник.

344003, Ростов-на-Дону, пл. Гагарина, 1



К. С. Коровина
ФГБОУ ВО Донской государственный технический университет
Россия

Коровина Ксения Сергеевна - старший преподаватель кафедры Математика.

344003, Ростов-на-Дону, пл. Гагарина, 1



Список литературы

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

2. Kowalski, R. Logic for Problem Solving, Revisited / R. Kowalski. London : Imperial College, 2014. — P. 321.

3. Кларк, Э. М. Верификация моделей программ / Э. М. Кларк, О. Грамберг мл., Д. Пелед // Москва : Изд-во Московского центра непрерывного математического образования, 2002. — 416 с.

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

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

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

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

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

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.

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

11. Гончаров, С. С. Модели данных и языки их описаний / С. С. Гончаров // Вычислительные системы. Логико-математические основы проблемы МОЗ. — 1985. — Вып. 107. — С. 52-70.

12. Мальцев, А. И. Алгебраические системы. Москва : Наука, 1976. — С. 392.

13. Глушкова, В. Н. Оценка сложности реализации логических спецификаций на основе контекстносвободных грамматик / В. Н. Глушкова // Кибернетика и системный анализ. — 1996. — № 4. — С. 50-58.

14. Горбатов, В. А. Логическое управление распределенными системами / В. А. Горбатов, М. И. Смирнов, И. С. Хлытчиев. — Москва : Энергоатомиздат, 1991. — 288 с.


Для цитирования:


Глушкова В.Н., Коровина К.С. Полиномиально вычислимые Σ-спецификации иерархизированных моделей реагирующих систем. Advanced Engineering Research. 2020;20(4):422-429. https://doi.org/10.23947/2687-1653-2020-20-4-422-429

For citation:


Glushkova V.N., Korovina K.S. Polynomially computable Σ-specifications of hierarchical models of reacting systems. Advanced Engineering Research. 2020;20(4):422-429. https://doi.org/10.23947/2687-1653-2020-20-4-422-429

Просмотров: 220


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2687-1653 (Online)