ИСТИНА

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