Интеграция спецификаций в программный код для программ с явным выделением состояний

Андрей Борисенко, Павел Федотов, Олег Степанов, Анатолий Шалыто

Тезисы

Университета информационных технологий, механики и оптики.

Андрей Борисенко

При создании систем со сложным поведением важную роль играет контроль качества разрабатываемых программ. Ошибка в таких системах может наблюдаться лишь в сложных сценариях использования, а её цена может быть слишком велика. Поэтому важно оптимизировать проверку соответствия создаваемой программы предъявленным к ней требованиям, максимально автоматизировав её. Этого можно добиться, формализовав все требования к программе и храня исполнимую спецификацию непосредственно вместе с кодом программы.

Для разработки программных систем со сложным поведением все чаще используется программирование с явным выделением состояний, позволяющее явно описывать сложное поведение. В настоящей работе исследуется вопрос формализации спецификаций систем со сложным поведением, реализованных с помощью этого подхода, и интеграции процесса верификации таких систем в общий процесс разработки программ. Кроме того, изучается проблема поддержания надежности автоматных программ при внесении в них структурных изменений.

Partners

Premium sponsors

Gold sponsors

Silver sponsors

Sponsors