Выбор языка программирования
Введение
Интернет с каждым днем приобретает все большую роль в производстве и повседневной жизни человека.
Данная работа посвящена созданию on-line средства для автоматической верификации автоматных программ. Практическим ее приложением явился инструмент, позволяющий строить модель программы и генерировать код, который в дальнейшем будет верифицироваться. Верификация производится с помощью метода Model Checking.
Описание предметной области
Общие понятия о верификации
Верификация модели программы – это один из основных методов поиска ошибок в программе. Для того, чтобы произвести верификацию программы, требуется:
§ Построить формальную модель, которая будет подходить для инструментальных средств верификации.
§ Сформулировать требования к модели на языке темпоральной логики. Также нужно помнить о полноте спецификации.
§ Произвести верификацию модели. Если модель не соответствует сформулированным требованиям, верификатор выдаст отчет с ошибкой, который поможет найти ошибку в программе. Также ошибка может появится в случае некорректной спецификации или неправильного построения модели. Отчет верификатора поможет устранить ошибку в формулировке спецификации или моделировании.
Верификатор SPIN
Существует большое число верификаторов, в том числе и с открытыми кодами. Наиболее популярным верификатором на данный момент является верификатор SPIN. На вход этот верификатор принимает код на языке Promela, сгенерированный по модели программы, и требования к модели, сформулированные на языке LTL. Далее по модели программы верификатор строит модель Крипке, а по требованиям к модели – автомат Бюхи. Затем строится пересечение модели Крипке и автомата Бюхи, и, если пересечение не пусто, выдается отчет с ошибкой.
Синтаксис языка Promela
Синтаксис языка Promela похож на синтаксис языка C. Модель состоит из следующих элементов:
§ объявление каналов передачи данных;
§ объявление типов данных;
§ определения и объявления процессов;
§ объявления переменных;
§ процесса init.
В принципе, процесс можно рассматривать как процедуру, выполняемую в отдельном потоке, соответственно процессы могут иметь локальные переменные и параметры. Также при использовании модификатора active, процесс можно запускать в нескольких экземплярах. Запуск осуществляется с помощью модификатора run. В языке Promela есть пять базовых типов данных: bit, bool, byte, short, int. Тело процесса представляет собой последовательность операторов. Операторы могут быть выполнимыми или заблокированными. Выполнимый оператор можно выполнить немедленно. Заблокированный оператор – это оператор, который выполнить мгновенно нельзя. Такой оператор блокирует выполнение процесса до тех пор, пока он не станет выполнимым. Например, оператор X < 7 может выполниться только когда X меньше семи. Пока условие не выполнено, процесс будет остановлен. Некоторые операторы, такие как оператор присваивания, всегда выполнимы.
Также язык Promela содержит операторы цикла и ветвления, синтаксис которых основан на охраняемых командах Дейкстры. Пример синтаксиса операторов цикла и ветвления приведен в таблице 1.1.
Таблица 1.1 – Синтаксис операторов цикла и ветвления
| if :: guard1 → S1 :: guard2 → S2 … :: else → Sk fi | do :: guard1 → S1 :: guard2 → S2 … :: else → Sk od |
Таблицу нужно понимать так: при условии выполнения guard выполняется действие Si. Если выполняются несколько условий, то недетерминированно выбирается одно из них. Если ни одно условие не выполняется, то выполняется действие Sk, соответствующее else. Конструкция else может отсутствовать. При этом выполнение процесса блокируется, пока хотя бы одно из условий не начнет выполняться.
Модель Крипке
Пусть AP —множество атомарных высказываний. Модель Крипке над этим множеством – это четверка M = (S, S0, R, L), где
§ S – конечное множество состояний;
§ S0 Í S – множество начальных состояний;
§ R Í S×S – отношение переходов;
§ L : S → 2AP –функция истинности.
Язык LTL
Язык LTL (Linear-Time Logic) состоит из множества атомарных высказываний p1, p2, … Î AP, логических связей Ø, /\, \/, →, и темпоральных операторов. Пусть φ — правильно построенная формула. Тогда
§ Xφ (в следующем состоянии φ верно — neXt);
§ Gφ (φ верно всегда — Globally);
§ Fφ (φ когда-нибудь будет верно — Finally);
§ ψUφ (ψ будет верно до тех пор, пока не станет верно φ — Until)
тоже верно построенные формулы.
Операторы G и F требуются для упрощения формул. Их можно выразить через оператор U:
§ Fφ º 1Uφ;
§ Gφ º Ø F Ø φ.
Формулы LTL интерпретируются через исполнение системы переходов в модели Крипке. Если все пути из начального состояния удовлетворяют формуле φ, то будем говорить, что поведение системы удовлетворяет формуле φ.
В таблице 1.2 приведено соответствие стандартного синтаксиса и принятого в верификаторе SPIN. Оператор X neXt) не поддерживается, так как верификатор SPIN генерирует вспомогательные и служебные состояния в модели Крипке.
Таблица 1.2 – Соответствие записи, принятой в верификаторе SPIN, и стандартного синтаксиса.
| [] | G |
| <> | F |
| ! | Ø |
| U | U |
| && или /\ | /\ |
| || или \/ | \/ |
| -> | → |
| <-> | ↔ |
Автомат Бюхи
Пусть AP – множество атомарных высказываний. Автоматом Бюхи
над алфавитом 2AP называется четверка A = (Q, q0, d, F), где
§ Q – конечное множество состояний;
§ q0 – начальное состояние;
§ d Í Q´2AP´Q – функция переходов;
§ FÍ Q – множество допустимых состояний.
Доказано, что для любой LTL-формулы можно построить автомат Бюхи, который ее выполняет. Более того, он может строиться автоматически.
Пример.Рассмотрим LTL-формулу [](p U q). Она обозначает, что
всегда гарантировано, что условие p остается верным, по крайней мере, до
тех пор, пока не станет верным условие q. Верификатор SPINее транслирует
в конструкцию never claim:
never { /* [](p U q) */
T0_init:
if
:: ((q)) -> goto accept_S9
:: ((p)) -> goto T0_init
fi;
accept_S9:
if
:: ((((p)) || ((q)))) -> goto T0_init
fi;
}
Эта конструкция соответствует автомату Бюхи, изображенному на рисунке 1.1. Двойная линия обозначает допустимое состояние.
Рисунок 1.1 Автомат Бюхи для формулы G(p U q)
С помощью автомата Бюхи можно верифицировать модель Крипке. С точки зрения верификации автоматных моделей — это наиболее удобный вариант, позволяющий при верификации и спецификации почти полностью ограничиться понятием конечный автомат.
Концепция MVC
MVC предназначен для разделения бизнес-логики и пользовательского интерфейса, чтобы разработчики могли легко изменять отдельные части приложения, не затрагивая другие. В архитектуре MVC модель предоставляет данные и правила бизнес-логики, представление отвечает за пользовательский интерфейс (например, текст, поля ввода), а контроллер обеспечивает взаимодействие между моделью и представлением.
Контроллер управляет запросами пользователя (получаемые в виде запросов HTTP, GET или POST, когда пользователь нажимает на элементы интерфейса для выполнения различных действий). Его основная функция – вызывать и координировать действие необходимых ресурсов и объектов, нужных для выполнения действий, задаваемых пользователем. Обычно контроллер вызывает соответствующую модель для задачи и выбирает подходящий вид.
Модель - это данные и правила, которые используются для работы с данными, которые представляют концепцию управления приложением. В любом приложении вся структура моделируется как данные, которые обрабатываются определённым образом. Что такое пользователь для приложения — сообщение или книга? Только данные, которые должны быть обработаны в соответствии с правилами (дата не может указывать в будущее, e-mail должен быть в определённом формате, имя не может быть длиннее Х символов, и так далее). Модель даёт контроллеру представление данных, которые запросил пользователь (сообщение, страницу книги, фотоальбом, и тому подобное). Модель данных будет одинаковой, вне зависимости от того, как мы хотим представлять их пользователю. Поэтому мы выбираем любой доступный вид для отображения данных. Модель содержит наиболее важную часть логики нашего приложения, логики, которая решает задачу, с которой мы имеем дело (форум, магазин, банк, и тому подобное). Контроллер содержит в основном организационную логику для самого приложения (очень похоже на ведение домашнего хозяйства).
Вид обеспечивает различные способы представления данных, которые получены из модели. Он может быть шаблоном, который заполняется данными. Может быть несколько различных видов, и контроллер выбирает, какой подходит наилучшим образом для текущей ситуации.
Веб приложение обычно состоит из набора контроллеров, моделей и видов. Контроллер может быть устроен как основной, который получает все запросы и вызывает другие контроллеры для выполнения действий в зависимости от ситуации.
Структура паттерна MVC представлена на рисунке 1.2.
Рисунок 1.2 Структура паттерна MVC
Концепция MVC применяется в тех случаях, чтобы показать пользователю одни и те же данные в разных контекстах. К примеру, можно выполнить следующие задачи:
§ Несколько видов связываются с одной моделью таким образом, чтобы не затронуть реализацию модели. Например, некоторые данные можно представить в виде таблиц и разных типов диаграмм;
§ Можно изменить реакцию системы на действия пользователя таким образом, чтобы не затронуть реализацию видов – достаточно просто взять другой контроллер;
§ Возможна совместная работа узко специализированных разработчиков. К примеру, программисты, разрабатывающие модель, могут вообще не знать, какой вид будет использоваться.
Постановка задачи
Цель работы – разработать веб-приложение для автоматической верификации программ. С точки зрения пользователя, приложение должно иметь возможность работать в сети Интернет без предварительной установки каких-либо дополнительных программ помимо браузера. Пользователь должен иметь возможность создавать, сохранять редактировать и удалять проекты. Также должен иметься удобный инструмент для проектирования модели и генерирования кода.
Для этого необходимо решить следующие задачи:
1. Обеспечить регистрацию пользователей в приложении;
2. Обеспечить хранение проектов в базе для каждого пользователя;
3. Разработать инструмент для проектирования автоматной модели;
4. Разработать методику записи автоматной модели на языке Promela;
5. Разработать способ преобразования автоматной модели в код на языке Promela.
Система должна по спроектированной автоматной модели сгенерировать промежуточный код на языке Promela, пригодный в дальнейшем для верификации с использованием верификатора SPIN.
Описание методов решения
Выбор языка программирования
Программное обеспечение реализовано с использованием языков PHP, 6-56256.php">2