X-машина - X-machine

В X-машина (XM) представляет собой теоретическую модель вычисление представлен Сэмюэл Эйленберг в 1974 г.[1]В Икс в «X-machine» представляет основной тип данных, на котором работает машина; например, машина, которая работает с базами данных (объекты типа база данных) будет база данных-машина. Модель X-machine конструктивно такая же, как и модель конечный автомат, за исключением того, что символы, используемые для обозначения переходов машины, обозначают связи типа Икс→Икс. Пересечение перехода эквивалентно применению отношения, которое его маркирует (вычисление набора изменений типа данных Икс), а прохождение пути в машине соответствует применению всех связанных соотношений одно за другим.

Оригинальная теория

Первоначальная X-машина Эйленберга была полностью общей теоретической моделью вычислений (включающей Машина Тьюринга, например), который допускал детерминированные, недетерминированные и неограниченные вычисления. Его основополагающая работа [1] опубликовали множество вариантов базовой модели Х-машины, каждый из которых обобщал конечный автомат немного по-другому.

В наиболее общей модели X-машина по сути является «машиной для манипулирования объектами типа X». Предположим, что X - некоторая тип данных, называется основной тип данных, и что Φ набор (частичных) соотношений φ: X → X. X-машина - это конечный автомат стрелки которого помечены соотношениями из Φ. В любом данном состоянии может быть один или несколько переходов. включено если домен ассоциированного отношения φя принимает (подмножество) текущие значения, хранящиеся в X. Предполагается, что в каждом цикле выполняются все разрешенные переходы. Каждый распознанный путь через машину формирует список φ1 ... φп отношений. Назовем композицию φ1 о ... о φп этих отношений отношение пути соответствующий этому пути. В поведение X-машины определяется как объединение всех поведений, вычисленных ее отношениями путей. В общем, это недетерминировано, поскольку применение любого отношения вычисляет набор результатов на X. В формальной модели все возможные результаты рассматриваются вместе, параллельно.

Для практических целей X-машина должна описывать некоторые конечные вычисления. Кодирующая функция α: Y → X преобразуется из некоторого Вход тип данных Y в начальное состояние X, а функция декодирования β: X → Z преобразует обратно из конечного состояния (состояний) X в некоторое выход тип данных Z. Как только начальное состояние X заполнено, X-машина работает до завершения, а затем наблюдаются выходы. Как правило, машина может блокироваться (блокироваться) или постоянно блокироваться (никогда не останавливаться), либо выполнять одно или несколько полных вычислений. По этой причине недавние исследования были сосредоточены на детерминированных X-машинах, поведение которых можно контролировать и наблюдать более точно.

Пример

Компилятор с оптимизатором для глаз можно рассматривать как машину для оптимизации структуры программы. В этом Оптимизатор-машине функция кодирования α берет исходный код из типа ввода Y (источник программы) и загружает его в тип памяти X (дерево синтаксического анализа). Предположим, что машина имеет несколько состояний, называемых FindIncrements, FindSubExprs и Завершенный. Машина запускается в исходном состоянии FindIncrements, который связан с другими состояниями через переходы:

 FindIncrements →DoIncrement FindIncrements FindIncrements →SkipIncrement FindSubExprs FindSubExprs →DoSubExpr FindSubExprs FindSubExprs →SkipSubExpr Завершенный

Соотношение DoIncrement отображает проанализированное поддерево, соответствующее «x: = x + 1», в оптимизированное поддерево «++ x». Соотношение DoSubExpr отображает дерево синтаксического анализа, содержащее несколько вхождений одного и того же выражения «x + y ... x + y», в оптимизированную версию с локальной переменной для хранения повторных вычислений «z: = x + y; ... z ... z ". Эти отношения доступны только в том случае, если X содержит значения домена (поддеревья), с которыми они работают. Остальные отношения SkipIncrement и SkipSubExpr находятся нуллопс (отношения идентичности) включены в дополнительных случаях.

Итак Оптимизатор-machine будет работать до завершения, сначала преобразуя тривиальные добавления в приращения на месте (в то время как FindIncrements состояние), затем он перейдет к FindSubExprs состояние и выполнить серию общих удалений подвыражения, после чего оно перейдет в конечное состояние Завершенный. Функция декодирования β затем отобразит из типа памяти X (оптимизированное дерево синтаксического анализа) в выходной тип Z (оптимизированный машинный код).

соглашение

Ссылаясь на исходную модель Эйленберга, «X-машина» обычно пишется со строчной буквы «m», потому что смысл - «любая машина для обработки X». Обращаясь к более поздним конкретным моделям, принято использовать заглавную букву «М» как часть собственного имени этого варианта.

1980-е

Интерес к X-машине возродил в конце 1980-х Майк Холкомб,[2] кто заметил что модель идеальна для софта формальная спецификация целей, потому что он четко разделяет поток управления из обработка. При условии, что кто-то работает на достаточно абстрактном уровне, потоки управления в вычислениях обычно могут быть представлены как конечный автомат, поэтому для завершения спецификации X-машины все, что остается, - это указать обработку, связанную с каждым из переходов машины. Конструктивная простота модели делает ее чрезвычайно гибкой; другие ранние иллюстрации идеи включали спецификацию Холкомба человеко-компьютерных интерфейсов,[3]его моделирование процессов в биохимии клетки,[4]и модели Стэннетта принятия решений в системах военного управления.[5]

1990-е годы

Икс-машины вновь привлекли к себе внимание с середины 1990-х годов, когда детерминированная теория Гилберта Лейкока Stream X-Machine[6] было установлено, что служит основой для определения больших программных систем, которые полностью проверяемый.[7] Другой вариант, Общение Stream X-Machine предлагает полезную тестируемую модель для биологических процессов[8] и будущее рой спутниковые системы.[9]

2000-е

X-машины были применены к лексическая семантика к Андраш Корнаи, который моделирует значение слов "остроконечными" машинами, у которых выделен один член базового множества X.[10] Применение к другим отраслям лингвистики, в частности к современной переформулировке Панини были первыми Жерар Юэ и его сотрудники[11][12]

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

X-машина редко встречается в ее первоначальном виде, но лежит в основе нескольких последующих моделей вычислений. Самой влиятельной моделью в теории тестирования программного обеспечения была Stream X-Machine. НАСА недавно обсуждал использование комбинации Обмен данными Stream X-Machines и процесс расчета WSCSS при разработке и тестировании спутник роя системы.[9]

Аналоговый X Machine (AXM)

Самый ранний вариант, непрерывный Аналоговый X-Machine (AXM), была представлена ​​Майком Стэннеттом в 1990 году как потенциально «супер-Тьюринговая» модель вычислений;[13]следовательно, это связано с работой в гипервычисления теория.[14]

Stream X-Machine (SXM)

Основная статья: Stream X-Machine

Наиболее часто встречающийся вариант X-машины - это Гилберта Лэйкока 1993 года. Stream X-Machine (SXM ) модель,[6]который лежит в основе теории Майка Холкомба и Флорентина Ипате. полный тестирование программного обеспечения, которое гарантирует известные свойства корректности после завершения тестирования.[7][15] Stream X-Machine отличается от исходной модели Эйленберга тем, что основной тип данных X имеет форму Из* × Mem × В*, куда В* - входная последовательность, Из* - это выходная последовательность, а Mem это (остальная) память.

Преимущество этой модели состоит в том, что она позволяет управлять системой, шаг за шагом, через ее состояния и переходы, наблюдая выходы на каждом шаге. Это значения-свидетели, гарантирующие выполнение определенных функций на каждом шаге. В результате сложные программные системы могут быть разложены на иерархию Stream X-Machines, спроектированную сверху вниз и протестированную снизу вверх. Такой подход к проектированию и тестированию, основанный на принципах разделяй и властвуй, подкреплен доказательством правильной интеграции Флорентин Ипате.[16] что доказывает, что независимое тестирование многоуровневых машин эквивалентно тестированию составной системы.

Связь X-Machine (CXM)

"CXM" перенаправляется сюда. Для ангольского аэропорта с этим ИАТА код см. Камашило аэропорт.

Самым ранним предложением о параллельном подключении нескольких X-машин было предложение Джудит Барнард 1995 г. Общение X-machine (CXM или же COMX) модель,[17][18]в которых машины подключены через именованные каналы связи (известные как порты); эта модель существует как в дискретном, так и в реальном времени.[19] Более ранние версии этой работы не были полностью формальными и не отображали полные отношения ввода / вывода.

Похожий подход взаимодействия X-Machine с использованием буферизованных каналов был разработан Петросом Кефаласом.[20][21] Основное внимание в этой работе было уделено выразительности композиции компонентов. Возможность переназначить каналы означала, что некоторые тестовые теоремы Stream X-Machines не были перенесены.

Эти варианты обсуждаются более подробно на отдельной странице.

Обмен данными Stream X-Machine (CSXM)

Первая полностью формальная модель параллельной композиции X-машины была предложена в 1999 году Кристиной Вертан и Хорией Георгеску,[22] основан на более ранней работе Филипа Берда и Энтони Коулинга по взаимодействующим автоматам.[23] В модели Вертана машины обмениваются данными косвенно, через общую матрица связи (по сути, набор ячеек), а не напрямую через общие каналы.

Бэлэнеску, Коулинг, Георгеску, Вертан и другие довольно подробно изучили формальные свойства этой модели CSXM. Могут быть показаны полные отношения ввода / вывода. В матрица связи устанавливает протокол для синхронной связи. Преимущество этого заключается в том, что он отделяет обработку каждой машины от их связи, что позволяет проводить отдельное тестирование каждого поведения. Эта композиционная модель оказалась эквивалентной стандартной Stream X-Machine,[24] таким образом, используя более раннюю теорию тестирования, разработанную Холкомбом и Ипате.

Этот вариант X-машины обсуждается более подробно на отдельной странице.

Объект X-Machine (OXM)

Кирилл Богданов и Энтони Саймонс разработали несколько вариантов X-машины для моделирования поведения объектов в объектно-ориентированных системах.[25] Эта модель отличается от Stream X-Machine подход, заключающийся в том, что монолитный тип данных X распределен и инкапсулирован несколькими объектами, которые составлены последовательно; и системы управляются вызовами и возвратами методов, а не входами и выходами. Дальнейшая работа в этой области касалась адаптации формальной теории тестирования в контексте наследования, которое разделяет пространство состояний суперкласса на объекты расширенного подкласса.[26]

Модель «CCS-augmented X-machine» (CCSXM) была позже разработана Саймонсом и Стэннеттом в 2002 году для поддержки полного поведенческого тестирования объектно-ориентированных систем при наличии асинхронной связи.[27] Ожидается, что это будет иметь некоторое сходство с НАСА последнее предложение; но окончательного сравнения этих двух моделей пока не проводилось.

Смотрите также

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

  • М. Стэннетт и А. Дж. Х. Саймонс (2002) Полное поведенческое тестирование объектно-ориентированных систем с использованием CCS-Augmented X-Machines. Технический отчет CS-02-06, факультет компьютерных наук, Шеффилдский университет. Скачать
  • Дж. Агуадо и А. Дж. Коулинг (2002) Основы теории X-машины для тестирования. Технический отчет CS-02-06, факультет компьютерных наук, Шеффилдский университет. Скачать
  • Дж. Агуадо и А. Дж. Коулинг (2002) Системы взаимодействия X-машин для задания распределенных систем. Технический отчет CS-02-07, факультет компьютерных наук, Шеффилдский университет. Скачать
  • М. Стэннетт (2005) Теория X-Machines - Часть 1. Технический отчет CS-05-09, факультет компьютерных наук, Шеффилдский университет. Скачать

внешняя ссылка

Рекомендации

  1. ^ а б С. Эйленберг (1974) Автоматы, языки и машины, Vol. А. Academic Press, Лондон.
  2. ^ М. Холкомб (1988) «Х-машины как основа для спецификации динамических систем», Журнал программной инженерии 3(2), стр. 69-76.
  3. ^ М. Холкомб (1988) «Формальные методы в спецификации интерфейса человек-машина», Интернэшнл Дж. Командование и управление, связь и информация. Системы. 2С. 24-34.
  4. ^ М. Холкомб (1986) «Математические модели биохимии клетки». Технический отчет CS-86-4, факультет компьютерных наук, Шеффилдский университет.
  5. ^ М. Станнетт (1987) «Организационный подход к принятию решений в командных системах». Интернэшнл Дж. Командование и управление, связь и информация. Системы. 1С. 23-34.
  6. ^ а б Гилберт Лэйкок (1993) Теория и практика тестирования программного обеспечения на основе спецификаций. Докторская диссертация, Шеффилдский университет. Абстрактный В архиве 5 ноября 2007 г. Wayback Machine
  7. ^ а б М. Холкомб и Ф. Ипате (1998) Правильные системы - построение решения для бизнес-процессов. Springer, Серия прикладных вычислений.
  8. ^ А. Белл и М. Холкомб (1996) «Вычислительные модели клеточной обработки», в Вычисления в клеточных и молекулярных биологических системах, ред. М. Холкомб, Р. Патон и Р. Катбертсон, Сингапур, World Scientific Press.
  9. ^ а б М. Г. Хинчи, К. А. Рафф, Дж. Л. Раш и В. Ф. Трушковски (2005) «Требования интегрированного формального метода для интеллектуальных роев», в Материалы FMICS'05, 5–6 сентября 2005 г., Лиссабон, Португалия. Ассоциация вычислительной техники, стр. 125-133.
  10. ^ А. Корнаи (2009) Алгебра лексической семантики. Документ, представленный на заседании 2009 г. Ассоциация математики языка. В In C. Ebert, G. Jäger, J. Michaelis (eds) Proc. 11-й семинар по математике языка (MOL11) Springer LNCS 6149 174-199 [1]
  11. ^ G. Huet и B. Razet (2008) Учебное пособие «Вычисления на реляционных машинах», представленное на ICON, декабрь 2008 г., Пуна «Архивная копия» (PDF). Архивировано из оригинал (PDF) 19 февраля 2015 г.. Получено 7 августа, 2013.CS1 maint: заархивированная копия как заголовок (связь)
  12. ^ П. Гоял, Г. Хуэт, А. Кулкарни, П. Шарф, Р. Бункер (2012) «Распределенная платформа для обработки санскрита» В Proc. COLING 2012, стр. 1011–1028 [2]
  13. ^ М. Станнетт (1990) «Х-машины и проблема остановки: построение супер-машины Тьюринга». Формальные аспекты вычислений 2, стр. 331-41.
  14. ^ Б. Дж. Коупленд (2002) «Гипервычисления». Умы и машины 12С. 461-502.
  15. ^ Ф. Ипате и М. Холкомб (1998) «Метод уточнения и тестирования обобщенных спецификаций машин». Int. J. Comp. Математика. 68, pp. 197-219.
  16. ^ Ф. Ипате и М. Холкомб (1997) «Доказано, что метод интеграционного тестирования обнаруживает все ошибки», Международный журнал компьютерной математики 63, стр. 159-178.
  17. ^ Дж. Барнард, К. Тикер, Дж. Уитворт и М. Вудворд (1995) «Коммуникационные X-машины в реальном времени для формального проектирования систем реального времени», в Труды DARTS '95, Universite Libre, Брюссель, Бельгия, 9–11 ноября 2005 г.
  18. ^ Дж. Барнард (1996) COMX: методология формального проектирования компьютерных систем с использованием коммуникационных X-машин.. Докторская диссертация, Стаффордширский университет.
  19. ^ А. Алдерсон и Дж. Барнард (1997) «О создании безопасного перехода», Технический отчет SOCTR / 97/01, Школа вычислительной техники Стаффордширского университета. (Citeseer)
  20. ^ Э. Кехрис, Г. Элефтеракис и П. Кефалас (2000) «Использование X-машин для моделирования и тестирования программ моделирования дискретных событий», Proc. 4-я всемирная мультиконференция по схемам, системам, связи и компьютерам, Афины.
  21. ^ П. Кефалас, Г. Элефтеракис и Э. Кехрис (2000) «Связь X-машин: практический подход к модульной спецификации больших систем», Технический отчет CS-09/00, Департамент компьютерных наук, Городской колледж, Салоники.
  22. ^ Х. Георгеску и К. Вертан (2000) «Новый подход к передаче потоковых X-машин», Журнал универсальных компьютерных наук 6 (5)С. 490-502.
  23. ^ П. Р. Берд и А. Дж. Каулинг (1994) «Моделирование логического программирования с использованием сети сообщающихся машин», в Proc. 2-й семинар Euromicro по параллельной и распределенной обработке, Малага, 26–28 января 1994 г.С. 156-161. Абстрактный
  24. ^ Т. Баланеску, А. Дж. Коулинг, Х. Георгеску, М. Георге, М. Холкомб и К. Вертан (1999) «Связанные системы X-машин - это не более чем X-машины», Журнал универсальных компьютерных наук, 5 (9)С. 494-507.
  25. ^ А. Дж. Х. Саймонс, К. Е. Богданов и В. М. Л. Холкомб (2001) «Полное функциональное тестирование с использованием объектных машин», Технический отчет CS-01-18, Департамент компьютерных наук, Университет Шеффилда
  26. ^ А. Дж. Х. Саймонс (2006) «Теория регрессионного тестирования для поведенчески совместимых типов объектов», Тестирование, проверка и надежность программного обеспечения, 16 (3), Джон Уайли, стр. 133-156.
  27. ^ М. Стэннетт и А. Дж. Х. Саймонс (2002) «Х-машины с расширением CCS», Технический отчет CS-2002-04, Департамент компьютерных наук, Шеффилдский университет, Великобритания.