SOFTWARE FORMAL VERIFICATION OF TEST AUTOMATION OF THE SPACECRAFT SYSTEMS
Наукові журнали НАУ
Переглянути архів Інформація| Поле | Співвідношення | |
| Title |
SOFTWARE FORMAL VERIFICATION OF TEST AUTOMATION OF THE SPACECRAFT SYSTEMS
ФОРМАЛЬНАЯ ВЕРИФИКАЦИЯ ПРОГРАММНОГО ОБЕСПЕЧЕНИЯ ДЛЯ АВТОМАТИЗАЦИИ ИСПЫТАНИЙ СИСТЕМ КОСМИЧЕСКИХ АППАРАТОВ ФОРМАЛЬНА ВЕРИФІКАЦІЯ ПРОГРАМНОГО ЗАБЕЗПЕЧЕННЯ ДЛЯ АВТОМАТИЗАЦІЇ ВИПРОБУВАНЬ СИСТЕМ КОСМІЧНИХ АПАРАТІВ |
|
| Creator |
Туркін, Ігор Борисович; Національний аерокосмічний університет «ХАІ» імені М.Є. Жуковського
Михнич, Борис Борисович; Національний аерокосмічний університет «ХАІ» імені М.Є. Жуковського |
|
| Subject |
Spacecraft; test automation; software; formal verification methods; workflow model; Petri net.
004.415.5 Космический аппарат; автоматизация испытаний; программное обеспечение; формальные методы верификации; модель потоков работ; сеть Петри. 004.415.5 Космічний апарат; автоматизація випробувань; програмне забезпечення; формальні методи верифікації; модель потоків робіт; мережа Петрі. 004.415.5 |
|
| Description |
Features of application of Windows Workflow Foundation technology on software development for test bench automatization of such spacecraft subsystem. There was shown that application of given technology allows the technologist to describe directly computational process flow, using base run-units (executed units) or templates in the form of working streams. This increases clearness and simplifies further system modification. The mechanism of verification of working threads of the applications constructed under specification Windows Workflow Foundation and capable to change business logic at a performance stage is considered. The mechanism of transformation of working threads in the notation of Petri nets offered and the example of such transformation is resulted. For verification it is offered to use a mathematical apparatus of Petri nets, analyzing properties faultlessness closed equivalent Petri net. Definition of the requirements characterizing faultlessness Petri net is made.
Рассматриваются особенности применения технологии Windows Workflow Foundation при разработке программного обеспечения для автоматизации стендовых испытаний подсистем космических аппаратов. Показано, что применение данной технологии позволяет технологу непосредственно описать ход вычислительного процесса, используя базовые исполняемые блоки или шаблоны в виде потоков работ, что повышает информативность и упрощает дальнейшие модификации системы. Рассматривается механизм верификации приложений, построенных по спецификации Windows Workflow Foundation и способных изменять бизнес-логику на этапе выполнения. Предложен механизм преобразования процесса в нотации сетей Петри. Для верификации предлагается использовать математический аппарат сетей Петри, анализируя свойства бездефектности замкнутой эквивалентной сети Петри. Дано определение требований, характеризующих бездефектную сеть Петри. Розглядаються особливості застосування технології Windows Workflow Foundation при розробці програмного забезпечення для автоматизації стендових випробувань підсистем космічних апаратів. Показано, що застосування даної технології дозволяє технологу безпосередньо описати хід обчислювального процесу, використовуючи базові блоки або шаблони у вигляді потоків робіт, що підвищує інформативність і спрощує подальші модифікації системи. Розглядається механізм верифікації програм, побудованих за специфікацією Windows Workflow Foundation і здатних змінювати бізнес-логіку під час виконання. Запропоновано механізм перетворення робочих потоків у нотацію мереж Петрі і наведений приклад такого перетворення. Для верифікації запропоновано використовувати математичний апарат мереж Петрі, шляхом аналізу властивостей бездефектної замкнутої еквівалентної мережі Петрі. Дано визначення вимог, що характеризують бездефектну мережу Петрі. |
|
| Publisher |
National Aviation University
|
|
| Contributor |
—
— — |
|
| Date |
2012-12-11
|
|
| Type |
—
— — |
|
| Format |
application/pdf
|
|
| Identifier |
http://jrnl.nau.edu.ua/index.php/IPZ/article/view/3383
|
|
| Source |
Інженерія програмного забезпечення; Том 1, № 1 (2010); 15
Engineering Software; Том 1, № 1 (2010); 15 Инженерия программного обеспечения; Том 1, № 1 (2010); 15 |
|
| Language |
ru
|
|