Икс-машина
X -машина ( XM ) — теоретическая модель вычислений, представленная Сэмюэлем Эйленбергом в 1974 году. [1] X в слове «X-машина» представляет фундаментальный тип данных, с которым работает машина; например, машина, которая работает с базами данных (объектами типа база данных ), будет машиной базы данных . Модель X-машины структурно аналогична конечному автомату используемые для обозначения переходов машины, обозначают отношения типа X → X. , за исключением того, что символы , Пересечение перехода эквивалентно применению помечающего его отношения (вычислению набора изменений типа данных X ), а прохождение пути в машине соответствует применению всех связанных отношений, одного за другим.
Оригинальная теория [ править ]
Оригинальная X-машина Эйленберга представляла собой совершенно общую теоретическую модель вычислений (включающую , например, машину Тьюринга ), которая допускала детерминированные, недетерминированные и незавершающиеся вычисления. Его плодотворная работа [1] опубликовал множество вариантов базовой модели X-машины, каждый из которых обобщал конечный автомат по-своему .
В самой общей модели X-машина по сути представляет собой «машину для манипулирования объектами типа X». Предположим, что X — некоторый тип данных , называемый фундаментальным типом данных , и что Φ — это набор (частичных) отношений φ: X → X. X-машина — это конечный автомат , стрелки которого помечены отношениями в Φ. В любом заданном состоянии один или несколько переходов могут быть разрешены, если область соответствующего отношения φ i принимает (подмножество) текущие значения, хранящиеся в X. Предполагается, что в каждом цикле все разрешенные переходы выполняются. Каждый распознанный путь через машину порождает список φ 1 ... φ n отношений. Композицию φ 1 o ... o φ n этих отношений мы называем отношением пути, соответствующим этому пути. Поведение . X-машины определяется как объединение всех поведений, вычисленных с помощью ее отношений пути В общем, это недетерминировано, поскольку применение любого отношения вычисляет набор результатов для X. В формальной модели все возможные результаты рассматриваются вместе, параллельно.
Для практических целей X-машина должна описывать некоторые конечные вычисления. Функция кодирования α: Y → X преобразует некоторый тип входных данных Y в исходное состояние X, а функция декодирования β: X → Z преобразует обратно из конечного состояния (состояний) X в некоторый тип выходных данных Z. Как только начальное состояние X заполнено, X-машина работает до завершения, а затем наблюдаются выходные данные. В общем, машина может зайти в тупик (быть заблокированной), или заблокироваться (никогда не останавливаться), или выполнить одно или несколько полных вычислений. По этой причине более поздние исследования были сосредоточены на детерминированных 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 ... з". Эти отношения активны только в том случае, если X содержит значения домена (поддеревья), с которыми они работают. Остальные отношения SkipIncrement и SkipSubExpr являются нулевыми (отношениями идентичности), включенными в дополнительных случаях.
Таким образом, машина Optimizer будет работать до завершения, сначала преобразуя тривиальные дополнения в приращения по месту (находясь в состоянии 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 . НАСА недавно обсуждало использование комбинации Communicating Stream X-Machines и расчета процессов WSCSS при проектировании и тестировании роевых спутниковых систем. [9]
Аналоговая машина X (AXM) [ править ]
непрерывного времени Самый ранний вариант, аналоговая X-машина ( 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-машин, спроектированных сверху вниз и протестированных снизу вверх. Этот подход к проектированию и тестированию по принципу «разделяй и властвуй» подкреплен доказательством правильной интеграции Флорентина Ипате: [16] что доказывает, что независимое тестирование многоуровневых машин эквивалентно тестированию составной системы.
Коммуникационная X-Machine (CXM) [ править ]
Самым ранним предложением параллельного подключения нескольких X-машин является модель Communicating X-machine ( CXM или COMX ) Джудит Барнард 1995 года. [17] [18] в котором машины соединены через именованные каналы связи (известные как порты ); эта модель существует как в дискретном, так и в реальном времени вариантах. [19] Более ранние версии этой работы не были полностью формальными и не отображали полные отношения ввода/вывода.
Аналогичный подход Communicating X-Machine с использованием буферизованной каналы были разработаны Петросом Кефаласом. [20] [21] Основное внимание в этой работе было уделено выразительности в составе компонентов. Возможность переназначать каналы означала, что некоторые теоремы тестирования из Stream X-Machines не были перенесены.
эти варианты рассмотрены Более подробно на отдельной странице.
Communicating Stream X-Machine (CSXM) [ править ]
Первая полностью формальная модель параллельной композиции X-машин была предложена в 1999 году Кристиной Вертан и Хорией Джорджеску. [22] основан на более ранних работах Филипа Берда и Энтони Коулинга по коммуникации автоматов. [23] В модели Вертана машины взаимодействуют косвенно, через общую коммуникационную матрицу (по сути, массив ячеек), а не напрямую через общие каналы.
Бэлэнеску, Коулинг, Джорджеску, Вертан и другие довольно подробно изучили формальные свойства этой модели CSXM. Могут быть показаны полные отношения ввода/вывода. Матрица связи устанавливает протокол для синхронной связи. Преимущество этого подхода в том, что он отделяет обработку каждой машины от ее связи, позволяя отдельно тестировать каждое поведение. Эта композиционная модель оказалась эквивалентной стандартной Stream X-Machine . [24] таким образом, используя более раннюю теорию тестирования, разработанную Холкомбом и Ипате.
этот вариант X-машины обсуждается Более подробно на отдельной странице.
Объект X-Machine (OXM) [ править ]
Кирилл Богданов и Энтони Саймонс разработали несколько вариантов X-машины для моделирования поведения объектов в объектно-ориентированных системах. [25] Эта модель отличается от подхода Stream X-Machine тем, что монолитный тип данных X распределяется и инкапсулируется в несколько объектов, которые последовательно составляются; и системы управляются вызовами и возвратами методов, а не входами и выходами. Дальнейшая работа в этой области касалась адаптации формальной теории тестирования в контексте наследования, которая разбивает пространство состояний суперкласса на расширенные объекты подкласса. [26]
Модель «X-машины, дополненной CCS» (CCSXM) была позже разработана Саймонсом и Стэннеттом в 2002 году для поддержки полного поведенческого тестирования объектно-ориентированных систем при наличии асинхронной связи. [27] Ожидается, что это будет иметь некоторое сходство с ; недавним предложением НАСА но окончательного сравнения двух моделей еще не проводилось.
См. также [ править ]
Технические отчеты, доступные для скачивания [ править ]
- М. Стэннетт и А.Дж. Саймонс (2002) Полное поведенческое тестирование объектно-ориентированных систем с использованием X-машин, дополненных CCS. Технический отчет CS-02-06, факультет компьютерных наук, Университет Шеффилда. Скачать
- Дж. Агуадо и А. Дж. Коулинг (2002) Основы теории X-машин для тестирования. Технический отчет CS-02-06, факультет компьютерных наук, Университет Шеффилда. Скачать
- Дж. Агуадо и А. Дж. Коулинг (2002) Системы связи X-машин для определения распределенных систем. Технический отчет CS-02-07, факультет компьютерных наук, Университет Шеффилда. Скачать
- М. Стэннетт (2005) Теория X-машин. Часть 1. Технический отчет CS-05-09, факультет компьютерных наук, Университет Шеффилда. Скачать
Внешние ссылки [ править ]
- http://www.dcs.shef.ac.uk/~ajc/csxms/index.html Тони Коулинга. коммуникационных систем SXM — страницы
- http://x-machines.com Майка Стэннета «Теория X-машин». — сайт
Ссылки [ править ]
- ↑ Перейти обратно: Перейти обратно: а б С. Эйленберг (1974) Автоматы, языки и машины, Vol. А. Академическое издательство, Лондон.
- ^ М. Холкомб (1988) «X-машины как основа спецификации динамических систем», Журнал программной инженерии 3 (2), стр. 69-76.
- ^ М. Холкомб (1988) «Формальные методы в спецификации человеко-машинного интерфейса», Международный J. Командование и управление, связь и информация. Системы. 2 , стр. 24-34.
- ^ М. Холкомб (1986) «Математические модели биохимии клетки». Технический отчет CS-86-4, факультет компьютерных наук, Шеффилдский университет.
- ^ М. Стэннетт (1987) «Организационный подход к принятию решений в системах управления». Международный J. Командование и управление, связь и информация. Системы. 1 , стр. 23-34.
- ↑ Перейти обратно: Перейти обратно: а б Гилберт Лэйкок (1993) Теория и практика тестирования программного обеспечения на основе спецификаций . Докторская диссертация, Университет Шеффилда. Аннотация. Архивировано 5 ноября 2007 г. в Wayback Machine.
- ↑ Перейти обратно: Перейти обратно: а б М. Холкомб и Ф. Ипате (1998) Правильные системы – построение решения для бизнес-процессов . Спрингер, Серия «Прикладные вычисления».
- ^ А. Белл и М. Холкомб (1996) «Вычислительные модели клеточной обработки», в книге «Вычисления в клеточных и молекулярных биологических системах» , под ред. М. Холкомб, Р. Пэтон и Р. Катбертсон, Сингапур, World Scientific Press.
- ↑ Перейти обратно: Перейти обратно: а б М.Г. Хинчи, К.А. Руфф, Дж.Л. Раш и В.Ф. Трушковски (2005) «Требования интегрированного формального метода для интеллектуальных роев», в материалах FMICS'05, 5–6 сентября 2005 г., Лиссабон, Португалия . Ассоциация вычислительной техники, стр. 125–133.
- ^ А. Корнаи (2009) Алгебра лексической семантики . Документ, представленный на заседании Ассоциации математики языка в 2009 году . В In C. Ebert, G. Jäger, J. Michaelis (ред.) Proc. 11-й семинар по математике языка (MOL11) Springer LNCS 6149 174-199 [1]
- ^ Г. Юэ и Б. Разет (2008) Учебное пособие «Вычисления на реляционных машинах», представленное на ICON, декабрь 2008 г., Пуна
«Архивная копия» (PDF) . Архивировано из оригинала (PDF) 19 февраля 2015 года . Проверено 7 августа 2013 г.
{{cite web}}: CS1 maint: архивная копия в заголовке ( ссылка ) - ^ П. Гоял, Г. Уэт, А. Кулкарни, П. Шарф, Р. Банкер (2012) «Распределенная платформа для обработки санскрита» в Proc. COLING 2012, стр. 1011–1028 [2]
- ^ М. Стэннетт (1990) «X-машины и проблема остановки: построение супермашины Тьюринга». Формальные аспекты вычислений 2 , стр. 331-41.
- ^ Би Джей Коупленд (2002) «Гиперкомпьютер». Умы и машины 12 , стр. 461–502.
- ^ Ф. Ипате и М. Холкомб (1998) «Метод уточнения и тестирования обобщенных характеристик машины». Межд. Дж. Комп. Математика. 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 , Школа вычислительной техники, Стаффордширский университет. (Гражданин)
- ^ Э. Керис, Г. Элефтеракис и П. Кефалас (2000) «Использование X-машин для моделирования и тестирования программ моделирования дискретных событий», Proc. 4-я Всемирная мультиконференция по схемам, системам, связи и компьютерам , Афины.
- ^ П. Кефалас, Г. Элефтеракис и Э. Керис (2000) «Связывающие X-машины: практический подход к модульной спецификации больших систем», Технический отчет CS-09/00, Факультет компьютерных наук , Городской колледж, Салоники.
- ^ Х. Джорджеску и К. Вертан (2000) «Новый подход к обмену потоковыми X-машинами», Journal of Universal Computer Science 6 (5) , стр. 490-502.
- ^ PR Bird и Эй Джей Коулинг (1994) «Моделирование логического программирования с использованием сети взаимодействующих машин», в Учеб. 2-й семинар Euromicro по параллельной и распределенной обработке, Малага, 26–28 января 1994 г. , стр. 156–161. Абстрактный
- ^ Т.Баланеску, А.Дж. Коулинг, Х. Джорджеску, М. Георге, М. Холкомб и К. Вертан (1999) «Связывающиеся системы X-машин - не более чем X-машины», Журнал Universal 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, стр. 133-156.
- ^ М. Стэннетт и AJH Саймонс (2002) «X-машины с дополненной CCS», Технический отчет CS-2002-04, факультет компьютерных наук , Шеффилдский университет, Великобритания.