Приложение В. Среда разработки и верификации на языке Event-B
Комплекс инструментальных средств AstraVer Toolset [109] включает в себя среду для разработки и верификации спецификаций на Event-B, основанную на платформе Rodin1. Rodin содержит в себе текстовый редактор спецификаций, который обладает возможностью обнаружения в спецификациях синтаксических ошибок. Более сложный анализ корректности проводится с помощью автоматических и интерактивных средств, которые также включены в состав Rodin. Интерактивные средства позволяют проводить доказательства вручную, причем их корректность затем проверяется одним из компонентов платформы. Автоматическое же доказательство осуществляется средствами встроенных инструментов, а также SMT решателями, которые можно добавить в Rodin с помощью плагина. Возможна и комбинация интерактивного и ручного доказательств, при которой доказательство сначала упрощается и разбивается на составные части вручную, каждая из которых затем подается на вход автоматическим инструментам.
Для каждого требующего доказательства случая — неоднозначность выражений, сохранность инвариантов, корректность проведенного пошагового уточнения (если данная техника была использована) — Rodin генерирует соответствующие утверждения для доказательства, причем платформа решает проблему поддержки актуальности сгенерированных утверждений и выполненных доказательств в случае изменений в спецификации. Полное доказательство спецификации означает, что доказаны все сгенерированные утверждения.
Далее приводятся основные типы генерируемых утверждений для доказательства:
WD (well-definedness) — аксиомы, инварианты, охранные условия и действия событий должны быть определены правильным образом. Пример: если в инварианте есть деление, то будет сгенерировано утверждение для доказательства того, что делимое не является нулем;
INV (invariant preservation) — для каждого события, изменяющего значение переменной, используемой в инварианте, требуется доказать, инвариант остается выполненным и при новых значениях переменной;
THM (proving theorems) — генерируется для доказательства справедливости аксиом, инвариантов, охранных условий, которые помечены как теоремы;
FIS (action feasibility) — каждое действие события должно быть выполнимо. Данное условие тривиально в случае детерминированных присваиваний;
GRD (guard strengthening) — охранное условие уточненного события должно являться усилением охранных условий соответствующего уточняемого события и не должно им противоречить;
SIM (action simulation) — действие уточненного события не должно противоречить действию уточняемого события;
EQL (equality of a preserved variable) — уточненное событие не должно изменять переменные уточняемой спецификации;
MRG (guard strengthening (merge)) — аналогично типу GRD, но для слияния двух уточняемых событий в одно уточненное (для слияния требуется, чтобы действия этих событий были идентичны, а одноименные параметры обладали одинаковым типом);
VWD (well definedness of a witness) — аналогично WD, но для свидетельств;
WFIS (feasibility of a witness) — аналогично FIS, но для свидетельств.
Rodin разработан на базе интегрированной среды разработки Eclipse и обладает набором расширяющих функциональность плагинов. В работе по спецификации МРОСЛ ДП-модели использовались плагины SMT Solvers и Atelier B Provers для расширения возможностей средств автоматического доказательства. На ранних этапах разработки также использовались альтернативный текстовый редактор спецификаций Camille и инструмент проверки и анимации моделей (model checking) ProB, однако от них пришлось отказаться из-за возникших проблем с производительностью в следствии роста размера спецификации.
Отдельного упоминания заслуживает Theory Plugin, который позволяет пользователям расширять математическую нотацию Event-B. Вместе с плагином поставляется набор готовых к использованию теорий, среди которых есть теории двоичных деревьев, списков, последовательностей, действительных чисел.
В.1. Пошаговое уточнение в Event-B
Поскольку поведение сложных систем описывается сложными же спецификациями, проведение их верификации также может требовать значительных усилий. Для облегчения этого процесса часто применяется техника пошагового уточнения (далее просто уточнение). Уточнение было разработано для декомпозиции сложных систем на составные части, которые легче понять и поддерживать.
Уточнение — это широко известная техника декомпозиции спецификаций, одно из первых формальных описаний которой можно встретить в работе Р.-Й. Бака 1978 года [110]. Данная техника поддерживается многими формальными методами. Вместо создания единой монолитной спецификации, которая будет содержать в себе все детали моделируемой системы, уточнение предлагает разрабатывать серию связанных между собой спецификаций. В такой серии первая спецификация представляет собой некоторую базовую версию системы, которая содержит в себе только основные детали. Дополнительные детали системы шаг за шагом добавляются в остальных спецификациях серии таким образом, что каждая последующая спецификация в серии является уточнением предыдущих.
Уточнение может быть двух типов. Горизонтальное уточнение используется для добавления новых свойств и событий, тогда как вертикальное уточнение позволяет заменять имеющиеся абстрактные структуры данных спецификации на более конкретные, как, например, неупорядоченное множество можно заменить на упорядоченный массив. Данный способ также иногда называют уточнением данных.
Отношение между двумя спецификациями, которые можно назвать уточняемой и уточненной, считается отношением уточнения, если выполнены следующие условия:
переменные уточненной спецификации включают все переменные уточняемой и могут содержать новые переменные. Заимствованные из уточняемой спецификации переменные называются далее старыми переменными, все остальные переменные уточненной спецификации новыми;
если взять значения только старых переменных в любом начальном состоянии уточненной спецификации, должно получиться начальное состояние уточняемой спецификации (множество начальных состояний, рассматриваемое с точки зрения значений заимствованных переменных, может только сузиться в уточненной спецификации);
события уточненной спецификации содержат все события уточняемой и могут включать новые события;
правила, описывающие изменения переменных при наступлении событий, либо остаются неизменными, либо расширяются следующим образом:
предусловия событий, имеющихся в уточняемой спецификации, в уточненной могут сохраняться или усиливаться (т. е. из уточненного предусловия должно следовать уточняемое);
постусловия событий, имеющихся в уточняемой спецификации, в уточненной могут быть пополнены правилами изменения новых переменных. Старые переменные должны меняться в точности по тем же правилам, что и в уточняемой спецификации;
постусловия новых событий уточненной спецификации могут описывать только изменения новых переменных.
Корректность каждого шага уточнения должна быть доказана, так как новые детали, добавляемые на определенном уровне уточнения, могут противоречить деталям, определенным ранее. Однако если проводить уточнение с использованием специальных правил трансформации, то оно может быть корректно по построению, что позволит избежать дополнительных доказательств.
Если уточнение построено корректно (выполняются указанные ограничения на отношение между двумя спецификациями), то инварианты, верные для уточняемой спецификации, будут верны и для уточненной спецификации. Соответственно, их можно не проверять, если доказана корректность уточнения, сэкономив тем самым усилия на проверку корректности уточненной спецификации.
Крайне важно понимать возможности и ограничения уточнения, особенности выбранного формального метода и, разумеется, самой формализуемой системы. Каждое неверное решение может в итоге привести к необходимости полной переделки спецификации. В некоторых случаях неправильно проведенное уточнение может затруднить формализацию и верификацию.
Платформа включает в себя базовый набор инструментов и средства для расширения функциональности.↩︎