Третий день SECR 2010

В третий день (15 октября) изначально было мало заинтересовавших меня докладов.

Первым из посещенных мною докладов был доклад Евгения Зуева из Интерстрон "Семантические интерфейсы языков программирования". Семантический интерфейс -- это набор классов С++, который соответствует узлам AST с небольшими дополнениями. Одной из задач исследований автора было использование XML для хранения модели и XSLT для преобразований кода. Выступление было сильно затянуто, и даже не хватило времени на вопросы. Пришлось задавать вопросы в коридоре. Готового парсера пока нет, он находится в разработке. Почему в качестве тестовой задачи для фреймворка было выбрана задача реинжиниринга UML, а не рефакторинг или какая-нибудь задача статического анализа выяснить не удалось. Почему нужно самим разрабатывать парсер, а не использовать готовый (GCC, Eclipse CDT, OpenCpp) также не очевидно. Ответ, что там теряется информация меня не очень устраивает.

Следующий доклад Набеля Азама из Софийского университета "Фреймворк мутационного тестирования для анализа моделей расчета надежности и оценки надежности ПО". Доклад был на английском, очень обстоятельно и на высоком уровне. Меня доклад заинтересовал, захотелось почитать статьи по теме.

Как всегда зажигал на конференции Стас Фомин. Умеет человек рассказывать интересно! Хотя, по большому счету, сказать что он предлагает что-то интересное и оригинальное нельзя: использовать вики для презентаций,делать презентации быстро и повторно использовать в следующий раз, тестировать знания в процессе обучения/самообучения.

В завершение был доклад Бьярна Страуструпа "Введение в C++0x". Было довольно интересно посмотреть на Бьярна и послушать про новый стандарт от создателя языка. Появилось желание почитать стандарт и попробовать фичи, реализованные в GCC.

CEE-SECR 2010. День второй

На мой взгляд, лучшими докладами второго дня были:

• Марат Ахин "Обнаружение клонов: современное состояние дел"


• Денис Тимофеев "Технология модификации программного кода, основанного на параметризуемых шаблонах"


• Михаил Моисеев "Обнаружение дефектов в многопоточных программах с синхронизацией на основе семафоров"

Их комментировать не буду.

Доклад про манифеcт SOA был для меня бесполезен. И тема SOA в целом не очень интересна, и обсуждение манифеста тем более!

Доклад Наталии Вегериной (Инфострой) "Экспертная система анализа качества исходного кода" был посвящен странной задаче: выдаче рекомендаций по улучшению качества исходного кода на основе анализа метрик.

Ирина Кузьмина (ФТИИ) поведала об особенностях реализации процесса интеграции при разработке сложных программно-аппаратных комплексов. Это доклад о том, как в конкретной организации пришли к Continuous Integration с использованием ClearCase, Putty и CruiseControl.NET.

Александр Калугин из Mercury выступил с докладом "Эффективная коммуникация в небольших аутсорсинговых проектах для зарубежных заказчиков". Было интересно послушать, но особых откровений из доклада я не вынес.

Интересным событием второго дня стал круглый стол "Написание статей по программной инженерии: курс молодого бойца". Круглый стол показал отсутствие единой точки зрения как в самом программном комитете, так и среди участников. Возможно, это поможет сформировать единые критерии рецензирования и повысить статус конференции.

CEE-SECR 2010

Конференция в целом оставила хорошие впечатления. Доклады на конференции были разной тематики, различного уровня и интересности. Конференция немного изменилась по сравнению с CEE-SECR 2009, который был совмещенным с SQA-Days: уменьшилось количество тестировщиков как среди участников, так и среди докладчиков. Кроме того, уменьшилось число докладчиков из научной среды. Сложилось впечатление, что уменьшился средний уровень докладов, хотя хорошие и интересные доклады были и на этой конференции.

Яркими пятнами первого дня конференции (13 октября) стали выступления:

• Андрея Уразова из компании Parasoft "Программирование, ориентированное на качество"


• Владимира Рубанова из ИСП РАН "Автоматическая генерация базовых тестов для программных
  интерфейсов библиотек на основе заголовочных файлов"

Эти два доклада показались интересными как своей тематикой, так и подготовкой докладчиков, хорошими ответами на вопросы.

Андрея Уразова спрашивали про точность и полноту обнаружения их средства статического анализа. По его примерным оценкам точность средства 80%. Измерений полноты анализа не выполнялось.

На сайте компании перечислены типы обнаруживаемых дефектов для С/С++:

• uninitialized or invalid memory


• null pointer dereferencing


• array and buffer overflows


• division by zero, memory and resource leaks, and dead code.

Владимира Рубанова спрашивали о смысле предлагаемого тестирования (функция вызывается с какими-то параметрами, результат не проверяется или проверяется слабо). Есть возможность как-то вручную управлять способом получения параметров. Применяется для свободно-распространямого ПО, в котором совсем нет тестов. Какие-то тесты лучше, чем никакие. Применение разработанного инструмента -- API Sanity Autotest -- позволило найти баги в реальных проектах. Сам проект свободно-распространяемый.

Выступление Радована Вречка "Конфигурационно-ориентированное программирование" понравилось меньше. С моей точки зрения в нем не было особой новизны. Не думаю, что ориентация на конфигурацию сильно облегчит жизнь и является какой-то ключевой идеей, хотя в каких-то проектах может быть полезна.

В завершении первого дня выступали Алексей Алексеев и Николай Гребнев из CustIS. Тема их доклада -- "Уменьшение влияния человеческого фактора" -- не очень совпадала с содержимым. Основной интерес для меня в их докладе был в использовании modelchecking для проверки бизнес-логики. В их подходе задаются аннотации к методам: StateTransition(fromState, toState) и StateRequire(CTL-formula). Первая аннотация означает, что вызов метода изменяет состояние с fromState в toState. Вторая аннотация описывает предусловие, которое должно выполняться в состоянии перед вызовом метода. Предусловие описывается CTL-формулой. Используется собственная реализация алгоритма CTL modelchecking.

Goanna. Обнаружитель дефектов на основе modelchecking

Goanna позволяет обнаруживать следующие типы дефектов в программах на С/С++:

• ошибки выхода за границу массива


• арифметические ошибки


• ошибки копирования


• ошибки непредсказуемого поведения (неинициализированные переменные)


• ошибки работы с памятью


• ошибки с указателями на функции


• ошибки неправильного использования указателей


• ошибки неспецифицированного порядка выполнения.

Для обнаружения дефектов используется верификатор NuSMV. Подробнее использование верификатора описано в статье Goanna: Syntactic Software Model Checking

Разработчики проверяли средство на свободно-распространяемых проектах, в том числе на Firefox.Плотность обнаружения дефектов составила 0.3-2 дефекта на 1000 строк исходного кода.

Для получения более объективной картины ниже приведены результаты средства на простых тестах (менее 20 строк кода, 1 функция):

• Выход за границу массива -- находятся случаи, когда реально выходят за границу массива и не находятся случаи, когда выходят за границу размерности (например, a[1][-1] в массиве размера 2x2)


• Разыменование указателя, выведенного за границу объекта -- не обнаруживается вообще


• Переполнения буфера для memcpy не обнаруживается


• Сравнение и вычитание указателей на различные объекты не обнаруживается


• Использование неинициализированной переменной (памяти)




• через указатель не находит


• в виде параметров функции находит


• не находится при копировании неинициализированной памяти с помощью memcpy




• Разыменование неинициализированного указателя -- находится


• Разыменование нулевого указателя -- находится в простых случаях, при использовании результата malloc, но не находится для статического указателя (инициализируется нулем)

Необходимо отметить, что ошибки выхода за границу массива достаточно хорошо обнаруживаются средством в рамках одной функции, но не находятся при межпроцедурном варианте теста.

В средстве реализовано обнаружение множества дефектов, то есть после нахождения одного дефекта анализ продолжается. Например, в коде

#include
int main(void)
{
int *p = NULL;
int *q = NULL;
*p = 0;
*q = 0;
return 0;
}

Обнаруживаются ошибки для обоих указателей, хотя после разыменования p программа упадет.

Средство порадовало отсутствием ложных обнаружений, хотя понятно, что для тестирования использовались простые программы, в которых у качественного анализатора не должно быть ложных обнаружений. Если посмотреть возможности обнаружения дефектов, то они весьма средние. Например, крайне сложные и важные для языка C ошибки выхода за границу объекта не обнаруживаются вообще.
Для тестирования использовалась версия goanna-cmdline-linux-2.1.tgz с интерфейсом командной строки.

Применение на практике mcheck

Читая описания шаблонов спецификации темпоральных свойств, встретил такую формулу

<>p -> (!p U (s & !p & X(!p U t))) 

Эта формула описывает требование, что событию p предшествуют события s,t.

На первый взгляд, кажется, что подформулу !p & X(!p U t) можно заменить на более короткую формулу !p U t. Эквивалентность этих двух формул можно легко проверить с помощью mcheck. Для этого необходимо создать файл eq.txt, содержащий пару формул с префиксом '?' и разделителем ':':

? !p & X(!p U t)
: !p U t

После запуска верификатора выясняется, что формулы не эквивалентные, и имеется контр-пример:

$ java -jar mch.jar eq.txt 
Comparing: LTL : !p & X (!p U t)

     with: LTL : !p U t


Not equivalent.

second allows: T t {T T T T}*

Анализируя контр-пример, становится понятно, что вторая формула допускает состояние с меткой t в следующем (втором) состоянии после начального, тогда как первая - не допускает!

Подходы modelchecking

Можно выделить несколько подходов к применению проверки моделей для верификации программ:

• построение моделей для существующих верификаторов (Modex/Feaver, Java2spin/JCAT, Java PathFinder 1, Bandera)


• анализатор кода и верификатор в одном средстве.

Достоинство первого подхода в том, что не нужно реализовывать верификатор. Недостаток в том, что сложно автоматически построить консистентную и адекватную модель поскольку многие возможности языков программирования не выразимы на языках моделирования напрямую (указатели, числа с плавающей запятой, динамическое выделение памяти, вызов функций, вызов через указатель, объединения, исключения, виртуальные функции, неявный вызов конструкторов), что приводит к необходимости моделировать эти конструкции имеющимися в языке верификатора средствами, а также использовать статический анализ. Кроме того, при построении модели необходимо учитывать возможности верификатора по проверке свойств (для SPIN в формулах можно использовать только глобальные переменные).

Второй подход более легко адаптируем к конструкциям языка программирования, однако более сложно реализуем. Большинство средств, использующих подход CEGAR (Counter-Example Guided Abstraction Refinement), реализованы с использование такого подхода.

Входные данные для верификации могут быть представлены:

• исходным кодом на языке программирования (Blast, YASM)


• моделью на специализированном языке (Promela, входной язык SMV)


• байт-кодом для платформ общего назначения (Java байт-код для Java Path Finder 2)


• байт-кодом виртуальной машины для генерации пространства состояний (NIPS VM-байт код для CMC)

Каналы в Promela

Каналы в языке Promela являются объектами первого порядка, то есть они могут быть переданы через канал как и любое другое значение. Это позволяет формировать динамическую структуру связей.

proctype A ( chan ptr )
{
   chan dest;  /* Объявляем канал */
   ptr ? dest; /* Считываем канал передачи из канала-параметра */ 
   dest ! 1;   /* Записываем в канал число 1 */
}

init {
   chan a = [ 1 ] of { chan }; /* Создаем канал для передачи канала */
   run A(a);                   /* Запускаем процесс с параметром-каналом */
   chan dest = [1] of {int};   /* Создаем канал назначения */
   a ! dest;                   /* Записываем в канал назначения канал передачи */
   int res;
   dest ? res;                 /* Считываем из канала передачи число */
   if
   :: res == 1 -> printf("OK") /* Убеждаемся, что считалась единица */
   fi
}

Каналы Promela можно использовать для моделирования указателей произвольной вложенности.

Простой учебный верификатор mcheck

В процессе изучения верификации методом modelchecking некоторый "разрыв" между алгоритмами верификации, использующими модель Крипке, и средствами верификации, использующими входные языки, подобные языкам программирования. Хотя по мере изучения доходят до алгоритмов, используемых средствами верификации (spin, smv), в самом начале изучения очень полезно понять и попробовать самые простые алгоритмы с явным представлением всех состояний.

В университете The University of British Columbia разработали простой учебный верификатор mcheck. Верификатор может быть запущен как апплет или как обычное java-приложение. Верификатор позволяет задать модель Крипке в простом текстовом формате:

{ > 0 1 2 p q
1 0 2 q r
2 2 r
}

Фигурные скобки задают границу описания модели Крипке. В каждой строке содержатся: номер состояния, номера состояний, в которые есть переходы из данного состояния, а также атомарные предикаты, истинные в данном состоянии. Символом '>' обозначается начальное состояние.

Верификатор поддерживает CTL- и LTL-формулы. Формулы могут размещаться в отдельном файле, либо в файле с описание структуры Крипке:

-- model
{ > 0 1 2 p q
1 0 2 q r
2 2 r
}
-- specifications
p U r -- LTL: p until r
F r -- LTL: future r
F G r -- LTL: eventually always r


Верификатор имеет возможность проверки эквивалентности LTL-формул, что можно использовать для самоконтроля при различных формулировках одного свойства, либо упрощении записи формулы.

Заманчиво в этом верификаторе то, что он очень прост сам, а также имеет простую и понятную документацию .