Формальное построение и валидация поведения торговых систем с акциями: подход на основе сетей ПетриFormal Modeling and Validation of Stock Trading Systems Behavior: A Petri Net Approach

Торговые системы с акциями - это программные платформы, используемые на финансовых рынках для поддержки обмена финансовыми инструментами между участниками. Учитывая ключевую роль систем торговли акциями в международных финансах, гарантировать правильное выполнение их процессов становится задачей первостепенной важности. Поэтому эксперты в этой области постоянно ищут новые способы проверки таких систем, в том числе подходы, которые могут обнаруживать различия между реальной платформой и ее спецификацией. Эта диссертация, в первую очередь, представляет собой исследование того, как расширения сетей Петри могут быть использованы для описания и анализа процессов в торговых системах. Сети Петри – хорошо известный формализм для моделирования параллельных распределенных систем. Кроме того, были разработаны новые методы проверки соответствия, использующие расширения сети Петри, чтобы проверить, соответствуют ли реальные процессы в торговых системах их спецификации. В результате эти методы указывают на «отклонения», т. е. конкретные различия, в которых реальная система (как записано в журналах событий) нарушает спецификацию. Чтобы продемонстрировать практическую значимость этого исследования, предложенные методы были реализованы в виде программного инструмента, и мы представляем результаты применения разработанных методов для проверки реальной торговой платформы. В работе также отображена информация об экспериментальных оценках с искусственными данными.