Стрим 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-х годах общая Х-машина была определена как потенциально полезная формальная модель для спецификации программных систем, [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 = В * Z = Выход *
а функции кодирования и декодирования определяются как:
α( ins ) = (<>, mem 0 , ins ) β( выходы , mem n , <>) = выходы
где ins: In *, outs: Out * и mem i : Mem . Другими словами, машина инициализируется всем входным потоком; и декодированный результат — это весь выходной поток при условии, что входной поток в конечном итоге будет использован (в противном случае результат не определен).
Каждой функции обработки в SXM присваивается сокращенный тип φ SXM : Mem × In → Out × Mem . Это можно отобразить на общее X-машинное отношение типа φ: X → X, если мы рассматриваем это как вычисление:
φ( outs , mem i , in :: ins ) = ( outs :: out , mem i+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, с приложениями в самых разных областях: от социальных насекомых до экономики.
Внешние ссылки [ править ]
- Проект MOTIVE , использующий методы SXM для создания наборов тестов для объектно-ориентированного программного обеспечения.
- Проект EURACE — применение методов CSXM к агентной вычислительной экономике.
- x-machines.net — сайт, описывающий предысторию исследований X-машин.
- Майка (профессора WML) Холкомба Веб-страница в Шеффилдском университете .
Ссылки [ править ]
- ^ Перейти обратно: а б Гилберт Лэйкок (1993) Теория и практика тестирования программного обеспечения на основе спецификаций . Докторская диссертация, Университет Шеффилда, факультет компьютерных наук. Аннотация. Архивировано 5 ноября 2007 г. в Wayback Machine.
- ^ Сэмюэл Эйленберг (1974) Автоматы, языки и машины, Vol. А. Лондон: Академическая пресса.
- ^ М. Холкомб (1988) «X-машины как основа спецификации динамических систем». Журнал программной инженерии 3 (2) , стр. 69-76.
- ^ Перейти обратно: а б Майк Холкомб и Флорентин Ипате (1998) Правильные системы – построение решения бизнес-процессов . Серия «Прикладные вычисления». Берлин: Springer-Verlag.
- ^ Перейти обратно: а б Ф. Ипате и У.М.Л. Холкомб (1997) «Метод интеграционного тестирования, который, как доказано, обнаруживает все ошибки». Межд. Дж. Комп. Математика. , 63 , стр. 159-178.
- ^ Ф. Ипате и М. Холкомб (1998) «Метод уточнения и тестирования обобщенных характеристик машины». Межд. Дж. Комп. Математика. 68 , стр. 197-219.