Введение

X-машина (XM) — это теоретическая модель вычислений, предложенная Сэмюэлем Эйленбергом в 1974 году. Буква X в названии "X-машина" обозначает фундаментальный тип данных, с которым работает машина; например, машина, работающая с базами данных (объектами типа "база данных"), будет машиной для работы с базами данных. Модель X-машины структурно идентична автомату с конечным числом состояний, за исключением того, что символы, используемые для обозначения переходов, представляют собой отношения типа X→X. Переход по переходу эквивалентен применению отношения, которым он помечен (вычислению множества изменений типа данных X), а проход по пути в машине соответствует последовательному применению всех связанных отношений.

2000-е годы

Машины X были применены к лексической семантике Андрашем Корнаем, который моделирует значение слова с помощью "указанных" машин, в которых один член базового множества X выделен. Применение к другим областям лингвистики, в частности к современной переформулировке грамматики Панини, было впервые осуществлено Жераром Хуэтом и его коллегами.

Основные варианты

Машину X редко можно встретить в исходной форме, но она является основой для нескольких последующих моделей вычислений. Наиболее влиятельной моделью в теориях тестирования программного обеспечения стала машина Stream X. Недавно NASA обсуждало возможность использования комбинации Communicating Stream X Machines и процесса WSCSS при проектировании и тестировании систем групповых спутников. В связи с этим, она связана с исследованиями в теории гипервычислений.

Поток X-машина (SXM)

Наиболее распространенным вариантом машины X является модель Stream X Machine (SXM) 1993 года разработки Gilbert Laycock. Stream X Machine отличается от оригинальной модели Эйленберга тем, что фундаментальный тип данных X имеет вид Out* × Mem × In*, где In* – последовательность входов, Out* – последовательность выходов, а Mem – (остальная часть) памяти. Преимущество этой модели заключается в том, что она позволяет пошагово управлять системой, переходя из состояния в состояние, и наблюдать выходные данные на каждом шаге. Эти данные являются свидетельствами, гарантирующими выполнение определенных функций на каждом этапе. В результате сложные программные системы можно разложить на иерархию Stream X Machines, разработанных сверху вниз и протестированных снизу вверх. Этот подход к проектированию и тестированию, основанный на принципе "разделяй и властвуй", подтверждается доказательством корректной интеграции, предложенным Florentin Ipate, которое показывает, что тестирование слоистых машин по отдельности эквивалентно тестированию составной системы.

Коммуникационный поток X-машины (CSXM)

Первая полностью формальная модель композиции конкурентных X-машин была предложена в 1999 году Кристиной Вертан и Хориа Жоржеску, основываясь на более ранних работах Филиппа Берда и Энтони Коулинга по взаимодействующим автоматам. В модели Вертан машины взаимодействуют косвенно, посредством общей матрицы коммуникаций (по сути, массива ячеек), а не напрямую через общие каналы. Bălănescu, Cowling, Georgescu, Vertan и другие подробно изучили формальные свойства этой модели CSXM. Можно вывести полные отношения ввода-вывода. Матрица коммуникаций определяет протокол для синхронного взаимодействия. Преимущество этого подхода заключается в том, что он разделяет обработку каждой машины и их взаимодействие, позволяя независимо тестировать каждое поведение. Было доказано, что эта композиционная модель эквивалентна стандартной Stream X-машине, что позволяет использовать более раннюю теорию тестирования, разработанную Холкомбом и Ипатом. Этот вариант X-машины рассматривается более подробно на отдельной странице.

Объект "Машина-Икс" (OXM)

Кирилл Богданов и Энтони Саймонс разработали несколько вариантов машины X для моделирования поведения объектов в объектно-ориентированных системах. Эта модель отличается от подхода Stream X Machine тем, что монолитный тип данных X распределен между несколькими объектами и инкапсулирован ими, которые последовательно компонуются; а системы функционируют за счет вызовов и возвратов методов, а не за счет входов и выходов. Последующие исследования в этой области были посвящены адаптации теории формального тестирования в контексте наследования, которое разбивает пространство состояний суперкласса на расширенные объекты подкласса. В 2002 году Саймонс и Станнетт разработали модель "CCS augmented X machine" (CCSXM) для поддержки полного поведенческого тестирования объектно-ориентированных систем при наличии асинхронной коммуникации. Предполагается, что она будет иметь некоторое сходство с недавним предложением NASA, однако окончательного сравнения этих двух моделей пока не проводилось.

Загружаемые технические отчеты

M. Stannett и A. J. H. Simons (2002) Полное поведенческое тестирование объектно-ориентированных систем с использованием CCS Augmented X Machines. Технический отчет CS 02 06, кафедра информатики, Университет Шеффилда. Скачать
J. Aguado и A. J. Cowling (2002) Основы теории X-машин для тестирования. Технический отчет CS 02 06, кафедра информатики, Университет Шеффилда. Скачать
J. Aguado и A. J. Cowling (2002) Системы взаимодействующих X-машин для спецификации распределенных систем. Технический отчет CS 02 07, кафедра информатики, Университет Шеффилда. Скачать
M. Stannett (2005) Теория X-машин, часть 1. Технический отчет CS 05 09, кафедра информатики, Университет Шеффилда. Скачать