Цель работы



Скачать 33.14 Kb.
Дата13.02.2017
Размер33.14 Kb.
Просмотров123
Скачиваний0


Аннотация

Данная работа содержит в себе описание алгоритма решения задачи построения управляющих конечных автоматов по экспертным данным и темпоральным свойствам с помощью сведения данной задачи к задаче о выполнимости обобщенной булевой формулы (Quantified Boolean Formula).


Введение


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

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

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

Цель работы


В работе [1] было спроектировано решение, позволяющее решить задачу построения автомата по сценариям работы с помощью сведения ее к задаче SAT, задаче о выполнимости булевой формулы. После этого сторонний SAT-solver находил решение данной формулы и на основании полученного примера построенный алгоритм строил необходимый автомат.

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


Базовые положения исследования

Входные условия и переменные


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

    • Пропозициональные переменные Prop

    • Булевы связки (¬, ∧, v)

    • Темпоральные операторы X (neXt) и U (Until)

    • Выведенные темпоральные операторы F(Future), G(Globally in the future), R(Release)

Пример входнного темпорального свойства:

(e1 R ¬e2) ∧ G (e2 -> N(e1 R ¬e2))


Алогоритм работы программного средства


Разработанное програмное средство в несколько шагов производит построение искомого конечного автомата:

  1. С помощью разработанного в работе [1] алгоритма по заданным сценариям работы создается булева формула

  2. С помощью подхода Bounded Model Checking, описанного в работе [2], входные темпоральные свойста, с помощью ограничения глубины проверки и обратных циклов, «разворачиваются» в булеву формулу.

  3. Полученные формулы с помощью кванторов «для любого» и «существует» соединяются в одну обобщенную QBF формулу



Где x, y – переменные задающие структуру автомата,



S – состояния строящегося автомата,

– отношение связанности,

– развертка LTL-формулы в SAT формулу, с помощью применения метода [2]

  1. Программное решение использует сторонне специализированное программное средство для решения полученной формулы и поиска результирующего управляющего конечного автомата.

Заключение


Разработан алгоритм автоматизированного построения управляющих автоматов по сценариям работы и темпоральным свойстав, основанный на сведении данных задач к проблеме о разрешимости обобщенной булевой формулы, содержащей оба вида кванторов «существует» и «для любого». В настоящий момент производитсся сравнение качества и скорости работы с методами, реализованными в работах [3], [4].

Литература


  1. Ulyantsev V., Tsarev F. Extended Finite-State Machine Induction using SAT-Solver /Proceedings of the Tenth International Conference on Machine Learning and Applications,ICMLA 2011, Honolulu, HI, USA // IEEE Computer Society, 2011. – V. 2. – P. 346–349.

  2. Biere A., Cimatti A., Clarke E. M., Zhu Y., Strichman O. Bounded Model Checking

  3. Егоров К.В., Шалыто А.А. Совместное применение генетического программирования и верификация моделей для построения автоматов управления системами со сложным поведением

  4. Walkinshaw N., Bogdanov K. Inferring Finite-State Models with Temporal Constraints



Поделитесь с Вашими друзьями:


База данных защищена авторским правом ©nethash.ru 2017
обратиться к администрации

войти | регистрация
    Главная страница


загрузить материал