4. Модель Крипке

Пусть AP —множество атомарных высказываний. Модель Крипке над этим множеством – это четверка M = (S, S0, R, L), где

• S – конечное множество состояний;

• S0  S – множество начальных состояний;

• R  S×S – отношение переходов;

• L : S → 2AP –функция истинности.

5. Язык 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
&& или /\	/\
|| или \/	\/
->	→
<->	↔

6. Автомат Бюхи

Пусть AP – множество атомарных высказываний. Автоматом Бюхи над алфавитом 2AP называется четверка A = (Q, q0, , F), где

• Q – конечное множество состояний;

• q0 – начальное состояние;

•   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)

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

7. Концепция mvc

MVC предназначен для разделения бизнес-логики и пользовательского интерфейса, чтобы разработчики могли легко изменять отдельные части приложения, не затрагивая другие. В архитектуре MVC модель предоставляет данные и правила бизнес-логики, представление отвечает за пользовательский интерфейс (например, текст, поля ввода), а контроллер обеспечивает взаимодействие между моделью и представлением.

Контроллер управляет запросами пользователя (получаемые в виде запросов HTTP, GET или POST, когда пользователь нажимает на элементы интерфейса для выполнения различных действий). Его основная функция – вызывать и координировать действие необходимых ресурсов и объектов, нужных для выполнения действий, задаваемых пользователем. Обычно контроллер вызывает соответствующую модель для задачи и выбирает подходящий вид.

Модель - это данные и правила, которые используются для работы с данными, которые представляют концепцию управления приложением. В любом приложении вся структура моделируется как данные, которые обрабатываются определённым образом. Что такое пользователь для приложения — сообщение или книга? Только данные, которые должны быть обработаны в соответствии с правилами (дата не может указывать в будущее, e-mail должен быть в определённом формате, имя не может быть длиннее Х символов, и так далее). Модель даёт контроллеру представление данных, которые запросил пользователь (сообщение, страницу книги, фотоальбом, и тому подобное). Модель данных будет одинаковой, вне зависимости от того, как мы хотим представлять их пользователю. Поэтому мы выбираем любой доступный вид для отображения данных. Модель содержит наиболее важную часть логики нашего приложения, логики, которая решает задачу, с которой мы имеем дело (форум, магазин, банк, и тому подобное). Контроллер содержит в основном организационную логику для самого приложения (очень похоже на ведение домашнего хозяйства).

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

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

Структура паттерна MVC представлена на рисунке 1.2.

Рисунок 1.2 Структура паттерна MVC

Концепция MVC применяется в тех случаях, чтобы показать пользователю одни и те же данные в разных контекстах. К примеру, можно выполнить следующие задачи:

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

• Можно изменить реакцию системы на действия пользователя таким образом, чтобы не затронуть реализацию видов – достаточно просто взять другой контроллер;

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