Обобщенная модель системы автоматов
Статья посвящена проблеме моделирования, композиции и детерминизма составных систем. Компоненты системы моделируются конечными автоматами с несколькими входами и выходами, а взаимодействие между ними - обменом сообщениями по симплексным каналам связи. Система описывается ориентированным графом связей, вершина которого соответствует автомату компонента, а дуга - каналу связи, соединяющему выход одного автомата с входом другого. Автоматы системы работают синхронно: на каждом такте каждый автомат выполняет один переход. Определяются ассоциативная композиция автоматов системы по графу связей и условия детерминированности системы.
Generalized model of automata system.pdf Большинство сложных, особенно распределённых, систем представляет собой набор взаимодействующих компонентов. В данной статье компоненты моделируются конечными автоматами, а взаимодействие - обменом сообщениями между автоматами. Автомат может иметь несколько входов для приёма сообщений и может принимать сразу несколько сообщений; также автомат может иметь несколько выходов для посылки сообщений и посылать сразу несколько сообщений. Структура связей между компонентами моделируется ориентированным графом (будем называть его графом связей), вершинам которого соответствуют автоматы, а дуги называются соединениями и соответствуют симплексным каналам передачи сообщений. Соединение, ведущее из автомата A в автомат B, помечается выходом j автомата A и входом i автомата B. При этом каждый вход (выход) каждого автомата соединён не более чем с одним выходом (входом) другого (или того же самого) автомата. Входы (выходы) автоматов, которые не соединяются с выходами (входами) автоматов, являются внешними, через них осуществляется связь системы с её окружением. Автоматы системы работают синхронно: на каждом такте каждый автомат выполняет один переход. Также на каждом такте окружение системы посылает сообщения на некоторые внешние входы системы и принимает сообщения с некоторых внешних выходов системы. Считается, что граф связей статический, т.е. не меняющийся в процессе работы системы. В этом случае система (так же как её компоненты) может моделироваться конечным автоматом, получающимся из автоматов-компонентов с помощью подходящего оператора композиции, учитывающего граф связей. Такая модель системы является обобщением модели, предложенной в [1]. Там дуга графа связей представляла собой, по сути, очередь сообщений длины 1. Она моделируется автоматом с одним входом и одним выходом. Синхронно взаимодействуют автомат в вершине с автоматом дуги, инцидентной этой вершине. Если в графе связей из [1] каждую дугу разбить на два соединения, вставив в «середину» дуги новую вершину, в которую поместить автомат дуги, то получится система автоматов, являющаяся частным случаем системы, предлагаемой в данной статье. «Частность» этого случая заключается в том, что автомат дуги может теперь моделировать не только очередь сообщений длины 1, но и очередь любой другой (в том числе неограниченной) длины, стек и т. д. Более того, в данной статье мы, по сути, не делаем различия между автоматом вершины и автоматом дуги: автомат дуги тоже может иметь несколько входов и выходов. Основная особенность предлагаемой модели автомата заключается в том, что переход автомата, предъявляя требования к состоянию всех входов и выходов автомата (указываются сообщения на них), отдельно указывает ту часть входов и выходов, по которым сообщения принимаются или посылаются. Синхронность взаимодействия автоматов означает, что для каждого соединения требования автоматов, связанных этим соединением, должны быть согласованы. Это даёт возможность описывать более широкий спектр поведений автомата. Например, приоритетный приём сообщений: если на входах автомата имеется несколько сообщений, автомат может принять сообщения с наивысшим приоритетом, не принимая остальные сообщения. Также это позволяет автомату выполнять приём сообщений детерминиро-ванно, т. е. независимо от того, удаётся или не удаётся одновременно послать некоторое сообщение на некоторый выход. Если удаётся послать сообщение, автомат выполняет один переход, а если не удаётся - то другой. Обычно это приводит к недетерминизму: на один стимул выдаются разные реакции. Однако в нашей модели реакция - это требования к выходам, а не указание той части выходов, по которым сообщения реально передаются. В статье определяется ассоциативная композиция переходов, автоматов и системы по известному графу связей. Ассоциативность важна для того, чтобы работа системы зависела только от множества её автоматов и соединений и не зависела от какого-либо упорядочивания этих множеств. Дополнительно определяется композиция автоматов, не связанных соединениями, что позволяет докомпоновать систему ровно до одного автомата, который может использоваться как компонент более сложных систем автоматов. Исследуется проблема детерминизма: даётся определение детерминированного автомата и выясняются условия, при которых композиция детерминированных автоматов является детерминированной. 1. Модель Пусть задано некоторое конечное множество сообщений M, которое мы будем называть алфавитом (сообщений). Пустое множество 0 будем называть пустым сообщением, считать, что 0 g M, и обозначать M0 = M и {0}. Автомат в алфавите M- это набор A = (M, I, J, S, T, s0), где: - I - конечное множество входов автомата; - J - конечное множество выходов автомата; - S - конечное множество состояний автомата; - T с S х X х P х Y х Q х S - множество переходов автомата, где: - X = {x | x: I ^ M0} - множество стимулов; - Y = {y I y: I ^ M0} - множество реакций; - P = 2I - семейство подмножеств входов (по ним принимаются сообщения); - Q = 2J - семейство подмножеств выходов (по ним посылаются сообщения); - s0 е S - начальное состояние; причём выполнены следующие условия: 1) множества входов и выходов не пересекаются: I n J = 0; 2) принимаются и посылаются только непустые сообщения: V(s, x, p, y, q, t) е T (Vi е p (x(i) Ф 0) & Vj е q (y(j) Ф 0)), что эквивалентно V(s, x, p, y, q, t) е T (p с x-1(M) & q с y-1(M)). Очевидно, что из конечности множеств M, I, J и S следует конечность множеств X, Y, P, Q, T. Для перехода a = (s, x, p, y, q, t) состояние s будем называть пресостоянием перехода, а состояние t - постсостоянием, и будем обозначать sa = s, xa = x, pa = p, ya = y, qa = q, ta = t. Для автомата A = (M, I, J, S, T, s0) будем обозначать IA = I, JA = J, SA = S, TA = T, s0A = s0. Работу автомата можно описать следующим образом. В текущем состоянии s проверяется состояние входов, т.е. какие сообщения можно принять с входов автомата. Это определяет стимул x. Далее рассматриваются переходы по этому стимулу, т.е. множество Ts,x с T переходов из s по x. Каждый переход из множества Ts,x определяет ту или иную реакцию y. Если для данных s и x имеются переходы с разными реакциями y, то недетерминированным образом выбирается реакция y как одна из реакций на переходах из множества Ts,x. После выбора реакции y проверяется состояние выходов, а именно какие непустые сообщения, определяемые реакцией у, могут быть переданы по соответствующим выходам, а какие нет. Это определяет параметр q. Тем самым определяется множество Ts?xy?q с Ts,x переходов с данными s, x, у, q. Если это множество содержит более одного перехода, то недетерминированным образом выбирается один из них. Если выбран переход (s, x, p, у, q, t), то параметр p определяет, какие непустые сообщения будут приняты с входов автомата. Таким образом, принимаются сообщения, определяемые стимулом x, по входам, определяемым параметром p; посылаются сообщения, определяемые реакцией у, по выходам, определяемым параметром q, после чего автомат переходит в состояние t. Это описание работы автомата неформально. Формальное описание есть, по существу, формальное определение композиции автоматов, которое будет дано в следующем разделе. Пусть V - конечное множество автоматов в алфавите M. Без ограничения общности можно считать, что входы, выходы и состояния автоматов разные: VA, B е V(A Ф B ^ IAn, IB= 0 & IA
Ключевые слова
ориентированные графы,
взаимодействующие автоматы,
композиция автоматов,
детерминизм,
сети,
directed graph,
communicating automata,
automata composition,
determinism,
networksАвторы
Бурдонов Игорь Борисович | Институт системного программирования РАН | доктор физико-математических наук, ведущий научный сотрудник | igor@ispras.ru |
Косачев Александр Сергеевич | Институт системного программирования РАН | кандидат физико-математических наук, ведущий научный сотрудник | kos@ispras.ru |
Всего: 2
Ссылки
Бурдонов И.Б., Косачев А.С. Тестирование системы автоматов // Труды ИСП РАН. 2016. T. 28 (1).
Бурдонов И.Б., Косачев А.С. Система автоматов: композиция по графу связей // Труды ИСП РАН. 2016. T. 28 (1).
Бурдонов И.Б., Косачев А.С. Система автоматов: условия детерминизма и тестирование // Труды ИСП РАН. 2016. Т. 28 (1).
Hoare C.A.R. Communicating Sequential Processes. Englewood Cliffs, NJ : Prentice Hall International, 1985.
Milner R. Communication and Concurrency. Prentice-Hall, 1989.
Langerak R. A testing theory for LOTOS using deadlock detection // Protocol Specification, Testing, and Verification IX / eds. by E. Brinksma, G. Scollo, C.A. Vissers. North-Holland, 1990. Р. 87-98.
Tretmans J. Test Generation with Inputs, Outputs and Repetitive Quiescence // Software-Concepts and Tools. 1996. Vol. 17, Issue 3.
van der Bijl M., Rensink A., Tretmans J. Compositional testing with ioco // Formal Approaches to Software Testing: Third Interna tional Workshop, FATES 2003, Montreal, Quebec, Canada, October 6th, 2003 / eds. by Alexandre Petrenko, Andreas Ulrich. LNCS Springer, 2003. V. 2931. Р. 86-100.
Petrenko A., Yevtushenko N., Huo J.L. Testing Transition Systems with Input and Output Testers. Proc. IFIP TC6/WG6.1 15th Int. Conf. Testing of Communicating Systems, TestCom'2003. Sophia Antipolis, France, 2003. May 26-29. Р. 129-145.
Бурдонов И.Б., Косачев А.С. Системы с приоритетами: конформность, тестирование, композиция // Программирование. 2009. № 4. С. 24-40.
Бурдонов И.Б., Косачев А.С. Согласование конформности и композиции // Программирование. 2013. № 6. С. 3-15.
Revised Working Draft on "Framework: Formal Methods in Conformance Testing". JTC1/SC21/WG1/Project 54/1, ISO Interim Meeting, ITU-T on. Paris, 1995.
Bourdonov I.B., Kossatchev A.S., Kuliamin V.V. Conformance theory of the systems with Refused Inputs and Forbidden Actions. M. : Nauka, 2008. 412 p. (in Russian)
Bourdonov I. Conformance theory (functional testing on formal model base). LAP LAMBERT Academic Publishing. Saarbrucken, Germany, 2011. 428 p. (in Russian)
Bourdonov I.B., Kossatchev A.S. Specification Completion for IOCO // Programming and Computer Software. 2011. V. 37 (1). P. 1-14.
Kamkin A.S., Chupilko M.M. Survey of modern technologies of simulation-based verification of hardware // Programming and Computer Software. 2011. V. 37 (3). P. 147-152.