Реализовать символическое выполнение без проверки модели

Question

Реализовать символическое выполнение без проверки модели

Как я могу реализовать symbolic execution за particular language без использования model checking а также Finite State Machine (FSM) например not такие как Java Path Finder? Мне нужна деталь об этом. например, на каком языке я могу реализовать это символическое выполнение и что еще мне нужно знать?

2

testing verification model-checking

Источник

user6454129 14 сен '16 в 12:34

1 ответ

Решение

Другие вопросы по тегам testing verification model-checking

user120163 14 сен '16 в 14:59 2016-09-14 14:59 · Accepted Answer · 2016-09-14 14:59

Тебе нужно:

Синтаксический анализатор для языка, который должен быть выполнен символически, который может создавать AST
Разрешение имени (и связанных таблиц символов), поэтому, когда ваш механизм исполнения встречает идентификатор, он может определить связанный тип и значение
Анализ потока управления, так что символический механизм выполнения может отслеживать поток управления через программу
Символическая алгебра, которая может составлять и упрощать символические термины. Для этого нужен парсер (чтобы вы могли вводить такие уравнения) и prettyprinter (чтобы вы могли видеть, что он вычисляет)
Способ указания предполагаемых значений в точке начала символического выполнения

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

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