Static analysis and testing of executable DSL specification

Qinan Lai, Andy Carpenter

В статье определены 7 категорий ошибок, возможных в спецификациях предметно-ориентированных языков. Также предложены методы статической проверки и тестирования спецификаций предметно-ориентированных языков для устранения этих ошибок. В качестве примера рассматривается WS-BPEL (Web Services Business Process Execution Language) в модельных спецификациях, построенных по стандартам fUML (foundational UML) и ALF (Action Language for foundational UML).

Подход к разработке, основанный на модельных технологиях, проще и быстрее традиционных подходов. Модельное описание понятно и людям и машинам и позволяет генерировать безошибочную реализацию напрямую из спецификации. Однако, пока что невозможно рассмотреть все аспекты спецификации предметно-ориентированного языка и определить их несовместимость или ошибки во вложенных спецификациях.

  • Синтаксические ошибки - неправильный синтаксис, несоответствие типов. Легки для проверки, но большинство инструментов не покрывают все типы.
  • Ошибки несовместимости - ccылки на недопустимые понятия, вызванные неполным изменения модели
  • Конфликты между инвариантами мета-модели, между пре- и пост-условиями операций и статической семантикой
  • Ошибки дефицита - нехватка определенных свойств, неиспользуемые понятия, заглушки на неопределенные операции
  • Расширенные статические ошибки - могут быть обнаружены при статическом анализе, но не относятся к синтаксическим
  • Платформо-зависимые ошибки - использование особенностей платформ в платформо-независимой модели
  • Логические ошибки и ошибки во время исполнения - определяются тестированием, не статическими проверками

WS-BPEL — это предметно-ориентированный язык, направленный на построение веб-сервисов. Синтаксис определен XML, а семантика — естественным языком.

Фреймворк использует синтаксис ALF и комментарии OCL. Мета-модель (Ecore из Eclipse BPEL Designer) является ALF программой. Ограничения OCL определены как комментарии. Поведенческая семантика определена как активности и операции. Фреймворк спецификаций разработан с помощью Xtext. Так как спецификация определена при помощи ALF, ошибки могут быть обнаружены с помощью Xtext валидаторов. Также, абстрактный синтаксис, статическая и поведенческая семантика определены в одном модельном пространстве, что способствует легкому обнаружению синтаксических ошибок и ошибок несовместимости (аналогично проверке правильности ALF программы).

Xtext валидатор автоматически обнаруживает ошибки, которые возможно обнаружить при помощи парсера. Отдельные правила валидатора направлены на проверку грамматики. Ошибки в OCL проверяются вызовом OCL валидатора из плагина EMF. Расширенные статические ошибки и платформо-зависимые ошибки обнаруживаются аналогично. Все статические проверки требуют десятки-сотни строчек несложного кода и существенно уменьшают количество ошибок в спецификации.

Большинство логических ошибок и ошибок во время исполнения сложны к обнаружению статическим анализом. Конфликтные ошибки не могут быть исправлены правилами XText валидаторов. Один из путей решения — перевести спецификацию в другую область и обратно. Фреймворк может обнаружить только простейшие ошибки дефицита.