Сборники трудов ИСП РАН


Комбинированный метод верификации масштабных моделей данных.

В.А. Семенов, С.В. Морозов, Д.В. Ильин.

Аннотация

Статья адресована актуальной проблеме верификации масштабных моделей данных, применяемых в различных индустриальных областях и специфицируемых на популярных универсальных объектно-ориентированных языках, таких как EXPRESS, UML/OCL. Основные преимущества языков информационного моделирования (высокая выразительность, декларативность, богатство синтаксических конструкций) отрицательно сказываются в процессе автоматической верификации спецификаций. Существующие методы верификации моделей вследствие высокой вычислительной сложности не могут использоваться для решения данной проблемы. В статье предлагается комбинированный метод верификации объектно-ориентированных моделей данных, основанный на последовательной редукции к нескольким постановкам математических задач: линейного программирования, удовлетворения ограничений (CSP), выполнимости булевых формул (SAT). Детально исследуется ключевая проблема определения необходимого количества экземпляров для генерации корректной коллекции объектов и ее редукция к задаче целочисленного линейного программирования. Работа поддержана РФФИ (грант 13-07-00390).

Ключевые слова

верификация моделей, объектно-ориентированное моделирование, UML/OCL, EXPRESS, логическое программирование в ограничениях, линейное целочисленное программирование, семантическая реконсиляция

Издание

Труды Института системного программирования РАН, том 26, вып. 2, 2014, стр. 197-230.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2014-26(2)-9

Полный текст статьи в формате pdf Вернуться к содержанию тома