ФОРМАЛЬНА ВЕРИФІКАЦІЯ ПРОГРАМНОГО ЗАБЕЗПЕЧЕННЯ ДЛЯ АВТОМАТИЗАЦІЇ ВИПРОБУВАНЬ СИСТЕМ КОСМІЧНИХ АПАРАТІВ
Ключові слова:
Космічний апарат, автоматизація випробувань, програмне забезпечення, формальні методи верифікації, модель потоків робіт, мережа Петрі.Анотація
Розглядаються особливості застосування технології Windows Workflow Foundation при розробці програмного забезпечення для автоматизації стендових випробувань підсистем космічних апаратів. Показано, що застосування даної технології дозволяє технологу безпосередньо описати хід обчислювального процесу, використовуючи базові блоки або шаблони у вигляді потоків робіт, що підвищує інформативність і спрощує подальші модифікації системи. Розглядається механізм верифікації програм, побудованих за специфікацією Windows Workflow Foundation і здатних змінювати бізнес-логіку під час виконання. Запропоновано механізм перетворення робочих потоків у нотацію мереж Петрі і наведений приклад такого перетворення. Для верифікації запропоновано використовувати математичний апарат мереж Петрі, шляхом аналізу властивостей бездефектної замкнутої еквівалентної мережі Петрі. Дано визначення вимог, що характеризують бездефектну мережу Петрі.Посилання
Горбулін В. П., Шевцов А. І. Збереження статусу ракетно-космічної держави – національне завдання України. Стратегічні пріоритети. – №1(6). – 2008. – С. 144 – 152.
Языково-ориентированное проектирование программного обеспечения для автоматизации стендовых испытаний подсистемы данных платформы спутника МС-2-8/Михнич Б.Б., Олейник С.В., Соколова Е.В. // Радиоэлектроные и компьютерные системы. – 2008. – №5(32). – С. 173 – 176.
Солнечные энергосистемы космических аппаратов. Физическое и математическое моделирование/ Под ред. акад. НАН Украины С.Н. Конюхова. – Харьков: Гос. аэрокосмический ун-т "Харьк. авиац. ин-т", 2000. – 516 с.
Советов Б. Я., Яковлев С. А. Моделирование систем. М.: Высш. шк., 2001. – 322 с.
Касьянов В. Н., Евстигнеев В. А. Графы в программировании: обработка, визуализация и применение. СПб.:БХВ-Петербург, 2003. – 262с.
Baeten J. C. M., Bergstra J. A. Real time Process Algebra. Formal Aspects of Computing, Vol. 3, 1991. – Р.142 – 188.
Ben-Ari M., Manna Z., Pnueli A.: The Temporal Logic of Branching Time. Proc. 8th Annual Symposium on Principles of Programming Languages ACM Press, Williamsburg. Springer-Verlag, 1992. – Р. 164 – 176.
C# 2005 и платформа .NET 3.0 для профессионалов / Кристиан Нейгел, Билл Ивьен – Издательство: Диалектика, 2008 – 1376 с.
Yet Another Workflow Language [Электронный ресурс]/[Pежим доступа]: http://www.yawl-system.com/
Wil van der Aalst Workflow Management: Models, Methods and Systems / Wil van der Aalst, Kees van Hee – Cambridge MIT Press, MA, USA 2002.
W.P.M. van der Aalast. Verification of Workflows nets / Application and Theory of Petri Nets / Berlin Springer-Verlag – 1997. – Р. 407-426.
