авторефераты диссертаций БЕСПЛАТНАЯ БИБЛИОТЕКА РОССИИ

КОНФЕРЕНЦИИ, КНИГИ, ПОСОБИЯ, НАУЧНЫЕ ИЗДАНИЯ

<< ГЛАВНАЯ
АГРОИНЖЕНЕРИЯ
АСТРОНОМИЯ
БЕЗОПАСНОСТЬ
БИОЛОГИЯ
ЗЕМЛЯ
ИНФОРМАТИКА
ИСКУССТВОВЕДЕНИЕ
ИСТОРИЯ
КУЛЬТУРОЛОГИЯ
МАШИНОСТРОЕНИЕ
МЕДИЦИНА
МЕТАЛЛУРГИЯ
МЕХАНИКА
ПЕДАГОГИКА
ПОЛИТИКА
ПРИБОРОСТРОЕНИЕ
ПРОДОВОЛЬСТВИЕ
ПСИХОЛОГИЯ
РАДИОТЕХНИКА
СЕЛЬСКОЕ ХОЗЯЙСТВО
СОЦИОЛОГИЯ
СТРОИТЕЛЬСТВО
ТЕХНИЧЕСКИЕ НАУКИ
ТРАНСПОРТ
ФАРМАЦЕВТИКА
ФИЗИКА
ФИЗИОЛОГИЯ
ФИЛОЛОГИЯ
ФИЛОСОФИЯ
ХИМИЯ
ЭКОНОМИКА
ЭЛЕКТРОТЕХНИКА
ЭНЕРГЕТИКА
ЮРИСПРУДЕНЦИЯ
ЯЗЫКОЗНАНИЕ
РАЗНОЕ
КОНТАКТЫ


Pages:   || 2 | 3 | 4 | 5 |
-- [ Страница 1 ] --

МИНИСТЕРСТВО ОБРАЗОВАНИЯ И НАУКИ

РОССИЙСКОЙ ФЕДЕРАЦИИ

ГОСУДАРСТВЕННЫЙ НАУЧНО-ИССЛЕДОВАТЕЛЬСКИЙ ИНСТИТУТ

ИНФОРМАЦИОННЫХ ТЕХНОЛОГИЙ И ТЕЛЕКОММУНИКАЦИЙ

МЕЖДУНАРОДНАЯ АКАДЕМИЯ ИНФОРМАТИЗАЦИИ

АКАДЕМИЯ ИНФОРМАТИЗАЦИИ ОБРАЗОВАНИЯ

ФОНД СОДЕЙСТВИЯ РАЗВИТИЮ МАЛЫХ ФОРМ ПРЕДПРИЯТИЙ

В НАУЧНО-ТЕХНИЧЕСКОЙ СФЕРЕ

НАУЧНО-ТЕХНИЧЕСКОЕ ПРЕДПРИЯТИЕ «КРИПТОСОФТ»

ПЕНЗЕНСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ

НОВЫЕ ИНФОРМАЦИОННЫЕ ТЕХНОЛОГИИ И СИСТЕМЫ ТРУДЫ IX Международной научно-технической конференции Часть 2 Proceedings of the Ninth International Conference of Science and Technology NEW INFORMATION TECHNOLOGIES AND SYSTEMS Penza, Russia, November 9–10, 2010 Volume 2 Пенза Издательство ПГУ УДК 004. Н Новые информационные технологии и системы : труды Н72 IX Международной научно-технической конференции (г. Пенза, 9–10 ноября 2010 г.) : в 2 ч. – Пенза : Изд-во ПГУ, 2010. – Ч. 2. – 220 с.

Представлены материалы докладов, сделанных на IX Международной научно технической конференции «Новые информационные технологии и системы»

(«НИТиС-2010»), проводимой Международной академией информатизации, Акаде мией информатизации образования, научно-техническим предприятием «Крипто софт» и Пензенским государственным университетом.

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

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

УДК 004. Редакционная коллегия:

В. И. Волчихин, Н. П. Вашкевич, В. Ю. Егоров, М. М. Бутаев, П. П. Макарычев, Х.-М. Ханиш © ГОУ ВПО «Пензенский государственный университет», «НИТиС-2010»

МОДЕЛИРОВАНИЕ ИНФОРМАЦИОННО-ВЫЧИСЛИТЕЛЬНЫХ СИСТЕМ В.С. Князьков1, М.М. Бутаев Россия, Вятка, Вятский Государственный Университет, Россия, Пенза, Пензенский государственный университет МОДЕЛИРОВАНИЕ ВЫЧИСЛЕНИЙ В ОСТАТОЧНЫХ КЛАССАХ В КЛАСТЕРНОЙ СРЕДЕ В настоящее время уделяется большое внимание применения методов прогнозного компьютерного моделирования для широко го спектра индустриальных и научных проектов. К таким задачам, например, относятся: задачи компьютерного моделирования раз личных летательных аппаратов, автомобилей, судов, инженерных конструкций;

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

задачи, решаемые в области ядерной физики, аэродинамики, фи зической газодинамики, гидро- и электродинамики;

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

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

Традиционно для решения подобных задач использовались и используются промышленные CAD-, CAE-системы и программ ные комплексы специального назначения (в подавляющем боль шинстве зарубежного производства).

Анализ предметной области показывает, что используемые в современных инженерных CAD-системах и программных ком плексах математические методы и их алгоритмически программные решения задач аэро-гидродинамики разрабатыва лись для вычислительных систем с ограниченным количеством вычислительных модулей. Адаптация этих методов, алгоритмов и их программных решений даже на 1000-ядерные вычислительные системы является весьма сложной и в ряде случаев невыполнимой задачей.

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

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

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





Следующей особенностью предметной области исследований и вытекающая из этого проблемой является то, что современные действующие и проектируемые многопроцессорные супер-ЭВМ и «НИТиС-2010»

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

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

Новизна предлагаемого подхода к конструированию методов, алгоритмов и программ для выполнения высокоскоростных мас штабируемых численных расчетов повышенной точности в среде распределенных гетерогенных вычислительных систем заключа ется в использовании при вычислениях специальных базисов мо дулярной арифметики – систем счисления в остаточных классах (СОК – также полиномиальная система классов вычетов), в кото рых числа представляются наборами остатков от деления на вы бранные модули (основания). В этом случае i-й разряд числа представляет собой наименьший положительный остаток от деле ния на i-ое основание СОК самого числа, а не предыдущего част ного, как это имеет место в позиционной системе. Причем, оста ток деления меньше делителя, и поэтому, если в качестве оснований полиномиальной системы выбрать числа, не выходя щие за пределы разрядной сетки ЭВМ, то и остатки от деления на эти основания, не будут выходить за пределы разрядной сетки.

IX Международная научно-техническая конференция Ранее задача использования систем счисления в остаточных клас сах для организации численных расчетов на мультипроцессорных и многоядерных платформах универсального назначения не ре шалась.

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

В отличие от ПСС, где посредством языков программирования заложена фиксированная градация типов числовых данных (на пример Byte, Int32, Int64 и т.д.), система остаточных классов мо жет быть настроена на конкретную разрядность чисел. Данная настройка может быть выполнена путем выбора оптимальных для работы с конкретными числовыми данными оснований СОК. Оп тимальными в являются взаимно-простые основания, произведе ние которых (а, следовательно, и верхний предел диапазона пред ставления числовых данных) максимально приближено к конкретной разрядности обрабатываемых чисел. С другой сторо ны, оптимальными для использования полиномиальной системы на универсальных процессорах, основанных на двоичной арифме тике, являются числа вида «2n-1», где число n не выходит за пре делы разрядной сетки процессора. Причем, если основания имеют одинаковую разрядность, то при параллельной обработке масси вов данных на многоядерных процессорах мультипроцессорной системы удастся достигнуть наиболее сбалансированной полезной загрузки всех ядер.

На кластере Вятского Государственного Университета ENIGMA (HP Hewlett-Packard Cluster Platform 3000 BL460c, Intel Xeon 5345 2.33GHz, Infiniband) были проведены следующее моде лирование:

– исследование влияния числа элементов массивов данных на время решения задачи;

«НИТиС-2010»

– исследование влияния разрядности числовых данных на время решения задачи;

– исследование эффективности применения грубой ап проксимации оснований СОК вида «2n-1» вокруг диапазона представления числовых данных;

– исследование эффективности применения сглажен ной аппроксимации оснований СОК вокруг диапазо на представления числовых данных.

Решалась задача сложения двух двумерных массивов, размер ностью 4000x8000 элементов. Сводный график по результатам экспериментов представлен на рисунке 1.

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

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

Таким образом, при выполнении вычислений в базисе четырех модульной полиномиальной системы каждое ядро процессора производит вычисления над фрагментами «своих» массивов дан ных, которые определяются соответствующим основанием данной системы. В результате этого, полная эффективная загрузка всех ядер вычислительного узла наблюдается при запуске двух парал лельных процессов, каждый из которых, в свою очередь, создает четыре параллельных потока, выполняющихся на соответствую IX Международная научно-техническая конференция щих ядрах процессора (согласно определению параллелизма на уровне разрядов чисел).

Рисунок 1. Результаты экспериментов по исследованию эффектив ности применения полиномиальной системы.

Из результатов экспериментов вытекает, что если число осно ваний полиномиальной системы совпадает с числом ядер процес соров вычислительного узла, то каждое ядро будет производить работу с фрагментами массивов данных только по соответствую щему ему основанию. Отсюда обеспечивается поддержка SIMD (Single Instruction Multiple Data) модели вычислений.

При создании программных решений использованы две техно логии параллельного программирования: MPI – для реализации параллелизма на уровне элементов данных и OpenMP – для реали зации параллелизма на уровне разрядов чисел при выполнении вычислений в системе остаточных классов.

По результатам моделирования можно судить о потенциальной эффективности использования системы остаточных классов и о возможности их использованию в качестве базиса для выполнения высокоточных параллельных численных расчетов на современных высокопроизводительных ВС с кластерной архитектурой. При «НИТиС-2010»

таком подходе обеспечивается:

Рисунок 2. Влияние числа параллельных процессов на количество одновременно используемых ядер вычислительного узла.

Во-первых, расширение диапазона представления исходных данных при сохранении высокой точности вычислений на боль ших массивах чисел с повышенной разрядностью.

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

В-третьих, обеспечивается высокая масштабируемость про граммных решений и соответственно повышается скорость реше ния задач.

В.Н. Дубинин Россия, Пенза, Пензенский государственный университет СИСТЕМА ИМИТАЦИОННОГО МОДЕЛИРОВАНИЯ РАСПРЕДЕЛЕННЫХ СИСТЕМ ПРОМЫШЛЕННОЙ АВТОМАТИКИ НА ОСНОВЕ ФУНКЦИОНАЛЬНЫХ БЛОКОВ Рассматриваются принципы построения интерпрета тора функциональных блоков международного стан дарта IEC 61499 для оценки производительности и IX Международная научно-техническая конференция качества функционирования распределенных компо нентно-базированных систем промышленной авто матики (РКБСПА).

1. Введение Распределенные компонентно-базированные системы про мышленной автоматики (РКБСПА) являются одним из основных направлений развития средств автоматизации современного про мышленного производства [1]. Принятый в 2005 году междуна родный стандарт IEC 61499 [2] определяет путь для создания сис тем управления нового поколения для РКБСПА [3]. Это интеллектуальные реконфигурируемые распределенные компо нентно-базированные системы на основе функциональных блоков (ФБ). В настоящее время в мире существует несколько компаний и университетов, активно занимающихся созданием соответст вующей инфраструктуры для внедрения стандарта IEC 61499 в инженерную практику, к числу которых относятся Holobloc Inc.

(США), Yamatake Corporation (Япония), Окленский университет (Новая Зеландия), Венский технологический университет, фирмы PROFACTOR GmbH и nxtControl GmbH (Австрия), Патрасский университет (Греция), Миланский политехнический университет (Италия), университеты Халле, Магдебурга, Кайзерcлаутерна и Ганновера (Германия), Тамперский технологический университет (Финляндия), технологический университет Chalmers (Швеция), университет Калгари, фирма O3NEIDA Inc. (Канада), а также ряд других компаний и университетов.

В целом проектирование РКБСПА включает фазы, являющиеся традиционными при проектировании сложных программно аппаратных систем, а именно: спецификацию, верификацию, оценку производительности, синтез, оптимизацию и реализацию.

Широкое распространение стандарта IEC 61499 и разработка сис тем управления на его основе сдерживается недостатком методов и соответствующих инструментальных средств поддержки проек тирования. На данный момент известны следующие некоммерче ские системы, ориентированные на проектирование распределен ных систем управления на основе ФБ IEC 61499: 1) FBDK/FBRT от фирмы Holobloc Inc. [4];

2) CORFU-FBDK, разработанная в «НИТиС-2010»

Патрасском 2. Основные сведения Особенностями предлагаемой СИМФБ являются: 1) однотип ное унифицированное представление систем управления и моде лей промышленных процессов в форме ФБ (возможность данного подхода была, например, продемонстрирована в [10];

2) использо вание событийного подхода к моделированию, причем для изме нения модельного времени используются переменные интервалы [11].

Система СИМФБ включает в себя интерпретатор ФБ, являю щийся ее основой, а также ряд дополнительных модулей, в число которых входят модуль для обработки статистических данных, модуль для построения временных диаграмм состояний, модуль для построения и анализа графа достигнутых состояний (ГДС), модуль для анализа трасс событий, модуль для оценки качества функционирования системы в целом, а также ряд других сервис ных модулей.

Входные и выходные данные интерпретатора ФБ, а также его связи с окружающей средой представлены на рисунке 1. Входны ми данными СИМФБ являются описания ФБ на языке XML в со ответствии со стандартом IEC 61499 (часть 2) [12], а также трассы входных событий, которые могут и отсутствовать ввиду возмож ности наличия генераторов событий в виде ФБ внутри модели руемой системы. Следует заметить, что представление ФБ на язы ке XML может быть получено, например, с помощью редактора ФБ, входящего в состав FBDK.

В ходе работы интерпретатора ФБ собирается статистика об элементах модели (число входов в заданное состояние, среднее время нахождения системы в заданном состоянии, относительное время нахождения в заданном состоянии, число сработавших пе реходов из одного состояния в другое), что позволяет оценить производительность и качество функционирования моделируемой системы.

IX Международная научно-техническая конференция Сеть Статистика Трассы Временные входных диаграммы событий Интерпретатор ФБ Граф дос тигнутых XML состояний представления ФБ Трассы выходных событий Рисунок 1. Входные и выходные данные интерпретатора ФБ.

Для представления истории функционирования модели имеет ся возможность построения: а) графа достигнутых состояний, включающего множество достигнутых состояний и множество переходов между этими состояниями;

б) трасс событий, относя щихся к одному ФБ, группе ФБ или всей системе в целом. Для возможности масштабирования пространства состояний предла гается конструирование структуры состояния путем включения в него интересующих исследователя координат. Историческая ин формация может использоваться для анализа корректности пове дения системы, недоступного на основе анализа статистических данных. После интерпретации возможен масштабируемый вывод временных диаграмм для заданных состояний, дающих дополни тельную возможность для визуальной проверки корректности функционирования системы.

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

При построении модели допускается использовать два типа ФБ «НИТиС-2010»

– базисный и составной. В базисном функциональном блоке (ФБл) имеется возможность явного задания длительности выпол нения алгоритмов, что полезно при моделировании систем реаль ного времени. Для этих целей в алгоритмах используется предо пределенная переменная time.

3. Объектная модель При разработке СИМФБ был использован объектно ориентированный подход, являющийся в настоящее время стан дартом при проектировании программного обеспечения. Цен тральной частью объектной модели интерпретатора ФБ является объектная модель ФБ. При ее разработке использовались: а) объ ектная модель для классов, которые могут быть использованы в системах поддержки проектирования, определенная в приложении C стандарта IEC 61499 [2];

б) объектная модель ФБ, ориентиро ванная на ее дальнейшую реализацию с использованием языков программирования (например, С++ или Java). Предложенная объектная модель ФБ имеет ряд общих черт с моделью, рассмот ренной в [13], но в целом является оригинальной. На рисунке приведена диаграмма (основных) классов интерпретатора ФБ.

Рисунок 2. Диаграмма классов интерпретатора ФБ.

В основе интерпретатора лежит класс FBManger, который про изводит инициализацию и управляет загрузкой и выгрузкой функциональных блоков. В класс ParserFB инкапсюлированы ал горитмы разбора исходных XML-файлов и формирования ФБ во внутреннем формате интерпретатора. Класс SystemContext реали IX Международная научно-техническая конференция зует механизмы сбора статистики и координации выполнения всех ФБ в системе. Экземпляр класса SystemContext является об щим для всех экземпляров ФБ в системе. Классы Statistic1 и Statis tic2 реализуют сбор статистики о состояниях и переходах базис ных ФБ, соответственно. Перечень классов объектной модели ФБ представлен в следующей таблице.

Класс Элемент ФБ Интерфейс ФБ InterfaceFB Переменная ФБ Var Буфер данных Buffer WITH-связи WithConnections Базисный ФБ BasicFB Входные событийные пере Event менные Состояния диаграммы ЕСС States Переходы диаграммы ЕСС Transitions Интерпретатор условий пе CondInterpreter рехода Интерпретатор алгоритмов AlgInterpreter Составной ФБ CompositeFB Хранилище внутренних ContainerFB блоков составного ФБ Событийные и информаци EventDataConnections онные связи внутри состав ного ФБ 4. Режимы и функционирование СИМФБ СИМФБ работает в двух режимах: автоматической и пошаго вой интерпретации. В режиме автоматической интерпретации за дается лимит времени моделирования или лимит числа срабаты ваний переходов диаграмм ECC и процесс имитации происходит без необходимости взаимодействия с пользователем. Однако пользователь может управлять процессом интерпретации, а имен но его останавливать и возобновлять, просматривать статистику и изменять некоторые входные параметры модели. В режиме поша говой интерпретации работа производится по шагам. После вы «НИТиС-2010»

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

Известно, что из-за неполного определения семантики ФБ в стандарте IEC 61499 допускаются различные реализационные мо дели выполнения ФБ [14,15]. Это относится и к СИМФБ, в кото рой некоторые элементы выполнения ФБ реализуются средствами операционной системы (ОС) Windows. В СИМФБ используется параллельное выполнение ФБ в отдельных потоках (с собствен ным управлением). Обмен событиями (сигналами) между ФБ мо жет производиться с использованием: а) очереди единичной емко сти (как в стандарте IEC 61499), б) очереди бесконечной емкости, что определяется опциями интерпретатора. Взаимодействие ФБ в СИМФБ осуществляется путем записи и чтения входных собы тийных переменных из очередей. Для исключения коллизий ис пользуются критические секции. Зацикливания при опросе очере дей исключаются путем перевода потоков в “спящий” режим.

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

Алгоритм выполнения базисного ФБл можно разделить на не сколько этапов: 1) создание потока, в котором будет выполняться ФБл;

2) получение входного события;

3) копирование перемен ных, связанных с этим событием из буфера данных;

4) определе ние множества разрешенных переходов;

5) выбор и выполнение перехода ECC. Шаги 4 и 5 выполняются до тех пор, пока не оста нется разрешенных переходов. Для планирования событий в СИМФБ используется список будущих событий [16]. По приве денной в статье [14] классификации моделей реализации ФБ рас смотренный интерпретатор ФБ можно отнести к типу “А3”.

5. Встроенные функциональные блоки В интерпретатор включены специальные типы сервисных ин IX Международная научно-техническая конференция терфейсных ФБ, предназначенных для организации моделирова ния и повышения функциональности системы. Блок временной задержки (рисунок 3) имеет следующие событийные входы:

START - запуск таймера;

STOP – сброс таймера, а также событий ные выходы EO и STOPPED – естественное и принудительное окончание временной задержки, соответственно. Информацион ный вход DT задает значение задержки, а выход REST – остаточ ное время.

Рисунок 3. Блок временной задержки.

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

Вывод информации осуществляется в определенную форму при приходе в ФБ входного события. Коммуникационные блоки ана логичны соответствующим блокам, реализованным в FBDK. Они выполняют пересылку сообщений по сети с использованием про токолов TCP и UDP.

6. Примеры моделирования Ниже представлены два примера моделирования. В качестве первого примера рассматривается имитационная модель для ис следования работы выталкивателя (рисунок4), представляющего некоторое мехатронное устройство [10].

Данная модель включает следующие блоки: F1:RESTART стартовый блок, F2:GEN - генератор заявок, F3:SGV2 – выталки ватель (на втором уровне), F4:EXPON - генератор случайных чи сел, распределенных по экспоненциальному закону, F5:DELAY «НИТиС-2010»

блок задержки. Блок SGV2 состоит в свою очередь из блока вы талкивателя (первого уровня) SGV1, включающего две временные задержки DELAY, и блока управления выталкивателем SGV1_CTL.

Модель функционирует циклически следующим образом: генери руется запрос, выполняемый в течение определенного время вы талкивателем, после чего следует временная задержка и выдается новый запрос. Основная статистика определяется по базисным ФБ GEN и SGV1_CTL.

Рисунок 4. Модель для исследования работы выталкивателя.

В качестве второго примера рассматривается разомкнутая од ноканальная система массового обслуживания (СМО), например, M/M/1 [17]. Модель данной системы включает генератор заявок, очередь и обслуживающий прибор. Блок очереди (QUEUE), пред назначенный для сбора статистических данных и управления оче редью (точнее, для управления загрузкой заявки из очереди в об служивающий прибор), представлен на рисунках 5-6.

Рисунок 5. Интерфейс блока управления очередью.

Для включения и исключения заявки из системы “оче редь+прибор” используются входы to_que и from_que, соответст венно. Они являются аналогами операторов QUEUE и DEPART языка имитационного моделирования GPSS [16].

IX Международная научно-техническая конференция Рисунок 6. Диаграмма ЕСС блока QUEUE.

Событие на выходе req появляется, когда обслуживающий прибор пуст и готов к обслуживанию новой заявки. Переменная Len определяет текущую длину очереди (без учета обслуживаю щего прибора). Алгоритмы AlgLenInc и AlgLenDec увеличивают и уменьшают на 1, а алгоритмы AlgLen0 и AlgLen1 устанавливают значение переменной Len в 0 и 1, соответственно. Состояния ЕСС определяют в основном число заявок в СМО, например, состояние s2 определяет две заявки, одна из которых в обслуживающем приборе, а вторая – в очереди к нему. Для повышения представи тельности и детальности статистики число состояний в приведен ной ЕСС должно быть определенным образом увеличено.

7. Реализация прототипа Программный прототип СИМФБ включает на данный момент только интерпретатор ФБ. Ограничениями прототипа является использование дискретного времени и целочисленных, булевых и строковых переменных. Система реализована на языке C++ в среде разработки Microsoft Visual Studio. Структуры данных, ис пользуемые в прототипе, основаны на контейнерах стандартной библиотеки шаблонов STL. Для обработки XML-файлов использо вана библиотека классов TinyXml [18]. Для выполнения алгорит мов, связанных с состояниями ЕСС, используется интерпретатор языка Бейсик. Интерфейс пользователя реализован с использова нием функций Windows API.

Заключение В данной работе была предложена проблемно ориентированная система имитационного моделирования СИМФБ, предназначенная для использования при проектирова нии РКБСПА. На примере было показано, что данный интерпре татор можно использовать и как общецелевую систему имитаци онного моделирования. Направлением дальнейших исследований «НИТиС-2010»

является разработка библиотеки встроенных ФБ, повышающих функциональность системы.

Список литературы 1. Tomilla Т., Venta О., Koskinen К. Next generation industrial automation – needs and opportunities // Automation Technology Review. - 2001. - P. 34-41.

2. Function blocks for industrial-process measurement and control systems - Part 1: Architecture, International Electrotechnical Commission, Geneva, 2005.

3. Chouinard J., Brennan R. Software for Next Generation Automa tion and Control // IEEE International Conference on Industrial In formatics (INDIN'2006), Singapore, 2006. - P. 886 – 891.

4. FBDK - Function Block Development Kit [Электронный ресурс]. –http://holobloc.com.

5. CORFU Engineering Support System [Электронный ресурс]. – http://seg.ee.upatras.gr/corgu/dev/index.htm.

6. FBench [Электронный ресурс]. – http://oooneida fbench.sourceforge.net/.

7. 4DIAC - Framework for Distributed Industrial Automation and Control [Электронный ресурс]. – http://www.fordiac.org.

8. nxtControl [Электронный ресурс]. – http://www.nxtcontrol.com.

9. ICS Triplex ISaGRAF Workbench for IEC 61499/ 61131 [Элек тронный ресурс]. –http://www.icstriplex.com/.

10. Дубинин В.Н., Дубравин А.А., Черемушкин В.В., Вяткин В.В.

Разработка визуальных имитационных моделей производст венных систем на основе UML и функциональных блоков // Труды VI Международной научно-технической конференции “Новые информационные технологии и системы (НИТС’2004)”, Пенза, 2004, часть 2. - C. 68-76.

11. Максимей И.В. Имитационное моделирование на ЭВМ. – М.:

Радио и связь, 1988. – 232 с.

IX Международная научно-техническая конференция 12. Function blocks for industrial-process measurement and control systems - Part 2: Software tool requirements, International Elec trotechnical Commission, Geneva, 2005.

13. Thramboulidis K., Doukas G., Frantzis A. Towards an Implemen tation Model for FB-based Reconfigurable Distributed Control Applications // 7th IEEE International Symposium on Object oriented Real-time distributed Computing (ISORC 2004), Vienna, Austria, 2004.

14. Ferrarini L., Veber C. Implementation approaches for the execu tion model of IEC 61499 applications // 2nd IEEE Int. Conference on Industrial Informatics (INDIN’04), Berlin, 2004. - P. 612-617.

15. Дубинин В.Н., Вяткин В.В. Разработка интегрированной па раметризованной модели выполнения функциональных бло ков IEC 61499 с использованием морфологических методов // Сб. статей Международной научно-технической конференции “Современные информационные технологии- 2008”, Весенняя сессия, Пенза, 2008. – C. 146-154.

16. Шрайбер Т. Дж. Моделирование на GPSS. – М.: Машино строение, 1980. – 592 с.

17. Клейнрок Л. Теория массового обслуживания - М.: Машино строение, 1979.

18. TinyXML [Электронный ресурс]. – http://www.grinninglizard.com/tinyxml/.

В.Н. Дубинин1, Х.-М. Ханиш2, В.В. Вяткин3, С.К. Шестаков Россия, Пенза, Пензенский государственный университет Германия, Халле, университет Мартина Лютера Новая Зеландия, Окленд, университет Окленда АНАЛИЗ РАСШИРЕННЫХ NCES-СЕТЕЙ НА ОСНОВЕ МЕТОДА MODEL CHECKING В статье предлагается подход к исследованию рас ширенных NCES-сетей, включая NCES-сети с инги биторными дугами и арифметические NCES-сети, на основе метода Model Checking с использованием хо рошо известного верификатора SMV. Рассматрива «НИТиС-2010»

ется набор правил для преобразования NCES-сетей в промежуточную асинхронную модель (А-модель), а также методика кодирования А-модели на входном языке SMV. Освещены вопросы валидации метода асинхронного моделирования NCES-сетей. Предло женный метод анализа NCES-сетей демонстрируется на ряде примеров.

1. Введение Формализм NCES-сетей был введен в 1995 г. в работе [1].

NCES-сети представляют собой сети Петри, расширенные собы тийными сигналами (дугами) и особым порядком срабатывания переходов. В сетях данного класса принято синхронное срабаты вание группы переходов, называемой шагом. В то же время сраба тывание шагов в рамках всей сети является асинхронным. Форми рование шага основано на достижимости переходов по событийным дугам из перехода – источника сигнала. Этот пере ход называется триггерным и аналогичен переходам обычных се тей Петри. Синхронное срабатывание переходов в шаге определя ет мгновенность передачи сигналов по событийным дугам. Это позволяет моделировать с помощью NCES-сетей как импульсные сигналы, так и сигналы в виде потенциала. Синхронно асинхронный характер NCES-сетей позволяет представлять с их помощью широкий спектр параллельных процессов. В дальней шем формализм NCES-сетей был расширен в направлении мо дульности и представления времени [2]. Ряд модификаций, ка сающихся функционирования NCES-сетей, был реализован в системе ViVe [3]. В работе [4] были предложены арифметические NCES-сети, позволяющие выполнять арифметическую обработку данных.

NCES-сети нашли широкое распространение в моделировании дискретно-событийных систем, особенно в сфере промышленной автоматики. Исследования в области NCES-сетей, связанные с их развитием и применением, а также разработкой инструменталь ных средств, проводятся в ряде университетов, в числе которых университет Мартина Лютера, Магдебургский университет и уни верситет Гумбольта (Германия), Оклендский университет (Новая IX Международная научно-техническая конференция Зеландия), Тамперский технологический университет (Финлян дия), Венский технологический университет (Австрия), государ ственный университет Нью-Джерси (США), Пензенский государ ственный университет (Россия), Софийский университет химической технологии и металлургии (Болгария), федеральный университет Санта Катарины (Бразилия).

Существует ряд инструментальных систем, позволяющих ана лизировать NCES-сети, в числе которых Sesa [5], Vive [6], TNCES Workbench [7]. Первые две системы поддерживают анализ NCES сетей, в том числе с временными задержками. Использование ин гибиторных дуг исключается. В системе Sesa реализован анализ сетевых моделей на основе метода Model Checking. Система ViVe предлагает развитый графический пользовательский интерфейс.

Следует отметить, что Sesa включена в состав ViVe. Система TNCES-Workbench, реализованная на языке SWI-Prolog [8], в от личие от Sesa и ViVe, работает с временными NCES-сетями, в ко торых допускаются также ингибиторные дуги. Данная система позволяет вычислять граф достижимости и анализировать его в дальнейшем с использованием формул временной логики, но практическое применение интерпретатора формул временной ло гики в случае графа достижимости большой размерности пробле матично вследствие невысокой скорости выполнения Пролог программ.

Результативным методом анализа моделей с конечным, воз можно очень большим, числом состояний (к каким относятся при определенных условиях и NCES-сети) является метод Model Checking [9]. Данный метод позволяет проектировщику опреде лить, удовлетворяет ли модель системы определенным требуемым свойствам. Как правило, в этой технике верификации использует ся алгоритм проверки формул временных логик LTL и CTL [10].

Инструментальные средства, поддерживающие Model Checking, позволяют анализировать системы с большим числом состояний благодаря сжатому представлению пространства состояний, осно ванному на упорядоченных двоичных решающих диаграммах (OBDD). При этом возможно верифицировать некоторые системы, которые имеют более чем 1020 состояний. Различные модифика «НИТиС-2010»

ции методов, основанных на OBDD, могут расширить число со стояний до 10120 и более [11].

Следует обратить внимание на определенные проблемы, свя занные с реализацией метода Model Checking, при создании, мо дификации и расширении инструментальных средств анализа NCES-сетей. Это связано со следующими факторами: а) нетриви альностью вычисления разрешенных шагов в NCES-сетях;

б) с эволюцией и развитием NCES-сетей, появлением новых модифи каций, в результате которых сетевой формализм расширяется, и поведение сети усложняется. В итоге реализацию метода Model Checking необходимо производить заново.

Для решения задачи реализации метода Model Checking для анализа NCES-сетей самых различных классов в данной работе предлагается использование хорошо известных и зарекомендо вавших себя верификаторов, созданных специально для поддерж ки метода Model Checking. К числу таких верификаторов, прежде всего, относятся свободно доступные системы SMV (Symbolic Model Verifier) [12] и NuSMV [13]. Однако непосредственное мо делирование NCES-сетей как синхронно-асинхронной системы в верификаторах типа SMV затруднительно из-за сложности явного вычисления разрешенных шагов [14], поэтому в работе [15] в ка честве промежуточного шага было предложено асинхронное мо делирование NCES-сетей. В асинхронной модели вычисление раз решенных шагов производится автоматически.

Предлагается методика исследования NCES-сетей на основе метода Model Checking, включающая следующие основные этапы:

1) переход от модульной иерархической NCES-сети к одно уровневой (плоской) модели;

2) преобразование NCES-сети в асинхронную модель (А модель);

3) кодирование А-модели на входном языке верификатора SMV;

4) формулировка в SPEC-предложениях языка SMV общих и частных свойств NCES-сети в проекции на А-модель с использо ванием временной логики CTL;

IX Международная научно-техническая конференция 5) вычисление формул временной логики, полученных в п.3, в системе SMV;

6) интерпретация полученных результатов.

Первые два этапа могут быть автоматизированы путем по строения транслятора внешнего представления NCES-сетей (на пример, XML-представления) в код SMV. В генерируемый SMV код также могут включаться общие свойства, инвариантные ко всем NCES-сетям. К данным свойствам относятся, например, свойства отсутствия тупиков (deadlock) и бесконечных зацикли ваний (livelock), а также свойства ограниченности и безопасности сети. Ниже подробно рассматриваются наиболее важные этапы приведенной методики. Следует заметить, что в данной работе в качестве примера рассматриваются только два класса сетей:

NCES-сети с ингибиторными дугами и арифметические NCES сети.

Наиболее близкой к данной статье, можно считать работы, свя занные с моделированием сетей Петри и их расширений с помо щью систем типа SMV. Обстоятельно методы моделирования се тей Петри в системе SMV приведены в работе [16]. В ряде работ было рассмотрено представление на входном языке верификатора SMV расширенных сетей Петри: PRES-сетей [17], сетей Петри с дуальными переходами [18], сигнально-интерпретированных се тей Петри (SIPN) [19,20] и цветных сетей Петри [21].

2. Формализм А-моделей Одним из основных этапов методики анализа NCES-сетей, приведенной выше, является преобразование NCES-сети в А модель. Формализм А-моделей был подробно представлен в рабо те [15]. Для предлагаемого ниже варианта преобразований доста точным является упрощенная версия формализма, основные типо вые конструкции которого приведены в таблице 1. Для наглядности дуги, связанные со сбросом, а также сопряженные дуги обозначены пунктирной или штрих-пунктирной линией.

Таблица 1. Структурные элементы формализма А-модели, ис пользуемые для моделирования NCES-сетей.

Текстовое Графическое обозна- Условие Изменение «НИТиС-2010»

описание чение разрешен- маркировки ности дуги при сраба тывании перехода Числовая m’(p)=m(p) p t (n1,n2) m(p)n (ординар n ная) дуга Безуслов Разрешена p t (0,all) m’(p)= ная дуга всегда сброса p Пороговая t (n,all) m’(p)= m(p)n дуга сброса Тестирую Маркировка щая дуга с p t (n,0) не изменя m(p)n проверкой на “больше ется или равно” Ингиби p t (n,0) Маркировка торная дуга m(p)n не изменя (дуга с про веркой на ется “меньше”) Сопряжен ные дуги (0,0) * Разрешена m’(p2)=m(p для безус ловного всегда 1) p p1 t копирова ния меток Сопряжен ные дуги m’(p2)=m(p (0,all) + Разрешена для безус 2)+m(p1) ловного всегда m’(p1)= p p1 t добавления меток Сопряжен m’(p2)= (0,all) * Разрешена ные дуги m(p1) для безус- всегда m’(p1)= p p1 t ловного IX Международная научно-техническая конференция передвиже ния меток 3. Особенности асинхронного моделирования NCES-сетей Одной из основных проблем при асинхронном моделировании NCES-сетей является вычисление разрешенных шагов [15]. При этом необходим постоянный мониторинг завершения срабатыва ния шага. По идее надо производить мониторинг выполнения ка ждого шага в NCES-сети. Основой шага в NCES-сети является триггерный переход. Один и тот же триггерный переход tti может быть центром образования нескольких шагов. А поскольку одно временное срабатывание шагов, включающих триггерный переход tti, исключается, то можно производить, не нарушая логику функ ционирования сети, мониторинг всей совокупности шагов, осно ванных на триггерном переходе tti (то есть учитывать только пе реходы, входящие в событийный граф максимально разрешенных шагов (СГМРШ) [14]).Процедура построения СГМРШ для триг герного перехода tti может основываться на поиске переходов NCES-сети, достижимых из этого триггерного перехода tti по со бытийным дугам. С другой стороны, как и в обычных сетях Петри [22], одновременное (в смысле синхронное) срабатывание триг герных переходов в NCES-сети исключается, что позволяет про изводить даже глобальный мониторинг срабатывания шагов в пределах всей сети.

На основе этих рассуждений в работе [15] выделено два подхо да к реализации мониторинга событийных сигналов. В первом случае (режим 1) для каждого СГМРШ вводится собственный ло кальный переход-монитор. Во втором случае (режим 2) использу ется только один глобальный переход-монитор. Следует отметить, что концепция глобального перехода-монитора в некоторых слу чаях и для некоторых видов NCES-сетей (например, арифметиче ских NCES-сетей) является неудобной и даже недостаточной. При срабатывании перехода-монитора выполняются действия, связан ные с завершением выполнения шага (например, передвижение меток из позиций-двойников в основные позиции). При срабаты «НИТиС-2010»

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

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

4. Правила преобразования NCES-сети в А-модель Ниже полуформально представлены правила преобразования NCES-сети в А-модель. Для простоты в правилах не приводятся условия запрещения применения правил (так называемые NAC условия [23]). Кроме того, некоторые правила содержат целые преобразования типовых ситуаций, включающие несколько пра вил, поэтому их нельзя рассматривать как “простые” явные пра вила системы перезаписи графов. Штриховым контуром отмеча ется СГМРШ, называемый в дальнейшем просто событийным графом. Приводимый ниже набор правил является полным и дос таточным для трансформации любой замкнутой одноуровневой NCES-сети, расширенной ингибиторными дугами, в А-модель, в IX Международная научно-техническая конференция которой используются локальные переходы-мониторы.

Правило на рисунке 1 создает одну единственную для всей се ти глобальную семафорную позицию. Правило, представленное на рисунке 2, создает для событийного графа, образованного триггерным переходом tti, локальную семафорную позицию locsemi и локальный переход-монитор monitori. При этом также создаются соответствующие дуги между данными элементами.

Рисунок 1. Правило создания глобальной семафорной позиции.

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

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

Рисунок 3. Правило связывания глобальной семафорной позиции с инфраструктурными элементами шага в случае, когда триггерный переход образует шаг.

«НИТиС-2010»

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

Согласно правилу на рисунке 5 для каждого форсируемого пе рехода создается событийная позиция. Число дуг, входящих в эту позицию, равно числу событийных дуг, входящих в форсируемый переход. Если этот переход имеет И-логику и число входящих в него событийных дуг больше единицы, то создается так называе мая порогово-событийная позиция, в других случаях – обычная событийная позиция. Для каждой событийной позиции создается переход типа reset для ее сброса. Событийная позиция соединяет ся со всеми созданными локальными переходами-мониторами с использованием ингибиторных дуг (данное правило не показано).

При этом если данная позиция является обычной событийной, то используется обычная ингибиторная дуга, а если порогово событийной, то вес ингибиторной дуги полагается равным (k,all), где k – число дуг, входящих в событийную позицию. Переброска событийных дуг между переходами на соответствующую собы тийную позицию осуществляется с помощью “простого” правила на рисунке 6.

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

IX Международная научно-техническая конференция Рисунок 6. Правило переброски событийной дуги на событийную позицию.

Для каждого форсируемого перехода, в который входит более одной событийной дуги, создается собственная ограничивающая позиция (рисунок 7). Следует, однако, заметить, что если в фор сируемый переход входят событийные дуги, исходящие только из триггерных переходов, то ограничивающая позиция не создаётся, поскольку из логики функционирования NCES-сетей следует, что переходы – образы таких форсируемых переходов в А-модели – могут сработать только один раз. Их повторное срабатывание не возможно вследствие того, что в NCES-сетях запрещены циклы, составленные из событийных дуг.

Рисунок 7. Правило создания ограничивающей позиции.

Маркировка этой позиции в самом начале срабатывания шага устанавливается равной единице. Эта маркировка ограничивает срабатывание каждого перехода в шаге одним разом. Это опреде ляется особенностью функционирования NCES-сетей. Графически ограничивающую позицию будем представлять в виде многолуче вой звезды. Следует заметить, что установку ограничивающей позиции можно осуществить и с помощью перехода типа monitor.

В этом случае в приведенном правиле триггерный переход tti за меняется переходом-монитором. Как раз эта модификация ис пользуется в примере, приведенном на рисунке 17. Данное прави ло может применяться также и для форсируемых переходов, в которые входит только одна дуга. Однако это нецелесообразно, учитывая Утверждение 4, приводимое ниже.

В соответствии с нашей концепцией интерпретации NCES «НИТиС-2010»

сетей, сигнал, приходящий на неразрешенный переход, должен быть немедленно удален (сброшен). Таким образом, для соверше ния этого действия надо уметь определять ситуацию, когда пере ход не разрешен. Как известно, переход t имеет входную И-логику (по позициям) и является разрешенным тогда, когда выполняется условие in1 & in2 &… & ink, где inj (i=1,k) –условия разрешенно сти перехода t по входным позициям. Следовательно, переход t является неразрешенным, если in1 in2 … ink. Данная операция дизъюнкции представляется в правиле создания цепи сброса событийной позиции неразрешенного ИЛИ-перехода (ри сунок 8) с использованием k переходов типа reset. Следует заме тить, что при моделировании необходимо принимать во внимание также ограничивающую позицию.


Рисунок 8. Правило создания цепи сброса событийной позиции не разрешенного ИЛИ-перехода.

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

...

...

Рисунок 9. Правило создания цепи сброса событийной позиции не разрешенного И-перехода.

IX Международная научно-техническая конференция При срабатывании шага в NCES-сети, информация, передавае мая по тестирующим и ингибиторным дугам в переходы, вовле ченные в срабатывание, является “замороженной” и не изменяется в течение срабатывания шага. Для А-моделирования данного фак та предлагается расщеплять позицию NCES-сети на две позиции:

основную позицию и позицию-двойник (рисунок 10). Основная позиция предназначена для обычных дуг, а дублирующая позиция – для тестирующих и ингибиторных дуг. Маркировка основной позиции может изменяться при срабатывании соответствующих выходных переходов, в то время как маркировка позиции двойника не изменяется. В частном случае, когда из позиции p выходят только тестирующие или ингибиторные дуги, или только обычные дуги, то создавать позицию-двойник нет необходимости.

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

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

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

Следует заметить, что если несколько переходов шага имеют не «НИТиС-2010»

которую позицию в качестве выходной, то позиция-двойник соз дается в одном экземпляре. Если же выходная позиция p не явля ется входной для любого перехода событийного графа, то приве денное на рисунке 11 правило не применяется.

Рисунок 11. Правило создания двойника для выходной позиции пе рехода шага.

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

5. Валидация метода Валидация предложенного метода асинхронного моделирова ния NCES-сетей может проводиться двумя путями: 1) формули ровкой характерных утверждений об А-модели NCES-сети, согла сующихся с теорией NCES-сетей, и их доказательстве;

2) тестированием метода на основе конкретных показательных при меров.

Функционирование А-модели NCES схематично проиллюстри ровано на рисунке 12. Черными кружками обозначены стабиль ные маркировки, то есть маркировки, в которых значение сема форных позиций равно единице. Это означает, что все переходные процессы в сетевой модели завершились. Стабильные маркировки представляют действительные маркировки NCES-сети.

IX Международная научно-техническая конференция Рисунок 12. Лепестковая диаграмма, представляющая функциони рование А-модели NCES-сети.

“Лепестки” представляют шаги срабатывания 1, 2,…,k. в NCES-сети, причем лепесток i определяет все варианты образо вания соответствующего шага. Лепестки можно интерпретировать как множества промежуточных маркировок, через которые про ходят трассы срабатываний переходов (представляющих шаг) от одной стабильной маркировки к другой. Лепестки могут перекры ваться, что возможно, как правило, при шагах, имеющий один и тот же триггерный переход. Тем не Рисунок 13. Структура лепестков, порожденных одним триггерным переходом.

менее, из одной и той же маркировки А-модели также возможны «НИТиС-2010»

два (и более) пути, начинающиеся разными триггерными перехо дами, но ведущими в одну и ту же нестабильную (внутреннюю) маркировку, которая будет вершиной, лежащей в области пере крытия соответствующих лепестков. Из данной вершины возмож но продолжение лепестков в форме, представленной на рисунке 12, но уже без перекрытий. Более подробная структура лепестков, порожденных одним и тем же триггерным переходом, представ лена на рисунке 13. Из данного рисунка видно, что вычисление семейства шагов начинается срабатыванием триггерного перехо да, а всегда заканчивается срабатыванием перехода monitor, отно сящегося к соответствующему событийному графу. Актуальной задачей является уменьшение числа промежуточных состояний и числа трасс (и, соответственно, площади этих лепестков), по скольку все это сказывается на времени анализа модели. Следует, однако, заметить, что наличие промежуточных состояний не уве личивает радикально общее число состояний модели.

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

Утверждение 1 [15] Введем следующую пометку А-модели: замаскируем служеб ные переходы А-модели с помощью “пустого” символа. Тогда префиксный язык L, порожденный фрагментом А-модели, кото рый соответствует СГМРШ триггерного перехода ttT NCES сети, определяет все возможные разрешенные шаги, источником которых является этот триггерный переход tt. При этом каждое слова языка L будет представлять собой некоторый шаг. Следует заметить, что при идентификации шага порядок переходов в слове языка L является несущественным. Так, например, два разных слова (t1,t3,t2) и (t3,t1,t2) определяют один и тот же шаг {t1,t2,t3}.

Приведенное утверждение определяет применимость предложен ного метода асинхронного моделирования NCES-сетей в принци пе.

Утверждение Назовем переход А-модели, представляющий переход NCES IX Международная научно-техническая конференция сети, базовым. Тогда срабатывание каждого базового перехода A модели строго сокращает число разрешенных базовых переходов, входящих в шаг. Это утверждение гарантирует, что процесс моде лирования вычисления и срабатывания разрешенного шага явля ется конечным.

Утверждение 3 [15]` Процесс вычисления некоторого разрешенного шага в А модели закончен, когда маркировка простых событийных позиций А-модели, связанных с этим шагом, равна нулю, а маркировка по роговых событийных позиций меньше числа событийных дуг, входящих в соответствующий И-переход. Данное утверждение определяет критерий окончания процесса моделирования сраба тывания шага.

Утверждение Базовый переход А-модели, в который входит одна событийная дуга, не может сработать более одного раза при условии ограни чения до единицы срабатываний тех (узловых) переходов, в кото рые входит более одной событийной дуги. Данное утверждение может использоваться для упрощения соответствующих преобра зований рассмотрением только узловых переходов.

Доказательство Данное утверждение вполне очевидно и его доказательство может быть проведено следующим образом. Представим разре шенный шаг в виде событийного (ациклического) графа (с одним источником в виде триггерного перехода), а срабатывание шага представим как мгновенное распространение сигналов по дугам этого графа с максимальной степенью параллелизма (в соответст вии с теорией NCES-сетей [1,2]). Ограничивая срабатывание узло вого перехода до единицы, мы определенным образом разбиваем ациклический граф на поддеревья. При этом узловые вершины распадаются на несколько вершин, одна из которых является ис точником единичного сигнала (из которого исходят событийные дуги), а остальные – приемниками (в которые событийные дуги заходят). Как известно, в древовидной структуре имеется только один путь из корня до любой другой вершины. Следовательно, «НИТиС-2010»

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

Иллюстрация данного Утверждения представлена на рисунке 14. В данном случае источником сигнала является триггерный пе реход tt. Переход t3 является узловым – в него входят две ветви и выходит одна ветвь. Ограничивая прохождение через переход t одним сигналом, мы достигаем того, что через переходы t4, t5 и t также проходит один сигнал.

t t1 t4 t t1 t4 t t3 tt tt t t t t Рисунок 14. Иллюстрация метода ограничения числа проходимых сигналов через узловые переходы.

Можно заметить, что применение правила ограничения числа проходящих через переход сигналов (на рисунке 14) к не узловым переходам не изменит правильность функционирования модели, но при этом размерность модели увеличивается, что приведет и к увеличению времени ее анализа. Применение данного правила можно исключить при условии, когда все (кроме одной) входящие в форсируемый ИЛИ-переход событийные дуги исходят из “чу жих” триггерных переходов или форсируемых переходов, при надлежащим “чужим” шагам. Это очевидно, поскольку их сраба тывание исключается при обработке собственного шага.


Утверждение 4 явилось основой введения в А-модель ограничи вающих позиций.

Утверждение Порядок срабатывания переходов сброса (типа reset) при вы числении шага в А-модели является несущественным.

Доказательство Непосредственное взаимовлияние срабатывания одного пере хода на другой может наблюдаться только на основе общих вход ных или выходных позиций. Переходы типа reset могут иметь общие входные и выходные позиции, как рабочие, так и служеб ные. Поскольку выходные позиции переходов в нашем случае не IX Международная научно-техническая конференция влияют на их разрешенность, то мы их в дальнейшем не рассмат риваем. Служебные входные позиции переходов типа reset такие, как событийные и ограничительные являются собственными по зициями, и по ним не может быть непосредственного влияния.

Также следует заметить, что в сработавший шаг входили только неконфликтные между собой переходы, то есть отсутствует кон фигурация, при которой у рабочих переходов шага имеется одна рабочая разделяемая позиция и эта позиция связана обычными дугами с этими переходами. А наличие разделяемой позиции с различными типами исходящих дуг (простые, тестирующие, ин гибиторные) исключается с помощью дублирования позиций. То есть каждый переход сброса в этом случае имеет собственные входные позиции. Таким образом, непосредственное влияние сра батывания одного перехода сброса на другой переход сброса ис ключается. Опосредованное влияние срабатывания одного пере хода сброса на другой могло бы наблюдаться только через событийные позиции. Срабатывание некоторого перехода сброса и соответственно сброс событийной позиции предотвращают рас пространение сигнала по событийному графу, и поэтому это не может повлиять на срабатывание других (разрешенных) перехо дов типа reset, а именно – привести к увеличению числа разре шенных переходов типа reset.

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

6. Методика кодировки А-модели на входном языке вери фикатора SMV Поскольку А-модель является расширением сетей Петри, то для ее моделирования на языке SMV можно адаптировать методи ки для моделирования обычных сетей Петри на языке SMV [16]. В работе [16] были представлены четыре подхода к представлению сетей Петри на SMV: 1) “Переходы как SMV-процессы”;

2) “Реше ние проблемы справедливости”;

3) “Позиции как модули”;

4) “Использование TRANS и INIT”. В дальнейшем рассмотрим адап «НИТиС-2010»

тированный вариант четвертого подхода как наиболее эффектив ный в плане быстродействия. Предлагаемая методика включает следующие положения:

1) Каждая позиция A-модели описывается как переменная в SMV. Если позиция является безопасной, то можно использовать переменную булевского типа, например, VAR p1: boolean;

Если же маркировка позиции k-ограничена, то можно использовать пере менную SMV целого (интервального) типа, например, VAR p1:

0..10;

В данном случае ограниченность позиции равна 10. Если же ограниченность позиции априори неизвестна, то следует исполь зовать целочисленную переменную с максимально допустимым значением (определяется инструментальной средой). Для задания точного соответствия рекомендуется переменным давать такие же имена, что и у соответствующих им позиций.

2) Начальная маркировка позиций описывается в ASSIGN разделе программы SMV с использованием операторов init, при чем значение маркировки позиции определяется значением цело численной или булевой переменной. Пример: init(p1) := 1;

3) Условие разрешенности перехода определяется в виде DEFINE-предложения, которое представляет собой логическое выражение над переменными, моделирующими позиции. Реко мендуется ставить DEFINE-предложение в начало модуля. При мер:

DEFINE t1.enabled := globsem & locsem1 & st1 & p1 = 1;

Приведенное DEFINE-предложение определяет по сути прави ло разрешенности перехода (пусть его имя будет t1). Слева от знака равенства стоит имя условия разрешенности перехода (t1.enabled), а справа – логическое выражение, определяющее ус ловие разрешенности. Условие разрешенности перехода t1 пока зывает, что для разрешенности перехода t1 необходимо, чтобы все его входные позиции (переменные) globsem, locsem1, st1 и p1были маркированы.

4) Закодировать отношение переходов напрямую с использо ваний конструкций TRANS и INIT. С использованием конструкции TRANS явно представляются все переходы в сетевой модели. При IX Международная научно-техническая конференция этом переходы в описании разделяются знаком |. Для каждого пе рехода описываются условие совершения перехода, а также то, как связано предыдущее и последующее значение каждой пере менной модели (или, по сути дела, как изменяется значение каж дой переменной). Пример кодировки перехода:

T11.enabled & next(P11) = P11 - 1 & next(P12) = P12+1 & next(P21) = P21 & next(P22) = P22 & next(R) = R - 5) Свойства сетевой модели (как общие, так и частные) форму лируются в использованием временной логики CTL в SPEC предложениях. Например, свойство наличия тупика в сети выра жается следующим образом (здесь знак ! определяет отрицание):

SPEC EF !Условие разрешенности 1-го перехода & !Усло вие разрешенности 2-го перехода&…& !Условие разрешенно сти n-го перехода 7. Пример. NCES-сеть с различными типами дуг и разделяемой позицией Рассмотрим пример NCES-сети, изображенной на рисунке 15.

Данная сеть включает два триггерных перехода (t1 и t6), четы ре форсируемых перехода (t2..t5), ординарные, событийные, ин гибиторные и тестирующие дуги, а также одну разделяемую по зицию r. Эта позиция является одновременно как входной, так и выходной по отношению к переходам некоторых шагов. Граф достижимых состояний для данной сетевой модели приведен на рисунке 16. Дуги данного графа помечены шагами, срабатывание которых переводит сеть из одного состояния в другое. Достижи мыми являются следующие маркировки: m0= {p1, p2, (2)p3, (2)p4, p5, p6, r}, m1= {p2, (2)p3, p4, p6, q1, q4, q5, r}, m2= {(2)p3, p4, q1, q2, q4, q5, q6}, m3= {(2)p3, p4, p5, p6, q1, q2, q4}, m4= {p3, p4, p5, q1, q2, q3, q4, q6}, m5= {p1, (2)p3, (2)p4, p5, q2, q6}, m6= {(2)p3, (2)p4, p5, q1, q2, q6}.

Преобразуем данную NCES-сеть в А-модель (рисунок 17). Для упрощения преобразований будем использовать концепцию гло бального перехода-монитора. В данном случае это возможно, по скольку действия при завершении (неактивного) шага (шагов) на «НИТиС-2010»

основе триггерного перехода t1 при реальном завершении актив ного шага (шагов) на основе триггерного перехода t6 (и наоборот) не причиняют вреда для дальнейшего корректного функциониро вания сети.

Рисунок 15. Пример NCES-сети.

m {t6,t2} {t1,t5,t4} {t1,t2,t4} m3 m m {t1} {t6,t3} {t6,t2} m4 m m Рисунок 16. Граф достижимости для сети на рисунке 14.

Ниже представлен пример кодирования перехода t1 на языке SMV:

t1.enabled & next(p1) = p1 - 1 & next(q1) = q1 +1 & next(p2) = p & next(q2) = q2 & next(p3) = p3 & next(q3) = q3 & next(p4) = p4 & next(q4) = q4 & next(p5) = p5 & next(q5) = q5 & next(p6) = p6 & next(q6) = q6 & next(e1) = e1 + 1 & next(e2) = e2 & next(e3) = e3 + IX Международная научно-техническая конференция 1 & next(e4) = e4 +1 & next(r) = r & next(_r) = _r & next(r_) = r & next(lim1) = lim1 & next(lim2) = lim2 & next(semaphore) = sema phore - На языке временной логики CTL было составлено более свойств А-модели, связанных с корректностью ее функциониро вания. Например, запрос на достижимость маркировки m2 в NCES-сети (рисунок 15-16) определяется как SPEC EF (p3=2 & p4=1 & q1=1 & q2=1 & q4=1 & q5=1 & q6=1 & p1=0 & p2=0 & p5=0 & p6=0 & r=0 & & semaphore=1) В данном случае условие semaphore=1 гарантирует, что будет производиться поиск стабильной маркировка А-модели, которая соответствует искомой маркировке NCES-сети.

Рисунок 17. А-модель NCES-сети, приведенной на рисунке 15.

Свойство зацикливания перехода t1:

SPEC EF AG t1.enabled Свойство неизбежности обнуления событийной позиции e4:

SPEC AG ((e4=1) - AF (e4=0)) «НИТиС-2010»

Свойство возможности разрешенности перехода-монитора при разрешенности одного из базовых переходов.

SPEC EF (t1.enabled | t2.enabled | t3.enabled | t4.enabled) & monitor.enabled Результаты проверки модели соответствуют нашим представ лениям о функционировании модели. Поэтому мы считаем, что трансформация NCES-сети в А-модель была произведена коррект но.

8. Пример. Арифметическая NCES-сеть В данном разделе показывается возможность асинхронного моделирования арифметических NCES-сетей (aNCES-сетей), вве денных в работе [4]. Сети данного класса являются удобным средством для моделирования параллельной логико арифметической обработки данных, как синхронной, так и асин хронной. В качестве иллюстративного примера выберем вычисле n result = c + (b * k ) ние итерационной суммы:, где b, c и n – кон k = станты. Для (параллельного) вычисления итерационной суммы предлагается aNCES-сеть, представленная на рисунке 18. Следует обратить внимание на то, что переходы t3 и add2 являются триг герными, но при этом шаги не образуют.

Используемая aNCES-сеть является доменно-ориентированной модификаций aNCES-сетей общего вида и включает специальные переходы-обработчики, выполняющие элементарные арифмети ческие, логические операции и операции сравнения. Для простоты не рассматриваются цепи для установки начальных значений па раметров b, c и n. Как можно видеть из рисунка 18, сетевая модель разделяется на две подсети. Первая подсеть, включающая перехо ды t1, t2 и t3, используется для управления вычислениями, в то время как вторая подсеть, включающая переходы mult, incr, add1, comp и add2, предназначена собственно для обработки данных.

Вычисления производятся циклически, по этапам и с учетом воз можности распараллеливания. На первом этапе параллельно вы полняются операции умножения и инкремента, на втором – опе IX Международная научно-техническая конференция рации сложения и сравнения. В конце основных (циклических) вычислений однократно выполняется операция сложения. Следу ет отметить, что для организации вычислений с использованием aNCES-сетей могут использоваться и другие вычислительные шаблоны и принципы (например, принцип потока данных). В этом случае нет необходимости в управляющей части сетевой мо дели.

Рисунок 18. aNCES-сеть для вычисления итерационной суммы.

Асинхронная модель aNCES-сети, представленной на рисунке 18, показана на рисунке 19. Следует отметить, что в данном слу чае расщепление позиции sum, которая является входной и вы ходной, на основную позицию и позицию-двойник не использует ся вследствие того, что дуга (sum, add2) не относится к шагу {t2, add1, comp}. Поэтому изменение маркировки позиции sum в про цессе срабатывания этого шага не влияет на сам процесс срабаты вания. В целях упрощения в результирующей А-модели не ис пользовались ограничивающие позиции.

Ниже в качестве примера приведена кодировка перехода add А-модели на языке SMV:

add1.enabled & next(p1) = p1 & next(p2) = p2 & next(p3) = p3 & next(c) = c & next(b) = b & next(n) = n & next(k) = k & next(k_) = k_ «НИТиС-2010»

& next(sum) = sum + rm & next(rm) = rm & next(rc) = rc & next(result) = result & next(e1) = e1 & next(e2) = e2 & next(e3) = e - 1 & next(e4) = e4 & next(globsem) = globsem & next(locsem1) = locsem1 & next(locsem2) = locsem В результате тестирования полученного SMV-кода для А модели путем формулировки и вычисления заданных характерных свойств получились ожидаемые результаты, что позволяет гово рить о правильности произведенных преобразований. Например, при входных параметрах c=9, b=5, n=8 была получена результи рующая сумма 189.

Рисунок 19. А-модель aNCES-сети, приведенной на рисунке 18.

Заключение В данной работе был предложен универсальный подход к соз данию верификаторов NCES-сетей на основе метода Model Checking, использующий известные стандартные верификаторы типа SMV. Данный подход позволяет сократить затраты на созда ние собственных верификаторов. Рассмотрены основные этапы методики проектирования верификаторов NCES-сетей заданного класса.

Произведена программная реализация прототипа транслятора IX Международная научно-техническая конференция XML-представления NCES-сети в код SMV на языке C++ в среде Visual Studio 2008. При этом в качестве входных данных исполь зуется XML-представление, создаваемое графическим редактором NCES-сетей, входящим в состав ViVe [7]. Данный графический редактор позволяет создавать NCES-сети с ингибиторными дуга ми.

Направлением дальнейших исследований является разработка метода асинхронного моделирования временных NCES-сетей и разработка для них верификаторов на основе предложенного под хода.

Список литературы 1. Rausch M., Hanisch H.-M. Net condition/event systems with mul tiple condition outputs // IEEE Int. Conf. on Emerging Technolo gies and Factory Automation. – Paris, 1995. - Vol. 1. - P. 592-600.

2. Hanisch H.-M., Lder A. Modular Modelling of Closed-Loop Sys tems // Colloquium on Petri Net Technologies for Modelling Communication Based Systems, Berlin, Germany, October 21-22, 1999. - P. 103-126.

3. Vyatkin, V. Modelling and Verification of Discrete Control Sys tems with Net Condition/Event Systems and Visual Verification Framework. - Working draft, 2007. - 178 c. [Электронный ре сурс]. – http://www.fb61499.com/license.html.

4. Дубинин В.Н. Моделирование систем функциональных бло ков IEC 61499 с помощью модульных арифметических NCES сетей // Тр. VIII Международной науч.-техн. конф. “Новые информационные технологии и системы ”. - Пенза, 2008. – Ч.

2. – С.47-64.

5. Starke P.H., Roch S. Analysing Signal-Net Systems. - Informatik– Bericht 162, Humboldt-Universitaet zu Berlin. - 2002. – 136 p.

6. SESA: Signal-Net System Analyzer [Электронный ресурс]. – http://www2.informatik.hu-berlin.de/lehrstuehle/automaten/tools/.

7. ViVe - VisualVerifier Tool Framework [Электронный ресурс]. – http://www.fb61499.com/license.html.

«НИТиС-2010»

8. TNCES Workbench [Электронный ресурс]. – http://sourceforge.net/projects/tnces-workbench/.

9. SWI-Prolog [Электронный ресурс]. – http://www.swi prolog.org/.

10. McMillan, K.L. Symbolic Model Checking. - Kluwer Academic Publishers, 1993.

11. Кларк Э., Грамберг О., Пелед Д. Верификация моделей про грамм: Model Checking - М.: МЦНМО, 2002. – 416 с.

12. Burch, J.R., Clarke E.M., Long, D.E. Symbolic model checking with partitioned transition relations // International Conference on Very Large Scale Integration, Edinburgh, Scotland, August, 1991.

- P. 49-58.

13. Cadence SMV [Электронный ресурс]. – http://www.kenmcmil.com/smv.html 14. NuSMV - New Symbolic Model Checker [Электронный ресурс].

–http://nusmv.irst.itc.it.

15. Dubinin V., Hanisch H.-M., Missal D. Event graph-based ap proach to interpretation of NCES models // Труды VII Междуна родной науч.-техн. конф. “Новые информационные техноло гии и системы”, Пенза, 2006. – Ч. 1. - С. 172-186.

16. Дубинин В.Н. Асинхронное моделирование NCES-сетей // Известия высших учебных заведений. Поволжский регион.

Технические науки. – 2009. – № 2. - C. 3-14.

17. Wimmel G. A BDD-based Model Checker for the PEP Tool. Major Individual Project Report, University of Newcastle. - New castle, 1997. – 107 P.

18. Cortes L.A., Eles P., Peng Z. Verification Methodology for Het erogeneous Hardware/Software Systems - SAVE Project Report, Linkping University. – Linkping, 2000. – 18 P.

19. Varea, M. Symbolic Model Checking of Dual Transition Petri Nets / M. Varea, B.M. Al-Hashimi, L.A. Cortes, P. Eles, Z. Peng // Int. Symposium on Hardware/Software Codesign (CODES’02), Estes Park, Colorado. – 2002.

IX Международная научно-техническая конференция 20. Klein S., Frey G., Litz L. A Petri Net based Approach to the De velopment of correct Logic Controllers // Second International Workshop on Integration of Specification Techniques for Applica tions in Engineering (INT’02), Grenoble, France, 2002. -P. 116 129.

21. Signal Interpreted Petri Nets (SIPN) Tool [Электронный ресурс] http://www.eit.uni-kl.de/litz/ENGLISH/software/SIPNEditor.htm.

22. Stotts D., Navon J. Model checking cobweb protocols for verifica tion of HTML frames behavior // 11th International Conference on World Wide Web, Honolulu, Hawaii, USA. - P. 182 – 190.

23. Котов В.Е. Сети Петри. – М.: Наука, 1984. – 160 с.

24. Ehrig H. Fundamentals of Algebraic Graph Transformation / H.

Ehrig, K. Ehrig, U. Prange, G. Taentzer. - Springer, 2006. - 373 c.

С.А. Зинкин, В.И. Волчихин Россия, Пенза, Пензенский государственный университет РАЗВИТИЕ НЕФОННЕЙМАНОВСКИХ КОНЦЕПЦИЙ В КОМПЬЮТЕРНОЙ И СЕТЕВОЙ АРХИТЕКТУРЕ Предлагается новая технология архитектурного мо делирования и проектирования систем и сетей обра ботки данных. Рассматриваемые методы базируются на формальном описании процессов над структури рованной памятью.

В настоящее время активно развиваются методы, основанные на предварительном формальном описании предметной области – ее понятий, отношений, закономерностей. При формализации предметных областей, связанных с системами и сетями хранения и обработки данных, широко используются сетевые модели. В сетевых моделях представляются как информационно структурные знания о предметной области, так и знания о процес сах, причинно-следственных связях, законах функционирования, сценариях деятельности. Модели представления знаний условно разделяются на декларативные (непроцедурные) и процедурные.

Принципы программной и структурной организации ЭВМ, «НИТиС-2010»

предложенные различными специалистами и описанные фон Нейманом, состоят в использовании внутреннего языка низкого уровня, в последовательном централизованном управлении вы числительным процессом с единственной последовательностью команд и в линейной организации памяти, состоящей из упорядо ченной последовательности одинаковых адресуемых ячеек. Как известно, недостатком многих мультипроцессорных вычисли тельных систем является жесткость их структуры, не позволяю щая эффективно решать сложные задачи с большим числом па раллельных процессов, активно взаимодействующих между собой, в то же время частичная модификация принципов фон Неймана неизбежно приводит к противоречию между структурой ЭВМ и организацией вычислительного процесса. Целью настоя щей работы является исследование новых принципов построения систем и сетей распределенной обработки информации, основой которых является система или сеть хранения данных, а согласо ванная работа модулей и узлов координируется через общее вир туальное пространство памяти – основной и внешней (возможно, сетевой).

Фундаментальный принцип структурной интерпретации язы ков высокого уровня, предложенный В.М. Глушковым для отече ственных интеллектуальных ЭВМ, является развитием первого из перечисленных фон-неймановских принципов. Применение раз деляемой основной и внешней памяти и комплексирование ЭВМ привело к развитию методов распараллеливания вычислений и изменило отношение разработчиков к реализации второго прин ципа. В дальнейшем получили развитие ассоциативные мульти процессорные вычислительные системы, в которых обращения к элементам памяти процессорных элементов осуществляются по признакам обрабатываемых данных, то есть “ревизии” подверга ется и третий принцип фон-неймановской архитектуры.



Pages:   || 2 | 3 | 4 | 5 |
 



Похожие работы:





 
© 2013 www.libed.ru - «Бесплатная библиотека научно-практических конференций»

Материалы этого сайта размещены для ознакомления, все права принадлежат их авторам.
Если Вы не согласны с тем, что Ваш материал размещён на этом сайте, пожалуйста, напишите нам, мы в течении 1-2 рабочих дней удалим его.