Как я могу реализовать symbolic execution для particular language без использования model checking и Finite State Machine (FSM), например not, таких как Java Path Finder? Мне нужны подробности об этом. например, на каком языке я могу реализовать это символическое выполнение и что еще мне нужно знать?
реализовать символьное выполнение без проверки модели
Ответы (1)
Тебе нужно:
- Синтаксический анализатор языка для символьного выполнения, который может создавать AST.
- Разрешение имен (и связанные таблицы символов), поэтому, когда ваш механизм выполнения встречает идентификатор, он может определить связанный тип и значение.
- Анализ потока управления, чтобы механизм символьного выполнения мог отслеживать поток управления через программу.
- Символическая алгебра, которая может составлять и упрощать символические термины. Для этого нужен синтаксический анализатор (чтобы вы могли вводить такие уравнения) и довольнопринтер (чтобы вы могли видеть, что он вычисляет)
- Способ указать предполагаемые значения в точке начала символьного выполнения
Это довольно много техники, и сложно найти ее всю в одном месте. Труднее построить все это только для одного инструмента, и это одна из причин, по которой вы не найдете много таких инструментов.
В нашем наборе инструментов для реинжиниринга программного обеспечения DMS есть все необходимое. Вы можете найти интересным пример символьного языка, реализованного с помощью DMS. .
person
Ira Baxter
schedule
14.09.2016
Спасибо за вашу помощь. если я хочу использовать проверку модели, какие изменения происходят с вышеуказанными шагами? упрощает ли использование проверки модели реализацию символического выполнения, чем когда она не используется?
- person any; 14.09.2016
Для проверки модели вы должны быть готовы перечислить различные символические симуляции для каждого состояния и добавить ограничения на то, какие состояния не разрешены. Поскольку пространства состояний огромны, вы, вероятно, захотите, чтобы все это работало параллельно. DMS имеет параллельные основы:-} См. semanticdesigns.com/Products/DMS/ParlanseForDMS.html< /а>
- person Ira Baxter; 14.09.2016
большое спасибо. Не могли бы вы немного подробнее объяснить четвертый и пятый пункты ответа?
- person any; 20.09.2016
Пункт 4: см. символический язык ссылок, реализованный в DMS. В частности, это означает возможность построения алгебраических/булевых формул и механического/автоматического упрощения этих формул с использованием алгебраических законов. Пункт 5: вам нужно выбрать часть вашего кода и указать (алгебраические) условия, при которых этот код начинает выполнение (предварительное условие).
- person Ira Baxter; 20.09.2016
Спасибо Вам большое.
- person any; 21.09.2016
