SOFTWARE FORMAL VERIFICATION OF TEST AUTOMATION OF THE SPACECRAFT SYSTEMS

Authors

  • Ігор Борисович Туркін National Aerospace University "HAI" of M.E. Zhukovskiy
  • Борис Борисович Михнич National Aerospace University "HAI" of M.E. Zhukovskiy

Keywords:

Spacecraft, test automation, software, formal verification methods, workflow model, Petri net.

Abstract

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.

Author Biographies

Ігор Борисович Туркін, National Aerospace University "HAI" of M.E. Zhukovskiy

Doctor of Technical Sciences, Professor, Head of Software Engineering Department of the National Aerospace University "HAI" of M.E. Zhukovskiy. Scientific interests: the design of real-time software.

Борис Борисович Михнич, National Aerospace University "HAI" of M.E. Zhukovskiy

Post-graduate student of Software Engineering Department of the National Aerospace University "HAI" of M.E. Zhukovskiy. Scientific interests: formal verification methods.

References

Горбулін В. П., Шевцов А. І. Збереження статусу ракетно-космічної держави – національне завдання України. Стратегічні пріоритети. – №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.

Downloads

Issue

Vol. 1 No. 1 (2010)

Section

SOFTWARE TESTING, VALIDATION AND VERIFICATION