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