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

Рассматривается фундаментальная научная проблема автоматизированного построения надежного программного обеспечения, используется парадигма автоматного программирования, в которой логика работы программы описывается системой управляющих конечных автоматов. Этот подход позволяет строить программы, поддающиеся автоматической верификации при помощи метода Model Checking, что является преимуществом перед традиционными подходами к программированию. В проекте решается задача построения управляющих конечных автоматов по экспертным данным, заданным сценариями работы программы и темпоральными свойствами на языке линейной темпоральной логики LTL. Сценарии работы задают желаемые варианты поведения программы в начале работы, а темпоральные свойства позволяют проверить корректность работы программы во всех возможных ее состояниях. Иначе говоря, решается NP-трудная задача автоматизированного построения программного обеспечения по его спецификации. Предлагается разработать и реализовать три метода решения задачи: один приближенный метод на основе метаэвристического муравьиного алгоритма и метода Model Checking, а также два точных метода, основанных на сведении поставленной задачи к задачам SAT и QSAT совместно с методом Bounded Model Checking и применении сторонних программных средств для решения этих задач. Предполагается, будут превосходить по качеству и эффективности известные решения, основанные на генетических алгоритмах и жадном слиянии состояний, что подтверждается проведенными предварительными исследованиями и научным заделом коллектива Проекта.

Проект направлен на развитие подходов для автоматизированного синтеза надежного программного обеспечения. В рамках Проекта программное обеспечение строится с использованием автоматного подхода. Ключевой особенностью автоматных программ является то, что модель программы, являющаяся системой управляющих конечных автоматов, строится разработчиком и верифицируется на этапе проектирования программы, а не после ее реализации. В рамках проекта разработан ряд методов для автоматизированного построения управляющих автоматов. В качестве входных данных используются сценарии работы и темпоральные свойства. Управляющим конечным автоматом называется конечный автомат, каждый переход которого помечен событием, последовательностью выходных воздействий и охранным условием, представляющим собой логическую формулу от входных переменных. Входными данными для построения управляющего автомата является множество сценариев работы и множество темпоральных свойств на языке линейной темпоральной логики LTL. Решается задача построения управляющего конечного автомата, удовлетворяющего следующим требованиям: (1) число состояний автомата равно заданному числу C; (2) автомат удовлетворяет заданному множеству сценариев работы; (3) автомат удовлетворяет заданным темпоральным свойствам. Как было показано ранее, задача построения управляющего автомата с заданным числом состояний и удовлетворяющего заданному множеству сценариев работы является NP-трудной. Рассматриваемая задача является также, как минимум, NP-трудной, поэтому для ее решения выбраны метаэвристические алгоритмы и подходы, основанные на сведении к классическим NP-трудным задачам. Получены следующие результаты: 1. Разработан и реализован на языке Java первый метод, основанный на муравьином алгоритме. Для оценки соответствия управляющих автоматов заданной спецификации используется функция приспособленности, включающая компоненты для оценки соответствия автомата заданным сценариям работы и темпоральным формулам. 2. Разработана математическая модель сведения задачи построения автоматов к задаче выполнимости (SAT) - предложены переменные и дизъюнкты нового типа. Разработан и реализован на языке программирования Java второй метод решения поставленной задачи, основанный на сведении к задаче SAT. При этом проверка моделей осуществляется на путях ограниченной длины - впервые используется Bounded Model Checking для управляющих конечных автоматов. 3. Разработан и реализован третий метод построения на основе сведения к задаче квантифицированной выполнимости (QSAT) с использованием Bounded Model Checking. Предложена новая математическая модель сведения к задаче QSAT. Для реализации были использованы современные методы решения QSAT, такие как DepQBF. 4. Проведены масштабные экспериментальные исследования разработанных методов. Полученные экспериментальные результаты позволяют сделать вывод о том, что на случайных данных муравьиный алгоритм существенно эффективнее генетического. Эксперименты также показали преимущество в скорости работы над остальными второго метода.