Информационные технологии в науке, образовании и производстве ИТНОП-2010. Материалы IV-й Международной научно-технической конференции. Том 2

Подождите немного. Документ загружается.

Министерство образования и науки Российской Федерации

Государственный НИИ информационных технологий и телекоммуникаций «Информика»

Санкт-Петербургский технологический институт (технический университет)

Российский университет дружбы народов

(филиал, г. Белгород)

Институт математики и информатики НАН Республики Молдова

Университет г. Ланкастер (Англия)

Университет г. Реймс (Франция)

Национальная высшая горная школа Сент-Этьен (Франция)

Орловский государственный технический университет

Информационные технологии

в науке, образовании и производстве

ИТНОП-2010

Материалы IV-й Международной

научно-технической конференции

22-23 апреля 2010 года, г. Орел

Том 2

Методологические и теоретические аспекты

создания и развития информационных технологий

Орел 2010

УДК 004 (062):[001+378.1+6] (062)

ББК 3297я431:72я431+74.48я431+3я431

И74

Печатается по решению программного комитета конференции.

И74 Информационные технологии в науке, образовании и производстве. ИТНОП-

2010: материалы IV-й Международной научно-технической конференции, г. Орел,

22-23 апреля 2010 г. – В 5-ти т. Т. 2 / под общ. ред. д-ра техн. наук проф.

И.С. Константинова. − Орел: ОрелГТУ, 2010. − 200 с.

ISBN 978-5-93932-272-0

Материалы IV-й Международной научно-технической конференции

представлены в пяти томах. Научные статьи посвящены актуальным проблемам в

области информатики и вычислительной техники; отражены научные достижения в

таких сферах, как математическое и программное обеспечение вычислительной

техники и автоматизированных систем; компьютерное моделирование; автоматизация

и управление технологическими процессами и производствами; телекоммуни-

кационные системы и компьютерные сети; информационная безопасность и защита

информации; информационные технологии в социально-экономических и

организационно-технических системах.

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

и теоретических аспектов создания и развития информационных технологий.

Материалы конференции предназначены для научных работников.

Секция 1. Методологические и теоретические аспекты создания и развития

информационных технологий.

Сопредседатели: д-р.техн.наук, проф. Гайндрик К.В. (институт математики

и информатики РАН Республики Молдова); д-р.техн.наук, проф. Коськин А.В.

(ОрелГТУ)

Секция 2. Проблемы применения информационных технологий в производстве.

Сопредседатели: д-р.техн.наук., проф. Долгий А. (Национальная высшая горная

школа Сент-Этьен, Франция); д-р.техн.наук, проф. Раков В.И. (ОрелГТУ)

Секция 3. Актуальные вопросы создания единого информационного

образовательного пространства.

Сопредседатели: профессор Маркарян Г. (университет г. Ланкастер, Англия);

д-р.экон. наук, проф. Савина О.А. (ОрелГТУ)

Секция 4. Проектирование и внедрение распределенных телекоммуникационных

систем и структур управления.

Сопредседатели: Цейтон Ж. (директор института информационных технологий

и коммуникаций университета г. Реймс, Франция);

д-р.техн.наук, проф. Еременко В.Т. (ОрелГТУ)

УДК 004 (062):[001+378.1+6] (062)

ББК 3297я431:72я431+74.48я431+3я431

ISBN 978-5-93932-272-0

ИТНОП-2010

УДК 004.432.2; 004.415.25

О.В. АМЕЛИНА

ПРОБЛЕМЫ И ПЕРСПЕКТИВЫ РАЗВИТИЯ ОБЪЕКТНО-

ОРИЕНТИРОВАННЫХ ТЕХНОЛОГИЙ

Статья посвящена объектно-ориентированному программированию, раскрывается его

сущность, описываются преимущества и недостатки. В качестве перспективы развития объектно-

ориентированных технологий рассматриваются унифицированный язык моделирования (UML), а

также компонентно-ориентированное программирование.

Ключевые слова: объектно-ориентированное программирование; компонентно-

ориентированное программирование; унифицированный язык моделирования; императивные языки

программирования.

This article explains the nature of object-oriented programming and it advantage and disadvantage.

As a perspective of development of object-oriented technology discussed a Unified Modeling Language and

Component-oriented Software Composition.

Keywords: object-oriented programming; component-oriented programming; unified modeling

language; imperative programming languages.

Начиная с середины 60-х годов и до недавнего времени, широкое распространение

получили структурные методологии анализа, проектирования и разработки информационных

систем, которые характеризуются искусственным разделением (часто неоптимальным)

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

в системе. В отличие от них, объектные технологии, ориентированные на тесную

взаимосвязь процессов и данных системы, позволяют программным системам быть более

надежными, легко реализуемыми и устойчивыми к изменениям.

Тем не менее, объектно-ориентированное программирование (ООП) основывается на

тех же принципах, что и традиционное, процедурное программирование. ООП обладает

императивным обликом. Процесс описывается как последовательность преобразований

состояния. Новшество состоит в разбиении глобального состояния на отдельные объекты и

связывании с объектом преобразователей состояния, называемых методами. Объекты

представляются как акторы, которые посылают другим объектам сообщения, побуждая их

изменять свое состояние. Описание шаблона объекта называется определением класса.

Эта парадигма непосредственно отражает структуру систем реального мира и поэтому

хорошо подходит для моделирования сложных систем со сложным поведением. Истоки ОПП

лежат в области имитационного моделирования систем. Успех ООП в области разработки

программных систем говорит сам за себя, начиная с языка Smalltalk и продолжая линией

Object Pascal, C++, Eiffel, Oberon, Java, и C#.

Несмотря на явное преимущество объектно-ориентированных технологий анализа и

проектирования перед структурными, их распространение сопровождалось постоянной

критикой со стороны ученых и разработчиков, поскольку ни один из методов не давал

единой и цельной объектной модели системы. Каждый метод хорошо освещал одну или

несколько сторон реальной системы, оставляя в тени множество других, не менее важных

сторон. Кроме того, отсутствие единого стандарта очень мешало широкому

распространению объектно-ориентированных методов при разработке программного

обеспечения.

UML

В качестве отраслевого стандарта расширяемого языка объектного моделирования в

OMG (Object Management Group) — некоммерческое объединение, занимающееся

разработкой и продвижением объектно-ориентированных технологий и стандартов — был

передан результат совместных усилий ученых Rational Software Corporation, а также

представителей множества компаний, таких, как Microsoft, IBM, Hewlett-Packard, Oracle,

IV Международная научно-техническая конференция

DEC, Unisys, IntelliCorp, Platinum Technology и нескольких сотен других. Этот результат

объединил все существенные и успешные разработки в данной области и известен как

унифицированный язык моделирования.

Унифицированный язык моделирования (Unified Modeling Language, UML) является

графическим языком для визуализации, специфицирования, конструирования и

документирования систем, в которых большая роль принадлежит программному

обеспечению. С помощью UML можно разработать детальный план создаваемой системы.

Такой план содержит не только ее концептуальные элементы, такие, как системные функции

и бизнес-процессы, но и конкретные особенности, например, классы, написанные на

специальных языках программирования, схемы баз данных и программные компоненты

многократного использования.

UML может быть применен на всех этапах жизненного цикла анализа бизнес-систем и

разработки приложений. Различные виды диаграмм, поддерживаемые UML, и богатейший

набор возможностей представления определенных аспектов системы делает UML

универсальным средством описания как программных, так и деловых систем.

Диаграммы дают возможность представить систему (как деловую, так и

программную) в таком виде, чтобы ее можно было легко перевести в программный код.

Кроме того, UML специально создавался для оптимизации процесса разработки

программных систем, что позволяет увеличить эффективность реализации программных

систем в несколько раз и заметно улучшить качество конечного продукта.

Несмотря на свою молодость, UML уже прекрасно зарекомендовал себя на множестве

успешных программных проектов. Средства автоматической кодогенерации позволяют

переводить модели на языке UML в исходный код объектно-ориентированных языков

программирования, что еще более ускоряет процесс разработки.

Практически все мировые производители CASE-средств заявили о реализации

поддержки UML в ближайших версиях своих продуктов. Уже сегодня существуют

множество CASE-средств, автоматизирующих процесс анализа и проектирования в UML

(Rational Rose, Paradigm Plus, Select Enterprise, Microsoft Visual Modeler for Visual Basic и др.),

поддерживающих множество языков программирования, таких, как C++, Java, Delphi, Power

Builder, Visual Basic, Centura, Forte, Ada, Smalltalk, а также позволяющих осуществлять

генерацию базы данных для большинства из существующих SQL-серверов. Модели,

разработанные в UML, позволяют значительно упростить процесс кодирования и направить

усилия программистов непосредственно на реализацию системы.

Диаграммы повышают сопровождаемость проекта и облегчают разработку

документации к программной системе. При модификации системы объектный подход

позволяет легко включать в систему новые объекты и исключать устаревшие без

существенного изменения ее жизнеспособности. Использование построенной модели при

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

поскольку они не ломают устоявшейся структуры системы, а только изменяют поведение

объектов.

КОМПОНЕНТНО-ОРИЕНТИРОВАННОЕ ПРОГРАММИРОВАНИЕ

Современные тенденции в развитии программных систем приводят к тому, что эти

системы должны становиться все более открытыми. При этом под открытостью понимается

не только независимость от технических и программных платформ, но также устойчивость и

способность удовлетворять постоянно растущие и меняющиеся требования к таким

системам.

Объектно-ориентированная технология разработки программного обеспечения

частично решает эти задачи, скрывая представление данных и реализацию деталей за

объектно-ориентированным интерфейсом и, таким образом, защищая пользователя от

необходимых изменений. Однако изменение в требованиях могут привести к ситуации, когда

изменятся взаимосвязи между объектами и их конфигурация. Таким образом, каждое

ИТНОП-2010

приложение можно рассматривать как экземпляр родового класса «Приложение», и каждый

из таких экземпляров строится из реконфигурируемых программных компонент. Понятие

компонента более общее, чем понятие объекта. В то время как объект инкапсулирует данные

и связанное с ними поведение, компонент может инкапсулировать некие полезные

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

абстракции – это объекты, однако в данном случае мы рассматриваем возможности гибкого

повторного использования программного кода, сфокусировавшись на объектах, при этом

открытое приложение будем рассматривать как композицию повторно используемых,

реконфигурируемых компонент.

Если попытаться ответить на вопрос, что такое компоненты и чем они отличаются от

объектов, необходимо различать два аспекта – методологический и технический. На

методологическом уровне компонент – это то, что было спроектировано для использования

вместе с другими компонентами. Компонент проектируется не изолированно, а как часть

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

абстрактная иерархия классов, или объектно-ориентированный язык, но если говорить в

общем виде, то примерами компонент могут служить процедуры, функции, макросы,

шаблоны, модули, а системой компонент – стандартизованные интерфейсы или

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

системе могут быть другие сущности, не обязательно программное обеспечение –

спецификации, документация, тестовые данные и т.д.

Если рассмотреть технический аспект компонентно-ориентированной разработки

программного обеспечения, то это очень старая идея, которая присутствует в самых ранних

работах по структурному программированию и модульности. Для языка программирования,

поддерживающего компонентно-ориентированную разработку, необходимо четко

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

может рассматриваться как вычислительная сущность, которая производит результат, а

также как конструкция программных компонентов, которые работают вместе для

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

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

полезные вычисления.

Таким образом, программные компоненты – это сущности, имеющие достаточно

длительный период жизни, они могут быть сохранены в программной базе независимо от

приложения, в котором предполагается их использование. При этом компоненты имеют

вполне определенные границы в программном обеспечении, куда они инкапсулированы, а

также четко определены пути взаимодействия с каждым компонентом (параметры, порты,

сообщения и т.д.). Создание программного обеспечения – это процесс конструирования

приложения из взаимосвязанных программных компонент. Появление компонентно-

ориентированной разработки программного обеспечения – это надстройка над объектно-

ориентированными техниками и методами для усиления и расширения инкапсуляции,

повторного использования кода, расширяемости объектов. Это смещает акценты от

программирования программных систем к их композиции.

ЛИТЕРАТУРА

1. Гради Буч. Объектно-ориентированный анализ и проектирование с примерами

приложений на С++, Бином, 1998 г.

2. Гради Буч, Джеймс Рамбо, Ивар Якобсон Язык UML. Руководство пользователя The

Unified Modeling Language: Users Guide, ДМК Пресс, 2007 г.

3. Oscar Nierstrasz and Dennis Tsichritzis (Ed.). Object-Oriented Software Composition, Prentice-

Hall, 1995.

http://scg.unibe.ch/archive/oosc/index.html

Амелина Ольга Викторовна

Орловский государственный технический университет, г. Орел

К.экон.н., доцент кафедры «Информационные системы»

Тел.: 89092298800

E-mail:

shu-shu-oa@yandex.ru

IV Международная научно-техническая конференция

УДК 681.3

В.А. БАШКИН

ГЛОБАЛЬНАЯ ВЕРИФИКАЦИЯ СВОЙСТВ ДОСТИЖИМОСТИ

СИСТЕМ С ОДНИМ НЕОГРАНИЧЕННЫМ РЕСУРСОМ

Рассматривается проблема формального доказательства свойств систем с бесконечным

числом состояний. Для систем с одним неограниченным ресурсом (односчетчиковых сетей Петри)

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

темпоральной логики EF (логики достижимости). Алгоритм основан на конструктивных

теоретико-числовых свойствах бесконечной части одномерных линейных и полулинейных множеств.

Ключевые слова: глобальная верификация моделей; темпоральная логика; односчетчиковые

сети; полулинейность; достижимость.

A problem of infinite model-checking is considered. An algorithm is presented for systems with one

unbounded resource (one-counter Petri nets), globally verifying an arbitrary property, written as EF

formula (where EF is temporal logic of reachability). The algorithm is based on constructive number-

theoretic properties of an infinite part of one-dimensional linear and semilinear sets.

Keywords: global model-checking; temporal logic; one-counter nets; semilinearity; reachability.

ВВЕДЕНИЕ

Проблема формального доказательства свойств систем.

При верификации систем с бесконечным числом состояний зачастую используют

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

выражения, грамматики, формулы арифметики Пресбургера). В данной работе

рассматривается однопериодическая форма задания значений счетчика в односчетчиковых

сетях (сетях Петри с не более чем одной неограниченной позицией). Предлагается алгоритм

глобальной верификации формулы темпоральной логики EF.

ФОРМАЛЬНОЕ ОПИСАНИЕ СВОЙСТВ

Темпоральная логика EF обладает следующим синтаксисом:

::= true | ¬

∧

| E〈a〉

| EF

Пусть LTS = (S, s

, →, L) – система помеченных переходов, где S – множество

состояний, s

∈ S – начальное состояние, → ⊆ S×S – отношение переходов (множество дуг),

L: (→) → Σ – помечающая функция (здесь и далее Σ – конечный алфавит меток

срабатываний).

Отношение выполнимости |= для состояния s системы LTS, темпоральной формулы

и метки a∈Σ определяется индуктивно:

s |= true;

s |= ¬

⇔ ¬(s |=

);

s |=

∧

⇔ s |=

∧ s |=

;

s |= E〈a〉

⇔ ∃ s' ∈ S : (s,s')∈(→) ∧ L(s,s')=a ∧ s' |=

;

s |= EF

⇔ для некоторого пути (s

,…), где s=s

, ∃ i

≥

1 : s

Стандартным образом определяются обычные логические связки (∨,⇒ и др.). Для

удобства записи формул обычно дополнительно определяют ещё и двойственные

темпоральные операторы: A〈a〉

= ¬E〈a〉¬

, AG

= ¬EF¬

Формула E〈a〉

означает «может сработать переход с меткой a, переводящий систему

в какое-то новое состояние, в котором выполняется формула

». Двойственная к ней

формула A〈a〉

означает «срабатывание любого перехода с меткой a переводит систему в

состояние, в котором выполняется формула

». Таким образом, оператор E формализует

понятие «существования», оператор A – понятие «неизбежности».

ИТНОП-2010

Формула EF

означает «s может сработать последовательность переходов,

переводящая систему в какое-то новое состояние, в котором выполняется формула

».

Двойственная к ней формула AG

означает «срабатывание любой последовательности

переходов переводит систему в состояние, в котором выполняется формула

».

Логика EF является расширением логики Хеннесси-Милнера и сужением логики

ветвящегося времени CTL. Она позволяет формализовать всевозможные свойства

достижимости, например:

• AG EF A〈a〉true – в системе всегда существует вероятность наступления события

«a» (точнее, из любого достижимого состояния достижимо состояние, при котором может

выполниться только переход «a»). Это свойство может служить признаком правильной

завершаемости процесса (если «a» – действие, возможное только в финальном состоянии).

• EF AG E〈a〉true – система может сработать таким образом, что в ней возникнет

единственный постоянно активный переход «a». Например, этот переход может

сигнализировать о возникновении переполнения памяти.

• AG (E〈a〉true ⇒ E〈b〉true) — событие «b» возможно только в таких состояниях

системы, в которых возможно событие «a». Например, подтверждение транзакции возможно

только тогда, когда возможен и её откат.

• A〈a〉 EF E〈b〉true – если возможно «a», то после его выполнения остается хотя бы

одна возможность когда-то в будущем выполнить «b». Например, в качестве «a» может

выступать событие принятия рискованного решения, в качестве «b» – событие получения

крупных дивидендов (другими словами, «риск не является бессмысленным»).

• AG A〈a〉 AG EF〈b〉true – если возможно «a», то после его выполнения рано или

поздно неизбежно наступает «b». Например, это может соответствовать правильности

написания параллельной программы (если «a» – событие распараллеливания, «b» – событие

синхронизации, то есть соединения распараллеленных ветвей вычисления).

• AG ((EF E〈a〉true) ∨ (E〈b〉true)) – всегда возможно либо возникновение в будущем

«a», либо прямо сейчас – «b». Например, «a» — это правильное завершение процесса, «b» —

предусмотренный аварийный выход.

Таким образом, темпоральная логика EF очень удобна в качестве языка описания

интересующих нас свойств систем. Разумеется, она не является универсальной (в частности,

не позволяет формализовать существование бесконечной последовательности срабатываний

одного и того же перехода), однако для большинства задач проверки свойств достижимости

вполне выразительна.

ФОРМАЛЬНОЕ МОДЕЛИРОВАНИЕ СИСТЕМ

Пусть Nat — множество неотрицательных целых чисел.

Односчетчиковой сетью называется набор N = (Q,T,L), где

• Q – конечное множество управляющих состояний,

• T⊂Q×Q×Z – конечное множество переходов,

• L:T→Σ – помечающая функция.

Состояние сети описывается парой (q,c), где q∈Q – текущее управляющее состояние,

c∈Nat — текущее значение счетчика.

Переход t=(q,q',z) активен в состоянии (q,c), если c+z>0.

Активный переход может сработать, переводя сеть в состояние (q',c+z)

(обозначается (q,c)

→

(q',c+z)). Изменение счетчика z также будем обозначать δ(t).

Внешний наблюдатель в момент срабатывания перехода t видит только его метку L(t)

(то есть он не может различить срабатывания переходов с одинаковой меткой).

Для конечной последовательности переходов U = t

…t

n-1

определим пред- и

постусловие (далее

⋅

обозначает усеченное вычитание до нуля):

•

U =

•

…t

n-1

) + |δ(t

)| при δ(t

)<0 и

•

…t

n-1

)

⋅

δ(t

) при δ(t

)≥ 0;

IV Международная научно-техническая конференция

•

= (t

…t

n-1

)

• ⋅

|δ(t

)| при δ(t

)<0 и U

•

=(t

…t

n-1

)

•

+δ(t

) при δ(t

)≥ 0.

Односчетчиковые сети эквивалентны сетям Петри с не более чем одной

неограниченной позицией.

Граф достижимости односчетчиковой сети с заданным начальным состоянием

представляет собой бесконечную (в общем случае) систему помеченных переходов.

Задача (локальной) верификации состоит в определении того, выполняется ли данная

формула темпоральной логики в данном состоянии.

Задача глобальной символьной верификации состоит в построении конечного

эффективного представления множества всех состояний, в которых выполняется данная

формула темпоральной логики.

Задача локальной верификации для счетчиковых сетей (и для более общего случая

счетчиковых машин) достаточно хорошо изучена ([4,6]). В частности, известно, что для

сетей с произвольным числом счетчиков задача верификации формул логики EF

неразрешима. Также известно [4], что для односчетчиковых сетей эта задача разрешима, хотя

и является P

–полной.

Для положительного решения более общей задачи глобальной символьной

верификации односчетчиковых сетей требуется наличие конечного символьного

представления для множества выполнимости произвольной формулы. Известно, что одно- и

двухсчетчиковые сети обладают полулинейным множеством достижимости [5], так что в

качестве такого представления естественно использовать периодичность значений счетчика.

ВЫЧИСЛЕНИЯ НАД БЕСКОНЕЧНЫМИ МНОЖЕСТВАМИ

С ИСПОЛЬЗОВАНИЕМ ОДНОПЕРИОДИЧЕСКИХ

ПОЛУЛИНЕЙНЫХ БАЗИСОВ

Для множества k–мерных векторов M⊆Nat

и вектора m∈Nat

определим операции

«сдвига вправо» и «сдвига влево»: M››m =

def

{m'+m | m'∈M}, M‹‹m =

def

{m'-m | m'∈M ∧ m'≥m}.

Множество m⊆Nat

называется линейным, если оно представимо в виде

m={v+n

+…+n

| n

,…,n

∈Nat}, где v,w

,…,w

∈Nat

— фиксированы.

Вектор v обычно называют базовым вектором линейного множества, вектора w

,…,w

– периодами.

Множество m⊆Nat

называется полулинейным, если оно является объединением

конечного числа линейных множеств.

Если M,M'⊆Nat

– полулинейные множества, то Nat

\M и M

∩

M' также являются

полулинейными [3]. Операции сдвига также сохраняют полулинейность. Известно, что

полулинейные множества – это в точности те множества, которые описываются

арифметикой Пресбургера.

Пусть x,y∈Nat. Через НОД(x,y) и НОК(x,y) обозначим наибольший общий делитель и

наименьшее общее кратное чисел x и y. В одномерном случае из линейности множества

следует его однопериодичность:

Лемма 1. [2] Пусть m⊆Nat – линейное множество, такое что m={v+n

∈Nat}, где v,w

∈Nat фиксированы. Тогда, обозначив p=НОД(w

) и

b=v+p(w

−

1)(w

−

1), имеем:

m=m

∪ m

∞

, где m

⊆{b−kp | k∈{1,2,…,(w

−

1)(w

−

1)}}, m

∞

={b+kp | k∈Nat}.

В доказательстве леммы используется теорема теории чисел ([1], задача 3.22) о том,

что для любых натуральных a, b и c, таких что a и b взаимно простые, а c≥(a

−

1)(b

−

1),

уравнение ax+by=c имеет натуральное решение.

Свойство единственности периода бесконечной части переносится и на произвольное

полулинейное множество:

Теорема 1. [2] Любое полулинейное множество m⊆Nat может быть представлено как

объединение конечного множества и конечного набора линейных однопериодических

ИТНОП-2010

множеств с одинаковым периодом: для некоторых p,b∈Nat существует характеристическое

множество Ψ⊆{b,b+1,b+2,…,b+(p

−

1)}, такое что

m = m

∪ m

∞

, где m

⊆

]/[

k =

(Ψ ‹‹ kp), m

∞

=0k

(Ψ ›› kp).

Рассмотрим двоичный вектор v длины p, такой что v[i]=0 для b+i∉Ψ и v[i]=1 для

b+i∈Ψ. Теорема утверждает, что этот вектор является «битовой маской» для периодического

«закрашивания» натурального ряда справа от числа b. Таким образом, мы можем

использовать в качестве конечного символьного представления произвольного

полулинейного одномерного множества m его однопериодический базис (m

,b,p,v),

состоящий из:

• конечного базового множества m

• базового элемента b,

• длины периода p,

• вектора периода v.

Данное представление проще формул арифметики Пресбургера, однако может быть

использовано только в одномерном случае.

Базис Z = (m

,b,p,v) полулинейного множества m⊆Nat называется минимальным, если

для любого базиса Z' = (m

',b',p',v') множества m выполняется p<p' или (p=p' и b≤b').

Известно [2], что минимальный базис существует и единственен; произвольный базис

может быть преобразован в минимальный за полиномиальное время (обозначим

соответствующий алгоритм как Mmz).

Минимальный базис множества m обозначим как Base(m); множество, определяемое

базисом Z, обозначим как Set(Z).

Для двоичных векторов v,v'∈{0,1}

через NOT(v), AND(v,v') и OR(v,v') обозначим

покомпонентное отрицание, умножение и сложение соответственно:

NOT(v)[i]=

def

(1-v[i]), AND(v,v')[i]=

def

min{v[i],v'[i]}, OR(v,v')[i]=

def

max{v[i],v'[i]}.

Через v

обозначим конкатенацию k векторов v.

Теоретико-множественные операции и отношения могут вычисляться

непосредственно над однопериодическими базисами:

Теорема 2. [2] Пусть m, m' ⊆ Nat – полулинейные множества, Base(m) = (m

,b,p,v),

Base(m') = (m

',b',p',v'), y∈Nat. Обозначим K=max{b,b'} и L=НОК(p,p'). Пусть K=b+ip=b'+jp'

для некоторых i,j∈Nat. Тогда:

1. Base(Nat)=(∅,0,1,(1));

2. Base(m∪m')=Mmz({x∈m∪m' | x<K},K,L,OR(v

L/p

,(v')

L/p'

));

3. Base(m∩m')=Mmz({x∈m∩m' | x<K},K,L,AND(v

L/p

,(v')

L/p'

));

4. Base(m\m')=Mmz({x∈m\m' | x<K},K,L,AND(v

L/p

,NOT((v')

L/p'

)));

5. m⊆m' ⇔ AND(v

L/p

, (v')

L/p'

)= v

L/p

∧ ∀x∈m (x<K ⇒ x∈m');

6. Base(m››y)=Mmz({x+y | x∈m

},b+y,p,v);

7. Base(m‹‹y)=Mmz({x-y | x∈m, x<B, x≥y},B,p,v), где B=min

{k∈Nat}

{b+kp

−

y | b+kp

−

y≥0}.

Все приведенные операции эффективны, то есть выполняются за полиномиальное

время относительно размеров входных базисов. Ограничение K=b+ip=b'+jp' носит

технический характер — оно позволяет записать формулы в более краткой форме.

Теорема 3. [2] Пусть m⊆Nat – полулинейное множество, представленное в

однопериодическом виде, x,y∈Nat. Пусть {A

(i)

} — последовательность полулинейных

множеств такая, что A

(0)

=m, A

(i+1)

=(A

(i)

‹‹ x) ›› y. Тогда найдется:

j≤max{[b/(|x

−

y|)], НОК(p,|x

−

y|)}+1 такое, что

∞

=1i

(i)

i 1=

(i)

Эта теорема показывает важное свойство одномерных полулинейных множеств:

конечно определенная аддитивная последовательность всегда стабилизируется за конечное

IV Международная научно-техническая конференция

число шагов. Свойство стабилизации приводится уже в [5], но только для прибавления

ресурса (сдвига вправо) и без оценки достаточного числа шагов.

ФОРМАЛЬНОЕ ДОКАЗАТЕЛЬСТВО СВОЙСТВ СИСТЕМ

Использование операций над базисами и представления в однопериодическом виде

позволяет строить полное символьное дерево достижимости односчетчиковой сети. Узлами

этого дерева являются пары вида (q|Z), где q – управляющее состояние, Z – базис

полулинейного множества возможных значений счетчика.

Алгоритм 1. (символьное дерево достижимости)

1. Корень: (q

|Base(c

)), пометим узел как «новый».

2. Пока есть «новые» узлы, для такого узла (q|Z) выполним:

2.1. Если ∀t=(q,q',z)∈T выполняется z<0 и (Set(m) ‹‹ |z|)=∅), пометим узел как «тупик».

2.2. Если (q|Set(Z))⊆(q|Reach(q)), где Reach(q) — объединение всех уже вычисленных

значений счетчика для q, то пометим узел как «старый».

2.3. Если на пути от корня найдется (q|Z') с Set(Z')⊂Set(Z), то срабатывание

последовательности (q|Z')

→

(q|Z) – цикл, увеличивающий счетчик. Заменим (q|Z) на (q|Z

∞

где Z

(0)

= Z, Z

(i+1)

= Base(Set(Z

(i)

) ∪ ((Set(Z

(i)

) ‹‹

•

U) ›› U

•

)).

2.4. Иначе пометим (q|Z) как «старый» и для любого активного перехода t=(q,q',z)

добавим «новый» узел (q'|Z'), где Z' = Base(Set(Z) ‹‹ |z|) при z<0 и Z' = Base(Set(Z) ›› z) при z≥0.

Сходимость алгоритма основана на свойстве стабилизации (теорема 3), а также на том

факте, что односчетчиковые сети являются плоскими системами [7], то есть системами, в

которых отношение достижимости исчерпывается простыми (невложенными) циклами.

Используя символьное дерево достижимости, мы можем решать глобальную

проблему верификации формул темпоральной логики EF.

Обозначим как Res(q,

) множество значений счетчика, при которых формула

выполняется в управляющем состоянии q. Значение Res(q,

) может быть вычислено

индуктивно по структуре формулы

Алгоритм 2. (глобальная верификация)

• Res(q,true) = Nat

• Res(q,¬

) = Nat \ Res(q,

)

• Res(q,

∧

) = Res(q,

) ∩ Res(q,

)

• Res(q,E〈a〉

) =

(q|Z)

→

(q'|Z') : L(t)=a

((Res(q',

) ∩ Set(Z')) ‹‹ t

•

) ››

•

• Res(q,EF

) =

(q|Z)

→

(q'|Z')

(((Res(q',

) ∩ Set(Z')) ‹‹ U

•

) ››

•

В определении алгоритма запись «(q|Z)

→

(q'|Z')» означает «для всех Z,t,q',Z' таких,

что в символьном дереве достижимости есть дуга t, соединяющая узлы (q|Z) и (q'|Z')»; запись

«(q|Z)

→

(q'|Z')» означает «для всех Z,U,q',Z' таких, что в символьном дереве достижимости

есть цепочка дуг U, соединяющая узлы (q|Z) и (q'|Z')».

ЗАКЛЮЧЕНИЕ

Представленные способы преобразования систем и анализа их свойств корректны с

точки зрения наблюдаемого поведения (в смысле бисимуляции состояний). Их можно

применять для любых систем с ресурсами, построенных на основе обыкновенных сетей

Петри.

ЛИТЕРАТУРА

1. Гашков С.Б., Чубариков В.Н. Арифметика. Алгоритмы. Сложность вычислений. – М.,

Высшая школа, 2000. – 320 с.

2. Bashkin V.A. On the single-periodic representation of reachability in one-counter nets. // Proc.

of CS&P'2009. Warsaw. – 2009. – P.60-71.