Х-машина ( ХМ ) является теоретической моделью расчета представлен Эйленбергом в 1974 году [1] Х в «X-машине» представляет тип фундаментальных данных , на которой работает машина; например, машина, которая работает с базами данных (объектами типа база данных ), будет машиной базы данных . Модель X-машины структурно такая же, как и конечный автомат , за исключением того, что символы, используемые для обозначения переходов машины, обозначают отношения типа X → X. Пересечение перехода эквивалентно применению отношения, которое его маркирует (вычисление набора изменений к типу данных X ), а прохождение пути в машине соответствует применению всех связанных отношений, одного за другим.
Оригинальная теория
Первоначальная X-машина Эйленберга была полностью общей теоретической моделью вычислений (например, включающей машину Тьюринга ), которая допускала детерминированные, недетерминированные и неограниченные вычисления. Его основополагающая работа [1] опубликовала множество вариантов базовой модели X-машины, каждый из которых обобщал конечный автомат несколько иначе.
В наиболее общей модели X-машина по сути является «машиной для манипулирования объектами типа X». Предположим, что X - некоторый тип данных , называемый фундаментальным типом данных , и что Φ - это набор (частичных) отношений φ: X → X. X-машина - это конечный автомат , стрелки которого помечены отношениями в Φ. В любом заданном состоянии один или несколько переходов могут быть разрешены, если домен ассоциированного отношения φ i принимает (подмножество) текущие значения, хранящиеся в X. В каждом цикле предполагается, что все разрешенные переходы выполняются. Каждый распознанный путь через машину создает список отношений φ 1 ... φ n . Мы называем композицию φ 1 o ... o φ n этих отношений отношением пути, соответствующим этому пути. Поведение Х-машины определяется как объединение всех поведений , вычисленных по его пути отношений. В общем, это недетерминировано, поскольку применение любого отношения вычисляет набор результатов на X. В формальной модели все возможные результаты рассматриваются вместе, параллельно.
Для практических целей X-машина должна описывать некоторые конечные вычисления. Функция кодирования α: Y → X преобразует некоторый тип входных данных Y в начальное состояние X, а функция декодирования β: X → Z преобразует обратно из конечного состояния (й) X в некоторый тип выходных данных Z. Как только начальное состояние X заполнено, X-машина работает до завершения, а затем наблюдаются выходы. В общем, машина может быть заблокирована (заблокирована), livelock (никогда не останавливаться) или выполнить одно или несколько полных вычислений. По этой причине недавние исследования были сосредоточены на детерминированных X-машинах, поведение которых можно контролировать и наблюдать более точно.
Пример
Компилятор с оптимизатором «глазок» можно рассматривать как машину для оптимизации структуры программы. В этой машине- оптимизаторе функция кодирования α берет исходный код из типа ввода Y (источник программы) и загружает его в тип памяти X (дерево синтаксического анализа). Предположим, что машина имеет несколько состояний, называемых FindIncrements , FindSubExprs и Completed . Машина запускается в начальном состоянии FindIncrements , которое связано с другими состояниями через переходы:
FindIncrements → DoIncrement FindIncrements FindIncrements → SkipIncrement FindSubExprs FindSubExprs → DoSubExpr FindSubExprs FindSubExprs → SkipSubExpr Completed
Отношение DoIncrement отображает проанализированное поддерево, соответствующее «x: = x + 1», в оптимизированное поддерево «++ x». Отношение DoSubExpr отображает дерево синтаксического анализа, содержащее несколько вхождений одного и того же выражения «x + y ... x + y», в оптимизированную версию с локальной переменной для хранения повторяющихся вычислений «z: = x + y; ... z ... z ". Эти отношения доступны только в том случае, если X содержит значения домена (поддеревья), с которыми они работают. Остальные отношения SkipIncrement и SkipSubExpr - это пустые значения (отношения идентичности), включенные в дополнительных случаях.
Итак, оптимизатор- машина будет работать до конца, сначала преобразуя тривиальные добавления в приращения на месте (находясь в состоянии FindIncrements ), затем она перейдет в состояние FindSubExprs и выполнит серию общих удалений подвыражений, после чего он перейдет в окончательное состояние " Завершено" . Затем функция декодирования β отобразит из типа памяти X (оптимизированное дерево синтаксического анализа) в выходной тип Z (оптимизированный машинный код).
соглашение
Ссылаясь на исходную модель Эйленберга, «X-машина» обычно пишется с строчной буквы «m», потому что смысл - «любая машина для обработки X». Обращаясь к более поздним конкретным моделям, принято использовать заглавную букву «М» как часть собственного имени этого варианта.
1980-е
Интерес к X-машине возродился в конце 1980-х Майком Холкомбом [2], который заметил, что эта модель идеально подходит для формальной спецификации программного обеспечения , поскольку она четко отделяет поток управления от обработки . При условии, что кто-то работает на достаточно абстрактном уровне, потоки управления в вычислениях обычно могут быть представлены как конечный автомат, поэтому для завершения спецификации X-машины все, что остается, - это указать обработку, связанную с каждым из переходов машины. Конструктивная простота модели делает ее чрезвычайно гибкой; другие ранние иллюстрации идеи включали спецификацию Холкомба интерфейсов человек-компьютер [3], его моделирование процессов в биохимии клетки [4] и моделирование Стэннеттом принятия решений в системах военного управления. [5]
1990-е годы
X-машины привлекли к себе новое внимание с середины 1990-х, когда было обнаружено, что детерминированная Stream X-Machine Гилберта Лэйкока [6] служит основой для определения больших программных систем, которые можно полностью тестировать. [7] Другой вариант, Communicating Stream X-Machine, предлагает полезную тестируемую модель для биологических процессов [8] и будущих спутниковых систем, основанных на роях. [9]
2000-е
X-машины были применены к лексической семантике по Андраш Корнай , которые модель слово , означающим на `заостренных» машины , которые имеют один член базового набора X отличается. [10] Применение к другим отраслям лингвистики, в частности к современной переформулировке Панини, было впервые применено Жераром Хуэ и его сотрудниками [11] [12]
Основные варианты
X-машина редко встречается в ее первоначальном виде, но лежит в основе нескольких последующих моделей вычислений. Наибольшее влияние на теории тестирования программного обеспечения оказала Stream X-Machine . НАСА недавно обсудило использование комбинации Коммуникационных потоковых X-Machines и расчета процессов WSCSS при проектировании и тестировании роевых спутниковых систем. [9]
Аналоговый X Machine (AXM)
Самый ранний вариант, Аналоговая Х-машина непрерывного времени ( AXM ), был представлен Майком Стэннеттом в 1990 году как потенциально «супер-Тьюринговая» модель вычислений; [13], следовательно, это связано с работой в теории гиперкомпьютеров . [14]
Stream X-Machine (SXM)
Наиболее часто встречающимся вариантом X-машины является модель Stream X-Machine ( SXM ) 1993 года Гилберта Лэйкока [6], которая составляет основу теории полного тестирования программного обеспечения Майка Холкомба и Флорентина Ипате , которая гарантирует известные свойства корректности после завершения тестирования. . [7] [15] Stream X-Machine отличается от исходной модели Эйленберга тем, что основной тип данных X имеет форму Out * × Mem × In *, где In * - входная последовательность, Out * - выходная последовательность. , а Mem - это (остальная) память.
Преимущество этой модели состоит в том, что она позволяет управлять системой, шаг за шагом, через ее состояния и переходы, наблюдая выходы на каждом шаге. Это значения-свидетели, которые гарантируют выполнение определенных функций на каждом шаге. В результате сложные программные системы могут быть разложены на иерархию Stream X-Machines, спроектированную сверху вниз и протестированную снизу вверх. Такой подход «разделяй и властвуй» к проектированию и тестированию подкреплен доказательством правильной интеграции Флорентин Ипате [16], которое доказывает, что независимое тестирование многоуровневых машин эквивалентно тестированию составной системы.
Связь X-Machine (CXM)
Самым ранним предложением по параллельному соединению нескольких X-машин является модель Джудит Барнард 1995 г. с коммуникационной X-машиной ( CXM или COMX ) [17] [18], в которой машины соединяются через названные каналы связи (известные как порты ); эта модель существует как в дискретном, так и в реальном времени. [19] Ранние версии этой работы не были полностью формальными и не отображали полные отношения ввода / вывода.
Похожий подход к взаимодействию X-Machine с использованием буферизованных каналов был разработан Петросом Кефаласом. [20] [21] Основное внимание в этой работе уделялось выразительности композиции компонентов. Возможность переназначить каналы означала, что некоторые тестовые теоремы Stream X-Machines не были перенесены.
Более подробно эти варианты обсуждаются на отдельной странице.
Обмен данными Stream X-Machine (CSXM)
Первая полностью формальная модель параллельной композиции X-машин была предложена в 1999 году Кристиной Вертан и Хориа Георгеску [22] на основе более ранней работы Филипа Берда и Энтони Коулинга по взаимодействующим автоматам. [23] В модели Вертана машины взаимодействуют косвенно, через общую матрицу связи (по сути, массив ячеек), а не напрямую через общие каналы.
Бэлэнеску, Коулинг, Джорджеску, Вертан и другие довольно подробно изучили формальные свойства этой модели CSXM. Могут быть показаны полные отношения ввода / вывода. Матрица связи устанавливает протокол для синхронной связи. Преимущество этого заключается в том, что он отделяет обработку каждой машины от их связи, что позволяет проводить отдельное тестирование каждого поведения. Эта композиционная модель была доказана эквивалентна стандартной поток X-Machine , [24] это с использованием ранее тестирования теории , разработанной Холкомбами и Ипате.
Более подробно этот вариант Х-машины обсуждается на отдельной странице.
Объект X-Machine (OXM)
Кирилл Богданов и Энтони Саймонс разработали несколько вариантов X-машины для моделирования поведения объектов в объектно-ориентированных системах. [25] Эта модель отличается от подхода Stream X-Machine тем , что монолитный тип данных X распределен и инкапсулирован несколькими объектами, которые составлены последовательно; и системы управляются вызовами и возвратами методов, а не входами и выходами. Дальнейшая работа в этой области касалась адаптации формальной теории тестирования в контексте наследования, которое разделяет пространство состояний суперкласса на объекты расширенного подкласса. [26]
Модель «CCS-augmented X-machine» (CCSXM) была позже разработана Саймонсом и Стэннеттом в 2002 году для поддержки полного поведенческого тестирования объектно-ориентированных систем при наличии асинхронной связи [27]. Ожидается, что она будет иметь некоторое сходство с Недавнее предложение НАСА ; но окончательного сравнения этих двух моделей пока не проводилось.
Смотрите также
- Stream X-Machine
- X-Machine Тестирование
- Общение X-Machine
Загружаемые технические отчеты
- M. Stannett и AJH Simons (2002) Полное поведенческое тестирование объектно-ориентированных систем с использованием CCS-Augmented X-Machines. Технический отчет CS-02-06, факультет компьютерных наук, Шеффилдский университет. Скачать
- J. Aguado и AJ Cowling (2002) Основы теории X-машины для тестирования. Технический отчет CS-02-06, факультет компьютерных наук, Шеффилдский университет. Скачать
- Дж. Агуадо и А. Дж. Каулинг (2002) Системы взаимодействия X-машин для определения распределенных систем. Технический отчет CS-02-07, факультет компьютерных наук, Шеффилдский университет. Скачать
- М. Станнетт (2005) Теория X-Machines - Часть 1. Технический отчет CS-05-09, Департамент компьютерных наук, Университет Шеффилда. Скачать
Внешние ссылки
- http://www.dcs.shef.ac.uk/~ajc/csxms/index.html - страницы Tony Cowling, посвященные коммуникационным системам SXM
- http://x-machines.com - Сайт Майка Стэннета по теории X-Machines
Рекомендации
- ^ a b С. Эйленберг (1974) Автоматы, языки и машины, Vol. . Academic Press, Лондон.
- ^ М. Холкомб (1988) «X-машины как основа для спецификации динамических систем», Software Engineering Journal 3 (2), стр. 69-76.
- ^ М. Холкомб (1988) «Формальные методы в спецификации интерфейса человек-машина», International J. Command and Control, Communications and Info. Системы. 2. С. 24-34.
- ^ М. Холкомб (1986) «Математические модели клеточной биохимии». Технический отчет CS-86-4, факультет компьютерных наук, Шеффилдский университет.
- ^ М. Станнетт (1987) «Организационный подход к принятию решений в командных системах». Интернэшнл Дж. Командование и управление, связь и информация. Системы. 1. С. 23-34.
- ^ a b Гилберт Лэйкок (1993) Теория и практика тестирования программного обеспечения на основе спецификаций . Докторская диссертация, Шеффилдский университет. Резюме. Архивировано 5 ноября 2007 года в Wayback Machine.
- ^ a b М. Холкомб и Ф. Ипате (1998) Правильные системы - Построение решения для бизнес-процессов . Springer, Серия прикладных вычислений.
- ^ А. Белл и М. Холкомб (1996) «Вычислительные модели клеточного процесса», в « Вычисления в клеточных и молекулярных биологических системах» , под ред. М. Холкомб, Р. Патон и Р. Катбертсон, Сингапур, World Scientific Press.
- ^ a b MG Hinchey, CA Rouff, JL Rash и WF Truszkowski (2005) «Требования интегрированного формального метода для интеллектуальных роев», в Proceedings of FMICS'05, 5–6 сентября 2005 г., Лиссабон, Португалия . Ассоциация вычислительной техники, стр. 125-133.
- ^ А. Корнаи (2009) Алгебра лексической семантики . Документ, представленный на заседании Ассоциации математики языка 2009 года. В In C. Ebert, G. Jager, J. Michaelis (eds) Proc. 11-й семинар по математике языка (MOL11) Springer LNCS 6149 174-199 [1]
- ^ G. Huet и B. Razet (2008) "Вычисления на реляционных машинах" Учебное пособие, представленное на ICON, декабрь 2008 г., Пуна "Архивная копия" (PDF) . Архивировано из оригинального (PDF) 19 февраля 2015 года . Проверено 7 августа 2013 года .CS1 maint: заархивированная копия как заголовок ( ссылка )
- ^ П. Гоял, Г. Хуэт, А. Кулькарни, П. Шарф, Р. Бункер (2012) «Распределенная платформа для обработки санскрита» В Proc. COLING 2012, стр. 1011–1028 [2]
- ^ М. Станнетт (1990) «Х-машины и проблема остановки: создание супер-машины Тьюринга». Формальные аспекты вычислений 2 , стр. 331-41.
- ↑ BJ Copeland (2002) «Гипервычисления». Умы и машины 12 , стр. 461-502.
- ^ Ф. Ипате и М. Холкомб (1998) «Метод уточнения и тестирования обобщенных спецификаций машин». Int. J. Comp. Математика. 68 , стр. 197-219.
- ^ Ф. Ипате и М. Холкомб (1997) «Метод интеграционного тестирования, доказывающий, что он находит все ошибки», Международный журнал компьютерной математики 63 , стр. 159-178.
- ^ Дж. Барнард, К. Тикер, Дж. Уитворт и М. Вудворд (1995) «Коммуникационные X-машины в реальном времени для формального проектирования систем реального времени», в Proceedings of DARTS '95, Universite Libre, Брюссель, Бельгия, 9–11 ноября 2005 г.
- ^ Дж. Барнард (1996) COMX: методология формального проектирования компьютерных систем с использованием коммуникационных X-машин . Кандидатская диссертация, Стаффордширский университет.
- ^ А. Алдерсон и Дж. Барнард (1997) «О создании безопасного перехода», технический отчет SOCTR / 97/01 , Школа вычислительной техники, Стаффордширский университет. (Citeseer)
- ^ Э. Кехрис, Г. Элефтеракис и П. Кефалас (2000) «Использование X-машин для моделирования и тестирования программ моделирования дискретных событий», Proc. 4-я всемирная мультиконференция по схемам, системам, связи и компьютерам , Афины.
- ^ П. Кефалас, Г. Элефтеракис и Э. Кехрис (2000) «Коммуникационные X-машины: практический подход для модульной спецификации больших систем», Технический отчет CS-09/00, Департамент компьютерных наук , Городской колледж, Салоники.
- ^ Х. Джорджеску и К. Вертан (2000) «Новый подход к передаче потоковых X-машин», Journal of Universal Computer Science 6 (5) , стр. 490-502.
- ^ PR Bird и AJ Cowling (1994) «Моделирование логического программирования с использованием сети сообщающихся машин», в Proc. 2-й семинар Euromicro по параллельной и распределенной обработке, Малага, 26–28 января 1994 г. , стр. 156-161. Абстрактный
- ^ T.Balanescu, AJ передок, Х. Георгеска, М. Георге, М. Холкомбы и С. Вертан (1999) «Связи X-машины система не болеечем Х-машин», журнал Юниверсал Computer Science , 5 (9 ) , стр. 494-507.
- ^ AJH Simons, KE Bogdanov и WML Holcombe (2001) 'Полное функциональное тестирование с использованием объектных машин', Технический отчет CS-01-18, Департамент компьютерных наук , Университет Шеффилда
- ^ AJH Simons (2006) «Теория регрессионного тестирования для поведенчески совместимых типов объектов», Software Testing, Verification and Reliability , 16 (3) , John Wiley, pp. 133-156.
- ^ М. Stannett и AJH Simons (2002) 'CCS дополненная X-Machines', технический отчет CS-2002-04, факультет компьютерных наук , Sheffield University, Великобритания.