ИСТИНА

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