Метод B и Event-B: формальные методы разработки программного обеспечения
B-Method
Метод B: формальная разработка ПО. Основан на нотации абстрактных машин, применяется в критически важных системах (Ariane 5, Парижское метро). Инструменты и доказательства.
Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
Метод разработки программного обеспечения
Метод B — это методология разработки программного обеспечения, основанная на языке B, формальном методе, поддерживаемом инструментами и использующем нотацию абстрактных машин, применяемом при создании компьютерного программного обеспечения.
Method of software development
The B method is a method of software development based on B, a tool supported formal method based on an abstract machine notation, used in the development of computer software.
Обзор
B был первоначально разработан в 1980-х годах Жаном Рэймоном Абриалом во Франции и Великобритании. B связан с нотацией Z (также разработанной Abrial) и поддерживает разработку кода языков программирования на основе спецификаций. B применялся в крупных системах, критичных к безопасности, в Европе (например, в автоматических линиях 14 и 1 парижского метро и ракете Ariane 5). Для B существует надежная, коммерчески доступная инструментальная поддержка для спецификации, проектирования, доказательства и генерации кода. По сравнению с Z, B имеет немного более низкий уровень абстракции и больше ориентирован на последовательное уточнение до кода, а не только на формальную спецификацию, поэтому спецификацию, написанную на B, легче правильно реализовать, чем спецификацию на Z. Для этого существует хорошая инструментальная поддержка. Один и тот же язык используется для спецификации, проектирования и программирования. В числе механизмов – инкапсуляция и локальность данных.
B was originally developed in the 1980s by Jean Raymond Abrial in France and the UK. B is related to the Z notation (also originated by Abrial) and supports development of programming language code from specifications. B has been used in major safety critical system applications in Europe (such as the automatic Paris Métro lines 14 and 1 and the Ariane 5 rocket). It has robust, commercially available tool support for specification, design, proof and code generation. Compared to Z, B is slightly more low level and more focused on refinement to code rather than just formal specification — hence it is easier to correctly implement a specification written in B than one in Z. In particular, there is good tool support for this. The same language is used in specification, design and programming. Mechanisms include encapsulation and data locality.
Событие-B
Впоследствии был разработан еще один формальный метод под названием Event B, основанный на методе B и поддерживаемый платформой Rodin. Event B – это формальный метод, предназначенный для моделирования и анализа систем на системном уровне. К особенностям Event B относятся использование теории множеств для моделирования, применение уточнения для представления систем на различных уровнях абстракции и использование математических доказательств для проверки согласованности между этими уровнями уточнения.
Subsequently, another formal method called Event B has been developed based on the B Method, support by the Rodin Platform. Event B is a formal method aimed at system level modelling and analysis. Features of Event B are the use of set theory for modelling, the use of refinement to represent systems at different levels of abstraction, and the use of mathematical proof for verifying consistency between these refinement levels.
Основные компоненты
Обозначение B опирается на теорию множеств и логику первого порядка для спецификации различных версий программного обеспечения, охватывающих весь цикл разработки проекта.
The B notation depends on set theory and first order logic in order to specify different versions of software that covers the complete cycle of project development.
Абстрактная машина
В первой и наиболее абстрактной версии, называемой Абстрактной машиной, разработчик должен определить цель проектирования.
In the first and the most abstract version, which is called Abstract Machine, the designer should specify the goal of the design.
Уточнение
Затем, на этапе уточнения, они могут дополнить спецификацию, чтобы прояснить цель или сделать абстрактную машину более конкретной, добавив детали о структурах данных и алгоритмах, определяющих, как достигается эта цель. Новая версия, называемая Refinement, должна быть доказана как непротиворечивая и включающая все свойства абстрактной машины. Разработчик может использовать библиотеки B для моделирования структур данных или для включения и импорта существующих компонентов.
Then, during a refinement step, they may pad the specification in order to clarify the goal or to turn the abstract machine more concrete by adding details about data structures and algorithms that define, how the goal is achieved. The new version, which is called Refinement, should be proven to be coherent and including all the properties of the abstract machine. The designer may make use of B libraries in order to model data structures or to include or import existing components.
Реализация
Уточнение продолжается до достижения детерминированной версии: Реализация. На протяжении всех этапов разработки используется единая нотация, и конечная версия может быть транслирована в язык программирования для компиляции.
The refinement continues until a deterministic version is achieved: the Implementation. During all of the development steps the same notation is used and the last version may be translated to a programming language for compilation.
B-инструментарий
B Toolkit – это набор программных инструментов, разработанных для поддержки использования B Tool, математического интерпретатора, основанного на теории множеств, с целью поддержки метода B. Разработка была первоначально начата Иб Холм Сёренсеном и другими специалистами в BP Research, а затем в B Core (UK) Limited. Инструментарий использует пользовательский графический интерфейс X Window Motif и предназначен в основном для работы в операционных системах Linux, Mac OS X и Solaris. Исходный код B Toolkit теперь находится в открытом доступе.
The B Toolkit is a collection of programming tools designed to support the use of the B Tool, is a set theory based mathematical interpreter, for the purposes of supporting the B Method. Development was originally undertaken by Ib Holm Sørensen and others, at BP Research and then at B Core (UK) Limited. The toolkit uses a custom X Window Motif Interface for GUI management and runs primarily on the Linux, Mac OS X and Solaris operating systems. The B Toolkit source code is now available.
Ателье Б
Разработанный компанией ClearSy, Atelier B — это промышленный инструмент, позволяющий использовать метод B в практической работе для разработки надежного и безошибочного программного обеспечения (формального программного обеспечения). Доступны две версии: 1) Community Edition, бесплатная для любого пользователя без ограничений; 2) Maintenance Edition, предназначенная исключительно для обладателей договора технической поддержки. Atelier B применялся при разработке систем автоматической безопасности для различных метрополитенов, установленных по всему миру компаниями Alstom и Siemens, а также для сертификации по стандарту Common Criteria и разработки системных моделей компаниями ATMEL и STMicroelectronics.
Developed by ClearSy, Atelier B is an industrial tool that allows for the operational use of the B Method to develop defect free proven software (formal software). Two versions are available: 1) Community Edition available to anyone without any restriction; 2) Maintenance Edition for maintenance contract holders only. Atelier B has been used to develop safety automatisms for the various subways installed throughout the world by Alstom and Siemens, and also for Common Criteria certification and the development of system models by ATMEL and STMicroelectronics.
Родин
Платформа Родена — это инструмент, поддерживающий методологию Event B.
The Rodin Platform is a tool that supports Event B.
APCB
APCB (Международльный управляющий комитет B-конференций) организовывал встречи, посвященные методу B. Он организовал конференции ZB совместно с Z User Group и конференции ABZ, включая абстрактные машины состояний (ASM) и нотацию Z.
APCB (, the International B Conference Steering Committee) has organized meetings associated with the B Method. It has organized ZB conferences with the Z User Group and ABZ conferences, including Abstract State Machines (ASM) as well as the Z notation.