ИСПОЛЬЗОВАНИЕ ПЕРСПЕКТИВ РЕСУРСОВ И УПРАВЛЕНИЯ ДЛЯ ВЕРИФИКАЦИИ ПОТОКОВ РАБОТ

Аннотация

Статья посвящена актуальной на сегодняшний день проблеме автоматической верификации потоков работ. На основе изучения существующих решений было установлено, что они не позволяют объединять различные перспективы потоков работ, и чаще всего, концентрируются на потоке управления. В связи с этим был разработан метод, объединяющий перспективы потоков работ, который позволяет находить ошибки синхронизации, взаимных блокировок и т.д. Путем анализа перспективы ресурсов и потока управления генерируется код на языке PROMELA. Полученный код может быть верифицирован с помощью SPIN, и в случае обнаружения ошибки построен контр пример. Для проведения экспериментов было разработано программное средство, доступное в открытом доступе. Положения данной статьи могут быть использованы для дальнейшего развития подхода, известного как «разработка потоков работ, управляемая моделями». Статья представляет интерес для специалистов в области разработки крупных программных систем, а также в областях, где необходимо создавать, верифицировать и исполнять потоки работ.