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

 

ISSN 0536-1028 (Print)              ISSN 2686-9853 (Online)  
УДК 004.05 DOI: 10.21440/0536-1028-2021-7-99-108


Download

 

Цель работы. Исследование возможности применения метода формального доказательства соответствия программной реализации модели заданным требованиям для систем, модели которых могут быть представлены в виде конечных автоматов.
Актуальность. Разработка программного обеспечения для систем контроля и управления на одном из первых этапов этого процесса предполагает создание модели системы. Эта модель строится на основе технического задания, спецификации и различной априорной информации. Большая часть таких моделей для технических систем, которые эксплуатируются на современных добычных предприятиях (конвейерные системы, системы проветривания и т. п.), может быть описана с помощью модели конечного автомата. Такая модель может быть
использована для решения широкого круга задач. Следующим шагом является программная реализация модели целиком либо какой-то ее части. В связи с этим возникает задача определения соответствия программной реализации модели ее исходному описанию.
Результаты. Один из способов решения данной задачи – это формальное доказательство наличия у программной модели свойств, которые определены в спецификации (описании) исходной модели. В статье на примере шахтной конвейерной системы показано применение метода, состоящего в программной реализации модели соответствующего конечного автомата, формировании предположений о наличии у модели свойств в виде теорем с их последующим доказательством с использованием специальных программных средств.
Выводы. Использование формальных методов для спецификации, разработки и верификации программных реализаций моделей систем в совокупности с другими методами позволит повысить качество и надежность разрабатываемых решений.

Ключевые слова: конечный автомат; формальное доказательство; тестирование; соответствие спецификации; корректность реализации модели; формализация требований; Coq; автоматизация доказательства теорем; конвейерная система шахты.

 

БИБЛИОГРАФИЧЕСКИЙ СПИСОК

  1. Блюмин С. Л., Корнеев А. М. Дискретное моделирование систем автоматизации и управления: монография. Липецк: ЛЭГИ, 2005. 124 с.
  2. Ezhilarasu U. P., Mahapatra R. P., Karthick S. Finite automata problems and solutions. LAP LAMBERT Academic Publishing, 2019. 588 p.
  3. Baranov Samary. Finite state machines and algorithmic state machines: fast and simple design of complex finite state machines. ISBN Canada, 2018. 185 p.
  4. Эванс Э. Предметно-ориентированное проектирование (DDD): структуризация сложных программных систем.: пер. с англ. СПб: Диалектика, 2019. 448 с.
  5. Ларман К. Применение UML 2.0 и шаблонов проектирования: практическое руководство: пер. с англ. М.: И. Д. Вильямс, 2013. 736 с.
  6. Myers Glenford J. The art of software testing. John Wiley & Sons, Inc., Hoboken, New Jersey, 2012. 240 p.
  7. Старолетов С. М. Основы тестирования и верификации программного обеспечения. СПб: Лань, 2020. 344 с.
  8. Камкин А. С. Введение в формальные методы верификации программ. М.: МАКС Пресс, 2018. 272 с.
  9. Monin Jean-Francois. Understanding formal methods. London–New York: Springer, 2003. 275 p.
  10. Никешин А. В., Пакулин Н. В., Шнитман В. З. Мутационное тестирование сетевых протоколов с использованием формальных моделей // Научный сервис в сети Интернет: труды XVII Всероссийской научной конференции / ИПМ им. М. В. Келдыша. М., 2015. С. 259–266.
  11. Татарников А. Д. Обзор методов и средств генерации тестовых программ для микропроцессоров // Труды ИСП РАН. 2017. Т. 29. Вып. 1. С. 167–194.
  12. Камкин А. С., Сергеева Т. И., Смолов С. А., Татарников А. Д., Чупилко М. М. Расширяемая среда генерации тестовых программ для микропроцессоров // Программирование. 2014. № 1. С. 3–14.
  13. Гратинский В. А., Новиков Е. М., Захаров И. С. Экспертная оценка результатов верификации инструментов верификации моделей программ // Труды ИСП РАН. 2020. Т. 32. Вып. 5. С. 7–20.
  14. Самонов А. В., Самонова Г. Н. Методика и средства разработки и верификации формальных fUML моделей требований и архитектуры сложных программно-технических систем // Труды ИСП РАН. 2018. Т. 30. Вып. 5. С. 123–146.
  15. Boulanger J.-L. Industrial use of formal methods: formal verification. Wiley-ISTE, 2012. 298 p.
  16. Cofer D. D. et al. Compositional verification of architectural models // NASA Formal Methods: 4th International Symposium, NFM 2012, Proceedings. Norfolk, P. 126–140.
  17. Gnesi S., Margaria T. Formal methods for industrial critical systems: a survey of applications. Wiley-IEEE Press, 2013.
  18. Jackson D. Software abstractions: logic, language and analysis. MIT press, 2012.
  19. Колмогоров А. Н., Драгалин А. Г. Математическая логика. Введение в математическую логику. М.: ЛАНАНД, 2017. 240 с.
  20. Клини С. Введение в метаматематику. М.: Либроком, 2009. 523 c.
  21. Карри Х. Б. Основания математической логики. М.: Мир, 1969. 567 c.
  22. Лапин Э. С., Абдрахманов М. И. Функциональный подход к моделированию динамики систем детерминированных конечных автоматов // Известия вузов. Горный журнал. 2021. № 2. C. 113–121.
  23. Benjamin C. Pierce. Logical foundations. URL: https://softwarefoundations.cis.upenn.edu/lfcurrent/toc.html (дата обращения: 02.04.2021).
  24. Chlipala Adam. Certified programming with dependent types. MIT Press Ltd, 2014. 424 p.
  25. Ilya Sergey. Programs and proofs. URL: https://ilyasergey.net/pnp/ (дата обращения: 02.04.2021).
  26. Bertot Yves, Castéran Pierre. Interactive theorem proving and program development: Coq art: The calculus of inductive constructions. Springer, 2004. 500 p.
  27. Pisetski V. B., Kornilkov S. V., Sashurin A. D., Lapin E. S., Lapin S. E., Balakin V. Y. Concept, system solutions and the results of geotechnical monitoring and forecasting of hazardous geodynamic phenomena in the processes of underground mining // European Association of Geoscientists & Engineers: conference proceedings, 13th Conference and Exhibition Engineering Geophysics 2017, April 2017. Vol. 2017. P. 1–4.
  28. Pisetski V. B., Huang R., Patrushev Y. V., Zudilin A. E., Schneider I. V., Shirobokov M. P., Balakin V. Y. The test results of the seismic monitoring systems state of stability of the rock mass in the process of construction of road tunnels // China European Association of Geoscientists & Engineers: conference proceedings, 13th Conference and Exhibition Engineering Geophysics 2017, April 2017. Vol. 2017. P. 1–7.

 

Язык сайта

Текущий выпуск №1 

Опубликован
20 Февраля 2024 года

Наша электронная почта:
Этот адрес электронной почты защищён от спам-ботов. У вас должен быть включен JavaScript для просмотра.
Этот адрес электронной почты защищён от спам-ботов. У вас должен быть включен JavaScript для просмотра.

Мы индексируемся в: