Stream X-Machine - Stream X-Machine

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

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

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

The Stream X-Machine

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

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

Отношение к Х-машинам

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

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

 Y = В* Z = Из*

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

 α (ins) = (<>, мем0, ins) β (выходы, мемп, <>) = выходы

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

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

 φ (выходы, мемя, в :: ins) = (выходы :: из, мемя + 1, ins)

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

Обработка и тестируемые свойства

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

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

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

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

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

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

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

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

  1. ^ а б Гилберт Лэйкок (1993) Теория и практика тестирования программного обеспечения на основе спецификаций. Кандидатская диссертация, Шеффилдский университет, факультет компьютерных наук. Абстрактный В архиве 2007-11-05 на Wayback Machine
  2. ^ Сэмюэл Эйленберг (1974) Автоматы, языки и машины, Vol. А. Лондон: Academic Press.
  3. ^ М. Холкомб (1988) «Х-машины как основа для спецификации динамических систем». Журнал программной инженерии 3 (2)С. 69-76.
  4. ^ а б Майк Холкомб и Флорентин Ипате (1998) Правильные системы - построение решения для бизнес-процессов. Серия прикладных вычислений. Берлин: Springer-Verlag.
  5. ^ а б Ф. Ипате и В. М. Л. Холкомб (1997) «Метод интеграционного тестирования, доказывающий, что он обнаруживает все ошибки». Int. J. Comp. Математика., 63, стр. 159-178.
  6. ^ Ф. Ипате и М. Холкомб (1998) «Метод уточнения и тестирования обобщенных спецификаций машин». Int. J. Comp. Математика. 68, pp. 197-219.