22 ноября: Символьная верификация и дедуктивное тестирование программных систем

Oleksandr Letichevskyy

В докладе будет рассмотрено использование дедуктивных методов на различных этапах процесса разработки программных систем.

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

На этапе дизайна модели рассматривается доказательство аннотаций, соответствие исходным требованиям, сохранение свойств а также дедуктивное тестирование модели и доказательное моделирование.

Рассматривается также дедуктивное тестирование С\С++ кода, как особая техника тестирования достигающая максимальное покрытие сценариев поведение системы.

Докладчик: Летичевский Александр Александрович - к.ф.-м.н., ст.научн.сотр. Института кибернетики имени В.М. Глушкова (Киев). Области интересов - символьное и доказательное моделирование, техника инвариантов, техники тестирования спецификаций, автоматизация доказательств, индуктивный вывод, верификация формальных спецификаций.