Технология UniTesK
Комплексный подход, позволяющий автоматизировать целый спектр задач тестирования на основе математических моделей, представляет собой технология тестирования UniTesK [, , ], разработанная в Институте Системного Программирования РАН. Данная технология использует широко известный подход программных контрактов [] для формального описания требований к программному обеспечению и уникальные методы генерации сложных последовательностей тестовых воздействий на основе неявного описания конечного автомата. Эффективность такого подхода была подтверждена в многочисленных проектах [], и, в частности, при разработке тестового набора для ядра операционной системы канадского телекоммуникационного гиганта Nortel Networks [].
Технология тестирования UniTesK основывается на базовых принципах формальных методов, таких как формальные спецификации требований к программной системе, и в то же время остается доступной для применения в крупных индустриальных проектах. Ключевым элементов в достижении этого является переход от доказательства корректности программной системы к проверке корректности реального поведения системы на тестовых данных. Для этого вместо построения модели реализации программной системы и доказательства ее корректности относительно модели требований на всех возможных входных данных используется наблюдение за реальным поведением программной системы на конкретных тестовых данных, построение по результатам наблюдения модели поведения системы и доказательство корректности этой модели относительно модели требований (рисунок 2).
Такое решение обладает двумя существенными достоинствами, которые обусловлены тем, что модель поведения программной системы на конкретных данных значительно проще, чем модель реализации этой системы, отражающая поведение программной системы на всех возможных входных данных.
Первое достоинство решения, предлагаемого технологией UniTesK, заключается в значительном сглаживании перехода между областью неформальных объектов и областью их математических моделей.
Этот переход является одним из наиболее критикуемых мест формальных методов []. Применительно к методам доказательства корректности программ проблема данного перехода заключается в том, что доказательство корректности математической модели реализации программной системы не гарантирует корректность самой реализации. И единственным средством для проверки соответствия между реализацией системы и ее моделью является их сопоставление, выполняемое человеком. Для реальных программных систем такое сопоставление является большой проблемой в виду размеров модели и сложности связей между ее составляющими. Модель поведения системы на конкретных данных, используемая в технологии UniTesK, является значительно более простой, чем модель реализации, а значит сопоставление модели поведения с реальным поведением системы является значительно более простым, чем сопоставление модели реализации с самой реализацией.
Второе достоинство решения, предлагаемого технологией UniTesK, состоит в упрощении методов доказательства корректности. Доказать, что поведение программной системы на конкретных тестовых данных является корректным, значительно проще, чем доказать то же самое для всех возможных входных данных. Наиболее важным практическим результатом данного факта является то, что область применимости методов доказательства корректности модели поведения программной системы на конкретных данных значительно превосходит область применимости методов доказательства корректности моделей реализации программных систем в целом. Поэтому во многих случаях, когда размеры программных систем не позволяют использовать методы доказательства корректности программ, тестирование на основе моделей по технологии UniTesK успешно применяется и доказывает свои преимущества.
Расплатой за эти преимущества является неполнота тестирования по сравнению с доказательством корректности программ. Если в результате доказательства корректности модели реализации, при допущении корректности соответствия между реализацией и ее моделью, следует корректность реализации на всех входных данных, то в результате доказательства корректности модели поведения программной системы на конкретных тестовых данных, при допущении корректности соответствия между реальным поведением и построенной моделью, следует корректность реализации только на тех тестовых данных, которые использовались в процессе тестирования.
С другой стороны, если сравнивать технологию UniTesK с обычными методами разработки тестов, то наличие формальных спецификаций требований и методов их автоматической проверки, позволяет значительно упростить процесс разработки высококачественных тестовых наборов. Это достигается за счет того, что добавление новых тестовых данных не требует решения задачи оценки корректности поведения тестируемой системы, так как эта оценка выполняется автоматически на основе формальной спецификации требований.
Более того, задача генерации тестовых данных также может быть в значительной степени автоматизирована на основе использования формальных спецификаций. И эта возможность также реализована в технологии UniTesK в виде уникальных методов генерации последовательностей тестовых воздействий на основе неявного описания конечного автомата.
Таким образом, технология UniTesK не предоставляет замену методам доказательства корректности программ, но позволяет воспользоваться формальным математическим базисом для разработки качественных тестов с меньшим уровнем затрат по сравнению с обычными методами разработки тестов.
