символьное выполнение и проверка модели

При проверке модели вы должны закодировать свою систему как конечный автомат и предоставить этот FSM средству проверки модели, а также спецификацию. Затем средство проверки модели будет следить за тем, чтобы спецификация всегда выполнялась в этой системе.

При символическом выполнении вы предоставляете только свою программу, а механизм символьного выполнения проверяет все возможные пути для создания тестовых входных данных или проверки утверждений.

Простой пример их различия: параллелизм. Проверка модели может обрабатывать многопоточные системы, поскольку она указана в FSM, предоставленном в качестве входных данных, однако символическое выполнение не может обрабатывать более одного потока.

Проверка модели: метод формальной проверки того, что программа удовлетворяет спецификации. Спецификация обычно дается в виде формулы временной логики, например: «если входной сигнал x, выходной сигнал должен быть y - выполняется для всех исполнений (глобально) программы» (см., например, Эдварда Ли).

Проверка символьной модели по сравнению с явной проверкой состояния: программы могут быть конечными автоматами (FSM). Здесь достаточно явной проверки состояния. Но, к счастью, средства проверки моделей существуют и для расширенных конечных автоматов, параллельных вероятностных приложений реального времени. Чтобы предотвратить взрыв состояния в системах с очень большим (бесконечным) числом состояний, используется проверка символьной модели. В символической модели проверки состояния и входы и т. д. рассматриваются как символы и пропозициональные формулы (или наборы состояний, операции над множествами и т. д.). Для выполнения проверки модели необходим анализ достижимости, и для этого программные переходы выполняются символически. Эти средства проверки не могут использовать нормальное выполнение инструментированного машинного кода.

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

Наконец, несколько примеров:

JPF, Java-Pathfinder: проверка модели, явная проверка состояния, ввод: байт-код java

SPF, Symbolic Pathfinder: символическое выполнение, расширение JPF

JCBMC: средство проверки ограниченной модели, расширение JPF, SPF

XRT: исследование и символьное выполнение, ввод: байт-код CIL

IntelliTest: параметризованные модульные тесты используют XRT

Spec Explorer: тестирование на основе моделей использует XRT