Перспективные направления верификации программ

По данным, опубликованным в [6.15], ежегодно ошибки в ПО США обходятся в 60 млрд. долларов. Для преодоления этих проблем американские специалисты и специалисты из европейских стран по формальным методам и спецификациям программ приняли решение поставить теоретические достижения в этой области на производственную основу [6.16]. Этому решению предшествовали результаты исследований по формальной верификации моделей ПрО и обращений к функциям на языке API проекта SDV фирмы Microsoft, а также проверка безопасности и целостности БД и др. Кроме того, начали активно применяться формальные языки спецификации (RAISE, Z, VDM и др.) для разработки приложений. В 2005 г. был сформулирован международный проект по формальной верификации ПО.
Идея создания этого проекта принадлежит Т.Хоару, она обсуждалась на симпозиуме по верифицированному ПО в феврале 2005 г. в Калифорнии. Затем в октябре того же года на конференции IFIP в Цюрихе был принят международный проект сроком на 15 лет по разработке "целостного автоматизированного набора инструментов для проверки корректности ПС".
В нем сформулированы следующие основные задачи:
· разработка единой теории построения и анализа программ;
· построение всеобъемлющего интегрированного набора инструментов верификации для всех производственных этапов, включая разработку спецификаций и их проверку, генерацию тестовых примеров, уточнение, анализ и верификацию программ;
· создание репозитария формальных спецификаций и верифицированных программных объектов разных видов и типов.
В данном проекте предполагается, что верификация будет охватывать все аспекты создания и проверки правильности ПО и, таким образом, она станет главной альтернативой обнаружения ошибок в создаваемых программах.
В связи с тем, что комитет ISO/IEC в рамках стандарта ISO/IEC 12207:2002 провел стандартизацию процессов верификации и валидации ПО и, учитывая цель проекта, проблема создания автоматизированного набора инструментов и репозитария для проверки корректности разных объектов программирования является перспективной.
Репозитарий станет хранилищем программ, спецификаций и инструментов, применяемых при разработках и испытаниях, оценках готовых компонентов, инструментов и заготовок разных методов. В его функции входит:
· накопление верифицированных спецификаций, методов доказательства, программных объектов и реализаций кодов для разных применений;
· накопление всевозможных методов верификации, их оформление в виде, пригодном для поиска и отбора реализованной теоретической концепции для дальнейшего применения;
· разработка стандартных форм для задания и обмена формальными спецификациями разных объектов, инструментов и готовых систем;
· разработка механизмов интероперабельности и взаимодействия для переноса готовых верифицированных продуктов из репозитария в новые распределенные и сетевые среды для использования в новых ПС.
Данный проект предполагается развивать в течение 50 лет. Известно, что более ранние проекты ставили подобные цели: улучшение качества ПО, формализация моделей сервисных услуг, снижение сложности за счет использования ПИК, создание отладочного инструментария для визуальной диагностики ошибок и их устранения и др. Однако эти направления еще не получили должной реализации и предполагаемого коренного изменения в программировании пока не произошло.
Повторное обращение к технике формальной спецификации программ еще не означает, что в программе будут отсутствовать ошибки. Остаются для исследований проблемы обнаружения ошибок в программных проектах, в интерпретаторах спецификаций языков программирования, в агентных и аспектных программах и др. Реализация международного проекта по верификации ПО дает перспективу для решения многих проблем обеспечения правильности программ и систем.