3 / 23
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. «Приборостроение». 2016. № 3
67
вывода. Если стратегия вывода полна, то успех доказательства наличия
свойств зависит от полноты аксиоматизации начальных знаний. Кроме
того, полная стратегия вывода может оказаться вычислительно сложной.
Однако главное, что ограничивает использование исчислений, — слож-
ность интерпретации и аксиоматизации на языке этих исчислений необ-
ходимых сведений участниками процесса верификации, которые, как
правило, не являются специалистами в области исчислений.
Моделе-ориентированное доказательство наличия свойств
. В от-
личие от формального доказательства в рамках исчисления моделе-
ориентированное доказательство наличия свойств использует модели
архитектуры и поведения системы, в которой реализуется интерфейс.
Если разработчик этих моделей полагает, что, создавая архитектуру и
описывая поведение системы, он выполнил все предъявляемые к ним
требования, то для верификации модели остается только доказать, что ее
архитектура и поведение этим требованиям удовлетворяют. Для подоб-
ного доказательства также применяют правила вывода, но семантика
этих правил существенно ориентирована на привычные для тех или
иных приложений понятия и смыслы.
Настоящая работа основана на моделе-ориентированном доказа-
тельстве свойств систем. Одни из самых популярных моделей, исполь-
зуемых для этих целей, — процессные модели описания архитектуры и
поведения систем. Прародителем класса таких моделей является,
например, язык процессных выражений процессной алгебры (пи-
исчисления) Р. Милнера [2]. Процессные алгебры предлагают доста-
точно естественный путь описания параллельных систем, состоящих
из агентов, которые взаимодействуют по общим каналам. Описание
динамического поведения агентов обычно использует операционную
семантику, представляемую в виде правил. К сожалению, языки про-
цессных алгебр хотя и изящны с математической точки зрения, но за-
частую слишком абстрактны для применения, а управление правилами
вывода в этих языках требует дополнительных усилий, не всегда сле-
дующих непосредственно из контекста.
В связи с этим популярным является использование так называе-
мых языков архитектурного описания (Architecture Description Lan-
guage, ADL), которые позволяют на разных уровнях абстракции опи-
сывать структуру и поведение систем [3]. В настоящее время предло-
жено довольно большое число различных языков архитектурного
описания [4–7], рассчитанных, прежде всего, на описание и проверку
программных систем.
В настоящей статье для описания поведения систем и доказательства
свойств их интерфейсов предложено применять формальные системы,
основанные на правилах — тайлах (
tile
). На русский язык термин
tile
пе-
реводится как черепица, плитка, изразец, что не очень естественно ис-
пользовать для рассматриваемых целей. Поэтому здесь будем использо-
вать англицизм «логика тайлов» (
tile logic
). Принципы доказательства