Jump to content

Стрим X-Машина

Stream X-машина ( SXM ) — это модель вычислений, представленная Гилбертом Лэйкоком в его докторской диссертации 1993 года « Теория и практика тестирования программного обеспечения на основе спецификаций» . [1] Основанный на Сэмюэля Эйленберга , X-машине расширенном конечном автомате для обработки данных типа X , [2] Stream X-Machine — это разновидность X-машины для обработки данных памяти типа Mem со связанными с ними входными и выходными потоками In * и Out *, то есть где X = Out * × Mem × In *. Переходы Stream X-Machine помечаются функциями вида φ: Mem × In Out × Mem , то есть которые вычисляют выходное значение и обновляют память из текущей памяти и входного значения.

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

Из-за интуитивной интерпретации Stream X-Machines как «агентов обработки с входами и выходами» они вызывают растущий интерес из-за их полезности для моделирования явлений реального мира. Модель SXM имеет важные применения в таких разнообразных областях, как вычислительная биология , тестирование программного обеспечения и агентная вычислительная экономика .

Stream X-Machine [ править ]

Stream X-Machine (SXM) — это расширенный конечный автомат со вспомогательной памятью, входами и выходами. Это вариант общей X-машины , в которой фундаментальный тип данных X = Out Mem × In *, то есть кортеж, состоящий из выходного потока, памяти и входного потока. SXM отделяет поток управления системой от обработки , выполняемой системой. Управление моделируется конечным автоматом (известным как ассоциированный автомат ), переходы которого помечены функциями обработки, выбранными из набора Φ (известного как тип автомата ), которые действуют на фундаментальный тип данных.

Каждая функция обработки в Φ является частичной функцией и может рассматриваться как имеющая тип φ: Mem × In Out × Mem , где Mem — тип памяти, а In и Out — соответственно типы ввода и вывода. В любом заданном состоянии переход возможен , если область определения связанной функции φ i включает в себя следующее входное значение и текущее состояние памяти. Если (максимум) один переход разрешен в данном состоянии, машина является детерминированной . Пересечение перехода эквивалентно применению связанной функции φ i , которая потребляет один вход, возможно, изменяет память и производит один выход. Таким образом, каждый распознанный путь через машину генерирует список функций φ 1 ... φ n , а SXM компонует эти функции вместе, чтобы сгенерировать отношение к фундаментальному типу данных |φ 1 ... φ n |: X X .

- с X Связь машинами

Stream X-Machine — это вариант X-машины , в котором основной тип данных X = Out * × Mem × In *. В исходной X-машине φ i являются отношениями на X. общими В Stream X-Machine они обычно ограничиваются функциями ; однако SXM по-прежнему является детерминированным только в том случае, если (максимум) один переход включен в каждом состоянии.

Обычная X-машина обрабатывает ввод и вывод, используя априорную функцию кодирования α: Y X для ввода и апостериорную функцию декодирования β: X Z для вывода, где Y и Z — соответственно типы ввода и вывода. В Stream X-Machine потоками являются следующие типы:

 Y = In*
 Z = Out*

а функции кодирования и декодирования определяются как:

 α(ins) = (<>, mem0, ins)
 β(outs, memn, <>) = outs

где ins: In *, outs: Out * и mem i : Mem . Другими словами, машина инициализируется всем входным потоком; и декодированный результат — это весь выходной поток при условии, что входной поток в конечном итоге будет использован (в противном случае результат не определен).

Каждой функции обработки в SXM присваивается сокращенный тип φ SXM : Mem × In Out × Mem . Это можно отобразить на общее X-машинное отношение типа φ: X → X, если мы рассматриваем это как вычисление:

 φ(outs, memi, in :: ins) = (outs :: out, memi+1, ins)

где :: обозначает объединение элемента и последовательности. Другими словами, отношение извлекает начало входного потока, изменяет память и добавляет значение в конец выходного потока.

и тестирования Свойства обработки

Из-за вышеуказанной эквивалентности внимание может быть сосредоточено на том, как Stream X-Machine обрабатывает входные данные в выходные, используя вспомогательную память. Учитывая начальное состояние памяти mem 0 и входной поток ins , машина работает поэтапно, потребляя по одному вводу за раз и генерируя по одному выводу за раз. При условии, что существует (по крайней мере) один распознанный путь path = φ 1 ... φ n , ведущий к состоянию, в котором входные данные были использованы, машина выдает конечное состояние памяти mem n и выходной поток outs . В общем, мы можем думать об этом как об отношении, вычисляемом всеми распознаваемыми путями: | путь | : Вход * → Выход *. Это часто называют поведением Stream X-Machine.

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

Холкомб и Ипат развили это в практическую теорию тестирования программного обеспечения. [4] который был полностью композиционным и масштабировался до очень больших систем. [6] Доказательство правильной интеграции [5] гарантирует, что тестирование каждого компонента и каждого уровня интеграции в отдельности соответствует тестированию всей системы. Такой подход «разделяй и властвуй» делает возможным исчерпывающее тестирование больших систем.

Метод тестирования описан в отдельной статье о методологии тестирования Stream X-Machine .

См. также [ править ]

  • X-machines , общее описание модели X-machine, включая простой пример.
  • Методология тестирования Stream X-Machine комплексная методика функционального тестирования . Используя эту методологию, можно определить конечный набор тестов, которые исчерпывающе определяют, соответствует ли реализация своей спецификации. Этот метод преодолевает формальные ограничения неразрешимости, настаивая на том, чтобы пользователи применяли тщательно определенный дизайн принципов тестирования во время реализации.
  • Communicating Stream X-Machines (CSXM) , параллельная версия модели SXM, имеющая применение в самых разных областях: от социальных насекомых до экономики.

Внешние ссылки [ править ]

Ссылки [ править ]

  1. Перейти обратно: Перейти обратно: а б Гилберт Лэйкок (1993) Теория и практика тестирования программного обеспечения на основе спецификаций . Докторская диссертация, Университет Шеффилда, факультет компьютерных наук. Аннотация. Архивировано 5 ноября 2007 г. в Wayback Machine.
  2. ^ Сэмюэл Эйленберг (1974) Автоматы, языки и машины, Vol. А. ​ Лондон: Академическая пресса.
  3. ^ М. Холкомб (1988) «X-машины как основа спецификации динамических систем». Журнал программной инженерии 3 (2) , стр. 69-76.
  4. Перейти обратно: Перейти обратно: а б Майк Холкомб и Флорентин Ипате (1998) Правильные системы – построение решения бизнес-процессов . Серия «Прикладные вычисления». Берлин: Springer-Verlag.
  5. Перейти обратно: Перейти обратно: а б Ф. Ипате и У.М.Л. Холкомб (1997) «Метод интеграционного тестирования, который, как доказано, обнаруживает все ошибки». Межд. Дж. Комп. Математика. , 63 , стр. 159-178.
  6. ^ Ф. Ипате и М. Холкомб (1998) «Метод уточнения и тестирования обобщенных характеристик машины». Межд. Дж. Комп. Математика. 68 , стр. 197-219.
Arc.Ask3.Ru: конец переведенного документа.
Arc.Ask3.Ru
Номер скриншота №: 81c45e8b1ed968cb097f0cd1c3396593__1627129740
URL1:https://arc.ask3.ru/arc/aa/81/93/81c45e8b1ed968cb097f0cd1c3396593.html
Заголовок, (Title) документа по адресу, URL1:
Stream X-Machine - Wikipedia
Данный printscreen веб страницы (снимок веб страницы, скриншот веб страницы), визуально-программная копия документа расположенного по адресу URL1 и сохраненная в файл, имеет: квалифицированную, усовершенствованную (подтверждены: метки времени, валидность сертификата), открепленную ЭЦП (приложена к данному файлу), что может быть использовано для подтверждения содержания и факта существования документа в этот момент времени. Права на данный скриншот принадлежат администрации Ask3.ru, использование в качестве доказательства только с письменного разрешения правообладателя скриншота. Администрация Ask3.ru не несет ответственности за информацию размещенную на данном скриншоте. Права на прочие зарегистрированные элементы любого права, изображенные на снимках принадлежат их владельцам. Качество перевода предоставляется как есть. Любые претензии, иски не могут быть предъявлены. Если вы не согласны с любым пунктом перечисленным выше, вы не можете использовать данный сайт и информация размещенную на нем (сайте/странице), немедленно покиньте данный сайт. В случае нарушения любого пункта перечисленного выше, штраф 55! (Пятьдесят пять факториал, Денежную единицу (имеющую самостоятельную стоимость) можете выбрать самостоятельно, выплаичвается товарами в течение 7 дней с момента нарушения.)