?????????????? ????????????? BPMN ? REO

Современные программные системы сильно увеличиваются в размерах. Это делает верификацию и валидацию таких систем все более сложной задачей. Увеличивается не только размер систем, но и количество функций и формализмов, которые необходимо разрабатывать и поддерживать для моделирования и анализа реальных приложений. Каждая система представляется в виде модели. Существует множество нотаций моделирования, таких как BPMN (Business Process Modeling Notation), UML, BPEL (Business Process Execution Language) и др. BPMN сама по себе способна представить все аспекты конкретного крупного бизнес-процесса. Поэтому BPMN является развивающимся стандартом для представления бизнес-процессов и косвенно программных систем. BPMN - это визуальная нотация моделирования процессов, которая может быть легко понята бизнес-аналитиками. Однако BPMN отстает от формальной семантики систем. Во время верификации конкретной системы таких нотаций моделирования недостаточно, чтобы обеспечить семантическую корректность системы. Таким образом, для верификации и валидации систем, согласно предлагаемому подходу, BPMN-модель системы преобразуется в REO-модель, а затем в формальный язык спецификации mCLR.