Спецификации UniTesK и статический анализ
Распространённый подход к верификации встроенного программного обеспечения основан на статическом анализе системы. К статическому анализу мы относим процедуры исследования свойств ПО по априорным описаниям или моделям. Примерами статического анализа систем могут служить аналитическая верификация и model-checking.
В методах статического анализа систем широко используются формальные спецификации для исследования свойств программных систем (таких как отсутствие тупиковых ситуаций, обязательное завершение исполнения, временные характеристики и т.п.).
Интересно сопоставить формальные спецификации UniTesK и формальные спецификации для статических методов. Можно задать следующие вопросы:
- применимы ли формальные спецификаций UniTesK для проведения априорных рассуждений о свойствах описываемых программ?
- применимы ли формальные спецификации, которые используются в такого рода исследованиях, для тестирования?
Как показывает практика, спецификации для анализа и спецификации для тестирования существенно различаются по своим свойствам. Спецификации для тестирования предоставляют разработчику гибкие, но трудно верифицируемые средства. Спецификации для анализа требуют применения строго ограниченных средств, которые стесняют разработчика спецификаций или трудно применимы для автоматического построения оракула.
К примеру, в спецификациях CTesK разрешается использование указателей, циклов и произвольных выражений языка С. Как нам представляется, наши спецификации можно (в принципе) использовать для анализа и доказательства теорем о свойствах описываемой системы, но для этого надо, как минимум, запретить указатели, циклы с переменными границами (ограничители времени исполнения) и ограничить выражения, которые могут встречаться в пред- и постусловиях. Мы считаем, что при выполнении указанных требований язык CTesK станет в один ряд с такими языками как VDM, RaiseSL, а для них имеются системы аналитической верификации. Правда, при этом пропадёт основное преимущество языка CTesK — приближенность к конечному пользователю.
На применимость методов статического анализа влияетещё один аспект — сложность модели(спецификации). Как показывает наша практика, модель, достаточно детальная для построения оракула, оказывается слишком сложной для автоматического анализа. Анализ возможен только для относительно простых моделей, которые могут дать лишь общий оракул, недостаточный для целей тестирования.
Вывод: спецификации, которые используются в UniTesK, могут, в принципе, использоваться для статического анализа встроенного ПО. На практике этому препятствует гибкость выразительных средств, которые используют разработчики спецификаций, и сложность моделей, необходимых для построения оракулов.
