Поддержка различных языков и нотаций
Очень многие инструменты верификации ориентируются на определенные языки представления моделей и требований. При интеграции различных методов сразу же встанет вопрос о том, какие языки использовать вообще, и поддержку каких из них стоит реализовать в первую очередь.
Опыт, полученный на основе большого числа проектов по верификации промышленного ПО [, , , , , ], позволяет утверждать, что использование в рамках технологий и инструментов языков, которые как можно меньше отличаются от привычных обычным разработчикам, существенно облегчает их внедрение и использование в промышленности. Поэтому в рамках среды в первую очередь необходимо использовать такие формы представления моделей, которые были бы минимально необходимыми расширениями широко распространенных языков программирования. В дальнейшем можно добавлять поддержку для наиболее известных языков формальных спецификаций.
Поддержка различных языков и нотаций должна быть организована на уровне некоторого общего промежуточного представления языковых конструкций, используемого всеми инструментами анализа, но не пользователями непосредственно. Разработка такого промежуточного представления, применимого для многих разных языков, является нетривиальной задачей. Как показывает опыт, создать адекватное общее представление программ для сильно отличающихся языков (например, для Java и Пролога), практически невозможно. Поэтому построение интерфейса для используемого средой промежуточного представления будет постепенным, опирающимся на накапливаемый опыт работы с различными языками. Сам набор понятий, на базе которого можно создать такое представление, пока не выработан, и строить его придется уже в ходе создания описываемой среды верификации.
При наличии такой возможности стоит использовать уже имеющиеся стандартные или широко используемые библиотеки для работы с промежуточным представлением для ряда языков. Например, для C и C++ стандартом де-факто постепенно становится промежуточное представление, используемое в рамках компилятора GCC []. Значительным преимуществом использования результатов подобных проектов является гарантированные их поддержка и развитие в будущем в течение обозримого времени.
