NONDETERMINISTIC AUTOMATA MODELES FOR FORMAL PRESENTTATION OF THE BASIC PROPERTIES OF THE CONTROL SYSTEMS OF PARALLEL PROCESSES AND RESOURCES

Full Text

Введение Формальное аналитическое описание основных свойств систем управления необходимо, с одной стороны, для аналитического представления алгоритмов управления параллельными процессами и ресурсами, а с другой - для верификации таких алгоритмов. При этом основные свойства систем управления ( СУ) должны быть такими, чтобы обеспечивалось выполнение основных характеристик таких систем, к числу которых относятся - надежность и эффективность систем. В связи с этим для реализации таких СУ и их верификации необходимо использовать математический аппарат, который, с одной стороны, обеспечивал бы формальное аналитическое представление сложных алгоритмов управления, а с другой - отличался бы простотой и компактностью. В качестве такого математического аппарата в данной статье предлагается использовать модели событийных недетерминированных автоматов (СНДА), которые обладают следующими достоинствами [12]: во-первых, модели СНДА отличаются значительной простотой и компактностью, так как описание свойств СУ выполняется не в терминах состояний детерминированных автоматов (ДА), а в терминах частных событий, реализуемых в системах управления, учитывая при этом, что число таких частных событий m СНДА будет значительно меньше числа состояний ТҐІ М эквивалентного ему ДА, так как М < 2 . Во-вто рых, использование моделей СНДА предоставляет широкие возможности для описания сложных алгоритмов управления параллельными процессами и ресурсами, так как основой таких моделей является практически сеть, вершины которой отождествляются с некоторыми событиями, а дуги - соотношениями между этими событиями [1-4]. Основные свойства СУ параллельными процессами и ресурсами и их формальное описание, когда события в явном виде зависят от времени Для увеличения производительности решения сложных вычислительных задач или задач промышленной автоматики такие задачи обычно разбиваются на параллельные ветви. В связи с этим возникает необходимость в реализации синхронизации взаимодействия таких параллельных ветвей (процессов) при обращении к общим критическим ресурсам или при обмене сообщениями. Для этой цели используют различные механизмы синхронизации процессов, к числу которых относятся критические интервалы, мониторы, кольцевые буферы, рандеву и др. Для обеспечения надежности и эффективности таких СУ параллельными процессами и ресурсами к используемым механизмам синхронизации предъяв- «Инфокоммуникационные технологии» Том 11, № 3, 2013 96 Бикташев Р. А., Вашкевич Н.П. ляют необходимые требования, которые являются основой определения и реализации основных свойств таких систем [5-6]. В качестве примера рассмотрим, какими свойствами должны обладать события, реализующие управление параллельными процессами, при использовании механизмов критических интервалов и мониторов. К числу таких основных свойств относятся справедливость, достижимость, взаимоисключение и приоритетность событий, определяющих вход процессов в свой критический интервал или в монитор и нахождение в них. События, определяющие вход 7-го процесса в - - ( л свой критический интервал I £к J или в монитор (^м) ’ можно представить таким образом [7]: iSkO + 1) ^впдс ^вздс^прдс v SKS„K > (!) L(/ + 1) і В уравнениях (1)-(2) первая составляющая, представленная конъюнкцией событий, определяет вход 7-го процесса в свой критический интервал (1) или монитор (2). Эти события и определяют отмеченные выше свойства, в том числе и свойства справедливости и достижимости, которые опре- і деляются событиями типа ^вп • Эти события для используемых механизмов синхронизации должны быть представлены в следующем виде: £вп,кО + 0 _(^з v ^ВПДС^К ’ ^ Sвп,м 0 + 0 _(^з v Sвп,м)'S’m $мп’ ^ і і где ^вп,к и £вп,м - события, свидетельствующие о восприятии заявки 7-го процесса (событие і Sз) к общему критическому ресурсу и ее сохранение только в том случае, когда данный процесс не находится в своем критическом интервале (3) или в мониторе (4) соответственно. Это означает, что ни один процесс не будет бесконечно долго ждать входа в свой критический интервал или монитор. і Событие Sun свидетельствует об отсутствии повторного входа в монитор 7-го процесса, который ранее вышел из монитора не обслуженным. В данном случае это обеспечивает свойство справедливости для таких процессов. Вторая составляющая уравнений (1)-(2), представленная конъюнкцией событий, определяет время нахождения 7-го процесса в своем критическом интервале (1) или монитора (2). В данном і случае событие Sпк свидетельствует об окончании одноразовой операции 7-го процесса с общим критическим ресурсом. і Событие SfiM свидетельствует об окончании одноразовой операции 7-го процесса с общим критическим ресурсом, если данный 7-ый процесс не вышел из монитора не обслуженным (Л \ I 1. Свойство достижимости событий I Sk и >м обеспечивается наличием события типа 5ВП’ которое является обязательным непосредственно предшествующим для таких событий. Необходимо отметить, что проверить наличие достижимости всех частных событий, реализуемых в СУ, можно путем построения прямой таблицы переходов (ПТП) для этих событий по определенному правилу. Это правило заключается в том, что очередная строка ПТП должна начинаться с представлением такого события, которое уже было отмечено в одной из предшествующих строк ПТП [1-2]. Свойство взаимоисключения событий типа vL и sL обеспечивается входом в одно и то w К JV1 же время в критический интервал или монитор только одного 7-го события из «-процессов. Это свойство формализуется следующими комбинационными событиями: 1 “ÛT W' + l)= AsK і »B3,M (Уа)[а^і] (5) (6) Свойство наличие приоритетности процессов обеспечивает однозначность входа 7-го процесса в свой критический интервал или монитор. Наличие приоритетности событий особенно необходимо в начальный период при обращении процессов к общему ресурсу, когда могут быть і і истинными все события типа Увз и *^вп . В качестве примера рассмотрим приоритетность 7-го процесса для циклической дисципли-І ны обслуживания Удр [6]. Это событие можно представить следующим выражением: £Пр(* + 1) = Snp(°)v ЯвпЯт (7) «Инфокоммуникационные технологии» Том 11, № 3, 2013 Бикташев Р. А., Вашкевич Н.П. 97 где 5пр^ - представляет собой сокращенное обозначение комбинационного события, определяющего начальный приоритет обслуживания i-го процесса: і і -а S пр(°) = Яо^ВП Л 5вП; (Va)[a<i] (8) S+ І) = хо V Sox„ • где хп - сигнал СУ; x0 - сигнал приведения і СУ в начальное состояние; S т - сокращенное обозначение комбинационного события, определяющего приоритет i-го процесса при наличии воспринятой заявки в повторных циклах циклической дисциплины обслуживания; а 5т ViSpk А 5ВП i=l (Va)(a>i) ), (9) где S p]ç - сокращенное обозначение события, определяющего выход i-го процесса из критического интервала или монитора после окончания процедуры обращения к разделяемым данным. Основные свойства систем управления параллельными процессами и ресурсами и их формальное описание, когда события не зависят в явном виде от времени В работе [8] рассматривается язык временной темпоральной логики, когда порядок событий в системе описывается без привлечения времени в явном виде. В данном разделе рассматриваются вопросы описания основных свойств таких систем на основе использования моделей СНДА. В связи с этим будут показаны широкие возможности языка СНДА для описания сложных систем управления, когда события, представленные в таких системах, не зависят в явном виде от времени. К числу основных свойств таких событий согласно [8] относятся следующие: достижимости, достижимости в будущем «рано или поздно», инвариантности, условного ожидания и разблокировки. Свойство достижимости «в следующий момент» (Х), означающее что любое событие S j будет достижимо тогда, когда имеет место событие, непосредственно предшествующее ему, то есть такое свойство уже было рассмотрено при описании событий в (1)-(2). Свойство «рано или поздно», или «когда-то в будущем» (F) . В данном случае таким свойством будет обладать некоторое событие S у, которое будет истинным только в том случае, когда станет истинным некоторое событие SP (определяющее условие зарождения события S у), время наступления которого точно не определено. Учитывая это обстоятельство, вводят вспомогательное событие S f > которое для события S j будет играть роль непосредственно предшествующего события. Тогда описания таких событий будут иметь вид Л'*0л-М SrSp V SjSj,к - (10) 'г, з V S ’ где Srß - событие, определяющее зарождение события Sr> Sу,к - событие, определяющее условие сохранения события S j. Свойством инвариантности, или «всегда, повсюду», (G) будет обладать некоторое событие Sj, которое будет истинным всегда (повсюду) для всех n- непосредственно предшествующих событий (s,) для события s j, то есть событие S j можно представить как J п - Sfi + 1) = V V SjSj'K , (11) /=1 где 5_Дз - событие, определяющее условие зарождения события S j. Свойство условного ожидания, или «до тех пор, пока», (U) - в данном случае таким свойством будет обладать некоторое событие S j, которое не будет истинным долго - до тех пор, пока не будет истинным некоторое событие Sр. При этом каждое из n непосредственно предшеству- ( л ющих событий I sr I (для события S j) после зарождения события S j станет равным нулю іл=0)’ будет облад , то есть каждое событие типа S г тоже эудет обладать отмеченным свойством «до тех пор, пока». Учитывая это обстоятельство, события S j и г S г будут иметь вид Sr(t + 1) = (sr,3vSr)sp , sj(t + 1) = V (sr) i=l (12) Sp V SjSj,к • Свойство разблокировки, «высвободить» (R). В данном случае свойство «высвободить» отно- «Инфокоммуникационные технологии» Том 11, № 3, 2013 98 Бикташев Р. А., Вашкевич Н.П. сится к некоторому событию S j > которое после зарождения будет существовать (то есть остается истинным) до тех пор, пока не зародится некоторое событие S г > которое, в свою очередь, может никогда и не зародиться, если событие, реализующее его зарождение, Sр = 0. Учитывая это, описание событий g - и sr будут иметь вид Д-0 = (^ Д-0= */,з v ^J SjSpVSrSr, к где Sj - событие, являющееся непосредственно предшествующим событию S j . В заключение отметим, что полученные представления событий, реализуемых в вычислительных многопроцессорных системах или в системах управления объектами промышленной автоматики, в виде системы канонических уравнений (модель СНДА), естественно по шагам отражают алгоритмы работы преобразования информации, что позволяет осуществить переход к различным вариантам их реализации: аппаратно, программно или в виде их комбинаций и выполнить их верификацию путем моделирования на модели [8-1

About the authors

N. P Vashkevich

Email: rabiktashev@mail.ru

R. A Biktashev

Email: vt@pnzgu.ru

References

Supplementary files