Символьное моделирование - Symbolic simulation
В информатике симуляция - это вычисление выполнения некоторой соответствующим образом смоделированной системы перехода между состояниями . Обычно этот процесс моделирует полное состояние системы в отдельных точках в дискретном линейном временном интервале, вычисляя каждое состояние последовательно, начиная с его предшественника. Модели для компьютерных программ или логических схем СБИС можно очень легко смоделировать, поскольку они часто имеют операционную семантику, которая может использоваться непосредственно для моделирования.
Символьное моделирование - это форма моделирования, в которой одновременно рассматриваются многие возможные варианты выполнения системы. Обычно это достигается за счет расширения области, в которой происходит моделирование. Символьная переменная может использоваться в представлении состояния моделирования для индексации нескольких запусков системы. Для каждой возможной оценки этих переменных существует конкретное состояние системы, которое косвенно моделируется.
Поскольку символьное моделирование может охватывать множество запусков системы за одно моделирование, оно может значительно уменьшить размер проблем проверки. Такие методы, как оценка символьной траектории (STE) и обобщенная оценка символьной траектории (GSTE), основаны на этой идее символьного моделирования.