В статье рассматриваются основные концепции, которые легли в основу В метода и Event-B. Описан процесс построения абстрактных машин и определения их характеристик с использованием структур B метода. Рассмотрены два направления B метода: классический и Event-B. Указаны подходы различных авторов к проблемам детализации и завершимости абстрактных моделей. Указано программное обеспечение, с помощью которого можно создавать абстрактные машины в нотации AMN (Abstract Machine Notation).
