Эксперименты с дедуктивным тестированием реактивных систем
Применение дедуктивных методов в тестировании возможно при определении соответствия программного обеспечения исходным требованиям. Предполагается, что программный код разрабатывается по требованиям, которые могут быть заданы в некотором формальном языке. Техника дедуктивного тестирования с использов...
Gespeichert in:
| Veröffentlicht in: | Математичні машини і системи |
|---|---|
| Datum: | 2013 |
| 1. Verfasser: | |
| Format: | Artikel |
| Sprache: | Russisch |
| Veröffentlicht: |
Інститут проблем математичних машин і систем НАН України
2013
|
| Schlagworte: | |
| Online Zugang: | https://nasplib.isofts.kiev.ua/handle/123456789/84268 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Zitieren: | Эксперименты с дедуктивным тестированием реактивных систем / А.А. Летичевский (мл.) // Математичні машини і системи. — 2013. — № 4. — С. 20-28. — Бібліогр.: 7 назв. — рос. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1859853013268561920 |
|---|---|
| author | Летичевский, А.А. (мл.) |
| author_facet | Летичевский, А.А. (мл.) |
| citation_txt | Эксперименты с дедуктивным тестированием реактивных систем / А.А. Летичевский (мл.) // Математичні машини і системи. — 2013. — № 4. — С. 20-28. — Бібліогр.: 7 назв. — рос. |
| collection | DSpace DC |
| container_title | Математичні машини і системи |
| description | Применение дедуктивных методов в тестировании возможно при определении соответствия программного обеспечения исходным требованиям. Предполагается, что программный код разрабатывается по требованиям, которые могут быть заданы в некотором формальном языке. Техника дедуктивного тестирования с использованием символьного выполнения программы позволяет получить наиболее полное покрытие наблюдаемых данных. В данной статье рассматривается пример дедуктивного тестирования реактивной системы.
Застосування дедуктивних методів у тестуванні можливе при визначенні відповідності програмного забезпечення вихідним вимогам. Передбачається, що програмний код розробляється за вимогами, які можуть бути задані в деякій формальній мові. Техніка дедуктивного тестування з використанням символьного виконання програми дозволяє отримати найбільш повне покриття спостережуваних даних. У даній статті розглядається приклад дедуктивного тестування реактивної системи.
The application of deductive methods in testing technology is possible at definition of equivalence of software product to initial requirements. It is anticipated that programme code is developed due to the requirements that could be presented as formal specifications. Deductive testing technique by using symbol programme execution allows obtaining the most complete coverage of all visible data. The example of deductive testing of reactive system is considered in this paper.
|
| first_indexed | 2025-12-07T15:41:52Z |
| format | Article |
| fulltext |
20 © Летичевский А.А. (мл.)., 2013
ISSN 1028-9763. Математичні машини і системи, 2013, № 4
УДК 519.685/519.686
А.A. ЛЕТИЧЕВСКИЙ* (мл.)
ЭКСПЕРИМЕНТЫ С ДЕДУКТИВНЫМ ТЕСТИРОВАНИЕМ РЕАКТИВНЫХ
СИСТЕМ
*
Институт кибернетики им. В.М. Глушкова НАН Украины, Киев, Украина
Анотація. Застосування дедуктивних методів у тестуванні можливе при визначенні
відповідності програмного забезпечення вихідним вимогам. Передбачається, що програмний код
розробляється за вимогами, які можуть бути задані в деякій формальній мові. Техніка дедуктив-
ного тестування з використанням символьного виконання програми дозволяє отримати найбільш
повне покриття спостережуваних даних. У даній статті розглядається приклад дедуктивного
тестування реактивної системи.
Ключові слова: автоматизація тестування, формальна верифікація, інженерія вимог, формальні
методи, автоматизація доказів.
Аннотация. Применение дедуктивных методов в тестировании возможно при определении соот-
ветствия программного обеспечения исходным требованиям. Предполагается, что программный
код разрабатывается по требованиям, которые могут быть заданы в некотором формальном
языке. Техника дедуктивного тестирования с использованием символьного выполнения программы
позволяет получить наиболее полное покрытие наблюдаемых данных. В данной статье рассмат-
ривается пример дедуктивного тестирования реактивной системы.
Ключевые слова: автоматизация тестирования, формальная верификация, инженерия требова-
ний, формальные методы, автоматизация доказательств.
Abstract. The application of deductive methods in testing technology is possible at definition of equiva-
lence of software product to initial requirements. It is anticipated that programme code is developed due
to the requirements that could be presented as formal specifications. Deductive testing technique by using
symbol programme execution allows obtaining the most complete coverage of all visible data. The exam-
ple of deductive testing of reactive system is considered in this paper.
Keywords: automation of testing, formal verification, requirements engineering, formal methods, proving
automation.
1. Введение
Современные технологии тестирования программного и аппаратного обеспечения в основ-
ном базируются на автоматизации тестирования методом «черного ящика». Сам «черный
ящик» представляет собой модель или готовое изделие программно-аппаратного комплек-
са, а технология тестирования заключается в изучении его поведения или реакций, полу-
ченных как ответы на внешние воздействия. Существует также проблема надежности
тестирования, в которой изучаются вопросы адекватности «черного ящика» требуемым
свойствам создаваемой программы.
Мы рассматриваем тестирование программного кода реактивных систем, то есть
систем, которые многократно получают от внешней среды входные воздействия, а в среду
возвращают реакции. Взаимодействие со средой происходит в виде обмена сообщениями
или данными. Если в требованиях к системе встречаются временные ограничения, то такая
система относится к классу систем реального времени.
Как математический объект реактивная система представляет собой транзиционную
систему, действия которой подразделяются на входные воздействия и реакции. В одном
действии могут быть также совмещены входные воздействия и реакции, даже конечные
последовательности таких действий.
Стандартная технология тестирования представляет собой, в первую очередь, опи-
сание функциональных спецификаций, которые содержат описание реакций системы на
ISSN 1028-9763. Математичні машини і системи, 2013, № 4 21
входящие воздействия, а затем создание тестового набора, который соответствует описан-
ным реакциям. Такой тестовый набор может быть создан автоматически, если
функциональные спецификации или требования к системе представлены в виде
формальных спецификаций. Существует ряд инструментов, которые позволяют
автоматически сгенерировать тестовый набор, удовлетворяющий некоторому покрытию
[1]. Под покрытием понимают некоторый критерий для оценки качества тестирования, та-
кой, как покрытие требований, покрытие данных, а также покрытие строк кода.
Тестирование методом «черного ящика» происходит с помощью контроля
конкретных значений атрибутов системы, которые наблюдаются в качестве реакции
системы на некоторый набор конкретных воздействий. Полученные значения автоматиче-
ски сравниваются с прогнозируемыми, и делается вывод о прохождении теста.
Таким образом, для обнаружения всех ошибок в программном коде системы
необходимо проверить все комбинации всех конкретных значений входных данных, что
для большинства систем сделать невозможно. Поэтому применяют выборочные данные,
соответствующие некоторому разумному выбору, например, использование граничных
значений, эквивалентных разбиений.
Такие методы также не дают гарантии обнаружения всех ошибок и адекватности
свойств программного кода системы исходным требованиям, так как даже при разумном
выборе может быть пропущено некоторое критическое состояние. В данной работе
предлагается использовать дедуктивный метод тестирования, где в тестах с целью
достижения полного покрытия данных рассматриваются не конкретные значения, а их
множества. Для этого используется символьное моделирование формальных специфика-
ций, в частности, программного кода реактивной системы.
2. Тестирование программного кода реактивных систем с применением формальных
методов
Методы автоматизации тестирования разрабатываются в соответствии с моделью процесса
разработки программного обеспечения. В качестве исходных требований рассматривается
некоторое описание будущей системы на уровне абстракции, соответствующей
пониманию заказчика.
Изначально выполняется процедура формализации исходных требований, а также
их формальная верификация с помощью специальных инструментов. Далее процесс
разработки происходит согласно следующей схеме (рис. 1).
Рис. 1. Процесс разработки
Формальные требования в языке спецификаций, подходящем для верификационных
инструментов, представляют модель будущей системы на некотором уровне абстракции.
Формализация
Верификация и
моделирование
Генерация
тестового набора
Создание
программного кода
Исходные
требования
Формальные
требования
Верификацион-
ный вердикт
Формальные
требования
Тестовый
набор
Автоматическое
тестирование
Программный
код
22 ISSN 1028-9763. Математичні машини і системи, 2013, № 4
Здесь нужно зафиксировать уровень абстракции информации, в частности, описание вход-
ных и выходных данных, который соответствовал бы и требованиям, и программному коду
системы. В этом случае можно автоматически сгенерировать тестовый набор, который был
бы применим в тестировании готовой системы.
Программист создает код системы согласно верифицированным требованиям. Он
может использовать исходное описание требований, а также и формальные требования.
Существует технология, когда из формальных требований возможно сгенерировать про-
граммный код автоматически. Полученный код будет соответствовать уровню абстракции
требований. Если этот уровень недостаточен, то проводится уточнение программного кода
или же понижение уровня абстракции. В этом случае схема выглядит следующим образом
(рис. 2).
Рис. 2. Процесс разработки, включающий генерацию кода
Автоматическое тестирование представляет собой процедуру, в которой входом яв-
ляются исходный программный код системы и некоторый тестовый набор, представляю-
щий последовательности реакций системы в соответствии с входными воздействиями.
Для поддержки традиционного метода тестирования «черного ящика» тестовый на-
бор представляет последовательность входных воздействий на программный код и множе-
ство выходных реакций, которые сравниваются с выходными реакциями программного
кода. При этом программный код непосредственно выполняется или моделируется.
Использование же символьных методов позволит работать с множествами наборов
входных данных. Так, например, на вход программного кода поступает не конкретное
значение некоторой переменной, а формула, которая описывает множество значений этой
переменной. В этом случае программный код моделируется и на выходе получаем также
формулу, которая описывает множество значений выходных данных или некоторое сим-
вольное состояние программы. Сравнивая полученную формулу с ожидаемой, можно
сделать вывод об адекватности поведения программы изначальным требованиям. Далее
мы рассмотрим подробнее эту технологию, определив более точно каждый этап.
3. Формализация требований и генерация тестового набора
Требования к реактивным системам представляют собой описания реакций системы на
внешние воздействия. Эти реакции содержат изменение среды системы и выходные сооб-
щения. Для формализации таких требований мы будем использовать язык базовых прото-
колов, синтаксис и семантика которого описаны в [2], а примеры и методика формализа-
ции в [3].
Базовый протокол представляет собой описание реакции системы на внешнее воз-
действие, а также изменение среды системы, которая определяется ее атрибутами.
Формализация
Верификация и
моделирование
Генерация
тестового набора
Уточнение
программного кода
Исходные
требования
Формальные
требования
Верификацион-
ный вердикт
Тестовый
набор
Автоматическое
тестирование
Уточненный
программный код
Генерация
программного кода
на уровне
абстракции
требований
Программный
код
Формальные
требования
ISSN 1028-9763. Математичні машини і системи, 2013, № 4 23
Базовый протокол содержит предусловие, в котором представлено триггерное
событие, а также условия, при которых оно происходит. Предусловие является формулой в
некотором базовом логическом типизированном языке, содержащем арифметические и
логические операции.
Базовый протокол также содержит постусловие, в котором могут быть
императивные операторы присваивания и формула в базовом языке.
Таким образом, базовый протокол представляет реакцию системы как некоторый
переход транзиционной системы, который изменяет ее состояние.
Мы различаем конкретные и символьные модели требований к системе. Состояние
конкретной модели требований определяется конкретными наборами значений атрибутов
системы. Состояние символьной модели представляет собой формулу в базовом языке
модели.
Рассмотрим пример требований к системе, которая моделирует работу некоторого
станка по изготовлению неких изделий.
R1. Станок-автомат должен принимать на вход заготовки двух типов. Станок дол-
жен состоять из двух встроенных внутренних механизмов, один из которых воспринимает
на вход заготовки типа А, а другой типа В.
R2. Заготовки типа А поставляются на вход в кассетах по 20 единиц, а типа В по 16
единиц. Новая кассета поставляется на вход в начале дня, если предыдущие заготовки ис-
черпаны.
R3. Максимальная производительность станка 10 изделий в день.
R4. Выходом станка являются изделия, собранные из деталей типа А и деталей типа
В, которые изготавливаются встроенными механизмами соответственно из заготовок типа
А и типа В. Для каждого изделия используется по одной детали типа А и типа В.
R5. Возможны общие потери в производстве станка в количестве 2 изделий как
брак.
R6. Если количество заготовок меньше, чем производительность станка или меха-
низма, то изготавливается то минимальное количество изделий, которое можно получить
из имеющихся заготовок, то есть равное количеству заготовок того типа, которых меньше.
R7. Если количество заготовок больше или равно производительности станка, то из-
готавливается количество изделий, равное производительности станка. Остальные заго-
товки остаются в кассете для следующего раза.
Необходимо построить программу, моделирующую данный, производящий изде-
лия, станок, которая соответствует вышеуказанным требованиям.
Мы рассматриваем эту систему как реактивную, которая воспринимает в качестве
входных воздействий количество заготовок типа А и типа В, поступающих в начале дня, а
выходной реакцией является количество изготовленных за день изделий.
Определим переменные в этой программе:
A – количество заготовок типа А;
В – количество заготовок типа В;
D – планируемое количество произведенных изделий;
D_OUT – количество произведенных изделий c учетом возможного брака.
Множество базовых протоколов, соответствующее требованиям, состоит из пяти
протоколов. Первые два представляют ввод заготовок в станок. Остальные три моделиру-
ют процесс изготовления изделий. Таким образом, получаем следующую модель требова-
ний.
P1: А = 0 <Ввод кассет с заготовками типа А> А := 20
P2: В = 0 <Ввод кассет с заготовками типа В> В := 16
P3: (A ≤ B) ∧ (A ≤ 10) <Произвести и выдать изделия в количестве A> D := A; A: = 0; B :=
B - A; (D_OUT ≥ D - 2) ∧ (D_OUT ≤ D)
24 ISSN 1028-9763. Математичні машини і системи, 2013, № 4
Рис. 3. Порядок на множестве базовых
протоколов
P4: (A > B) ∧ (B ≤ 10)<Произвести и выдать изделия в количестве B> D :=B; B := 0; A := A
- B; (D_OUT ≥ D - 2) ∧ (D_OUT ≤ D)
P5: (A ≤ B) ∧ (A ≥ 10) ∨ (A > B) ∧ (B ≥ 10) <Произвести и выдать изделия в количестве 10>
A:= A - 10; B := B – 10; D:=10; (D_OUT ≥ 8) ∧ (D_OUT ≤ 10)
Мы также определяем порядок на множестве базовых протоколов, который задает
последовательность их применения согласно вышеуказанным требованиям. Данный поря-
док мы можем изобразить в виде диаграммы (рис. 3).
Согласно диаграмме процесс ра-
боты станка начинается с ввода загото-
вок типа А (протокол Р1) и типа В (про-
токол Р2). Если количество заготовок
больше нуля, то их ввод не
производится, что воплощено в
стрелочках, обходящих протоколы Р1 и
Р2. После этого производится изготов-
ление изделий согласно количеству за-
готовок (протоколы Р3 – Р5).
Зафиксировав некоторое началь-
ное состояние модели требований ( ) ( )0 0A B= ∧ = , мы можем моделировать описанные
требования посредством применения базовых протоколов. При этом мы получаем трассы,
содержащие символьное состояние среды после каждого применения базового протокола.
Эти трассы могут быть основой теста для поверки программы, которая должна соответст-
вовать вышеизложенным требованиям.
Ниже представлена одна из возможных последовательностей базовых протоколов и
соответствующих символьных состояний среды.
Таблица 1. Состояния среды в модели
ISSN 1028-9763. Математичні машини і системи, 2013, № 4 25
Рис. 4. С-программа
Каждое новое состояние среды получается с помощью предикатного трансформера
функцией pt , имеющей в качестве аргументов текущее состояние среды –
oldE , предусло-
вие Precond и постусловие Postcond базового протокола. Таким образом, новое состояние
newE среды получается следующим образом:
( ),new oldE pt E Precond Postcond= ∧ .
В дальнейшем для моделирования также используется функция обратного преди-
катного трансформера, позволяющая получать предыдущие состояния среды от текущего.
( )1 ,old newE pt E Postcond Precond−= ∧ .
Описание свойств функции pt содержится в работе [4].
4. Символьное моделирование программного кода
Система может быть спроектирована любыми способами программистом с использовани-
ем исходных требований. Программист может либо написать код, соответствующий этим
требованиям, либо использовать генерацию программного кода и уточнять его в соответ-
ствии с требуемым уровнем абстракции.
В данных требованиях мы абстрагированы от двух механизмов, обрабатывающих
заготовки типа А и типа В, которые являются составляющими системы и о структуре кото-
рых на уровне требований мы ничего не
знаем. Эти механизмы производят дета-
ли типа А и типа В. Каждый из них мо-
жет иметь определенную производи-
тельность и определенный процент бра-
ка. При проектировании систем допус-
кают переиспользование ранее спроек-
тированных таких механизмов со своими
собственными свойствами в новой сис-
теме.
Таким образом, задача програм-
миста состоит в том, чтобы создать код,
представляющий более низкий уровень
абстракции с учетом информации о со-
ставляющих механизмах, а с другой сто-
роны, этот код должен соответствовать
исходным требованиям. Для связи моде-
ли с ее реализацией естественно требо-
вать, чтобы программа использовала все
атрибуты модели требований, в частно-
сти, те, которые используются для взаи-
модействия системы со средой.
Пусть мы имеем некоторые уточ-
нения, относящиеся к работе механизмов А и В, являющихся составляющими системы, за-
ключающиеся в том, что механизм, производящий детали типа А, имеет производитель-
ность 15 деталей, а типа В – 9 деталей в сутки. При этом количество возможного брака со-
ставляет 3 детали и 1 деталь соответственно.
Учитывая эти уточнения, можно написать С-программу (рис. 4).
26 ISSN 1028-9763. Математичні машини і системи, 2013, № 4
Рис. 6. Процедура дедуктивного тестирования
В данной программе мы уточнили производство деталей типа А и типа В. Но будет
ли тогда данная программа соответствовать исходным требованиям?
Для дедуктивного тестирования будет использоваться символьное моделирование
С-программы. Мы рассматриваем некоторое подмножество С-программ, состоящих из
операторов присваивания, условных операторов, операторов цикла и процедур. В этом
случае символьное моделирование будет производиться так же, как и моделирование тре-
бований. Отличием будет то, что подпрограммы или библиотечные функции должны быть
аннотированы пред- и постусловиями. Таким образом, мы имеем следующие состояния
среды после выполнения каждого оператора (рис. 5).
Рис. 5. Состояния среды в С-программе
5. Дедуктивное тестирование
Входом дедуктивного тестирования (рис. 6) является множество трасс, полученных по-
средством символьного моделирования модели требований. Другим входом является про-
граммный код (в данном случае написанный на С).
Мы рассматриваем тестируемую
программу и внешнюю среду, посред-
ством которой управляется модели-
рующая программа.
Управляющая программа ими-
тирует эту внешнюю среду, подавая на
вход моделирующей программы дан-
ные вместе с формулой, ограничиваю-
щей их значения, в соответствии с сим-
вольной трассой, полученной в процес-
се моделирования требований.
В точках взаимодействия управ-
ляющей и тестируемой программы
производится контроль значений. В качестве такой точки контроля выбрана точка ответа
системы, а именно выдача количества деталей после их производства.
ISSN 1028-9763. Математичні машини і системи, 2013, № 4 27
В точке контроля мы получаем текущее символьное состояние среды в модели-
рующей программе и сравниваем его с контрольным значением в трассе. Рассматриваются
следующие случаи.
1. Символьное состояние среды на контрольной трассе эквивалентно символьному
состоянию среды, полученной в результате символьного моделирования С-программы.
Это означает, что ответ программы соответствует требуемой модели требований.
2. Символьное состояние среды, полученной в результате символьного моделиро-
вания С-программы, следует из символьного состояния среды на контрольной трассе. Это
означает, что на уровне кода запрограммировано поведение, которое выходит за рамки
требований.
3. Символьное состояние среды на контрольной трассе следует из символьного со-
стояния среды, полученной в результате символьного моделирования С-программы. Это
означает, что на уровне кода не запрограммировано поведение, которое определено в тре-
бованиях. Трассу, не соответствующую требованиям, можно найти обратным моделирова-
нием на уровне требований.
4. Ни одно из символьных состояний не следует из другого. В этом случае про-
грамма не удовлетворяет требованиям.
Рассмотрим дедуктивное тестирование на примере, предложенном выше. В данном
примере изначально мы имели эквивалентные состояния среды ( ) ( )0 0A B= ∧ = на уровне
требований (в символьной трассе) и в самом коде.
Рассмотрим первую точку контроля программы, которая соответствует точке s8,
представляющей функцию produce .
Контрольное состояние среды в трассе:
(A=10) ∧ (B = 6) ∧ (D_OUT≤ 10) ∧ (D_OUT ≥ 8).
Состояние среды в С-программе:
(A=5) ∧ (B=7) ∧ (3 ≤ A_OUT ≤ 7) ∧ (8 ≤ D_OUT ≤ 9) ∧ (i = 0) ∧ (B_OUT = 0).
Эти две формулы не являются эквивалентными, что говорит о том, что программа
работает не в соответствии со сценариями, представляющими требования.
Для анализа формул возможно рассматривать информационно независимые
литералы.
В отношении переменных А и В можно сказать, что значения в С-среде не соответ-
ствуют значениям на контрольной трассе, значит, поведение неверно. ~((B = 6) � (B = 7))
и ~((А = 10) � (А = 5)).
В отношении переменно D_OUT можно сказать, что С-программа не моделирует те
сценарии, которые представлены требованиями.
~((8 ≤ D_OUT ≤ 9) � (D_OUT <= 10) ∧ (D_OUT ≥ 8)).
Имея отрезок трассы от начальных значений до обнаруженного несоответствия,
требованиям можно найти место, где появляется это несоответствие, визуальным анализом
или методом обратного моделирования, который также описан в работе [4].
Нарушение для переменных А и В возникает на операторах, помеченных s3 и s4,
или же производительность блоков, изготавливающих детали А и В, влияет на общую
производительность станка. Для переменной D_OUT нарушение обнаруживается в момент
выполнения функций PERCENT_A и PERCENT_B, то есть процент брака встроенных ме-
ханизмов не совместим с требуемым процентом брака.
6. Выводы
Дедуктивное тестирование является методом, который может решить задачу покрытия
тестами всех конкретных значений переменных в программе. В данной методике не
28 ISSN 1028-9763. Математичні машини і системи, 2013, № 4
рассматривается вопрос покрытия всего кода или же всех требований тестами. Это рас-
сматривается в работах, посвященных символьному моделированию и генерации трасс с
заданным покрытием [5].
Вместе с тем в данном методе существуют проблемы, требующие уточнения в
реальных индустриальных примерах.
Первая проблема заключается в определении соответствия между переменными в
требованиях и переменными в программе. Одним из условий возможности дедуктивного
тестирования является соответствие уровня абстракций в интерфейсе между внешним
воздействием на программу и выходом программы для требований и для создаваемого
кода. Все переменные должны быть четко описаны в требованиях и использованы в коде.
На этапе кодирования при уточнении требований возможны уточнения некоторых
абстракций и, соответственно, появление переменных, которые не относятся к перемен-
ным, фигурирующим в требованиях. В этом случае мы выбираем переменные, которые
информационно зависимы от переменных, участвующих в требованиях, и проверяем фор-
мулу среды в С-программе на эквивалентность с формулой состояния среды в требовани-
ях, относя новые информационные переменные под квантор всеобщности.
Другой проблемой является появление недетерминизма в символьном
моделировании С-программы вследствие уточнения кода. Таким образом, в коде
появляется информация, которая не отражена в требованиях. Соответственно среда С-
программы может быть не эквивалентной среде, фигурирующей в требованиях. В этом
случае следует проверять не на эквивалентность, а на импликацию формулы среды в
требованиях из формулы среды в С-программе. Тем не менее, покрытие данных может
быть определено с помощью техники обратного моделирования.
Рассмотренный пример содержит программу, построенную с помощью линейных
арифметических преобразований. Используя методы символьного моделирования, разра-
ботанные авторами [2], возможно рассматривать также рациональные числа, списки,
функциональные и перечислимые типы данных. В качестве будущих работ планируется
использовать ряд индустриальных примеров, а также технику инвариантов.
СПИСОК ЛИТЕРАТУРЫ
1. Кулямин В.В. Формальные подходы к тестированию математических функций / Кулямин В.В. //
Труды ИСП РАН. – Москва, 2006. – Т. 10. – С. 69 – 114
2. Спецификация систем с помощью базовых протоколов / А.А. Летичевский, Ю.В. Капитонова,
А.А. Летичевский (мл.) [и др.] // Кибернетика и системный анализ. – 2010. – № 4. – С. 3 – 21.
3. Летичевский А.А. (мл.) / Об одном классе базовых протоколов / А.А. Летичевский (мл.) // Про-
блемы программирования. – 2005. – № 4. – С. 82 – 97
4. Свойства предикатного трансформера системы VRS / А.А. Летичевский, А.Б. Годлевский,
А.А. Летичевский (мл.) [и др.] // Кибернетика и системный анализ. – 2005. – № 4. – С. 4 – 14.
5. The technology of Automation Verification and Testing in Industrial Projects / S. Baranov, V. Kotlya-
rov, A. Letichevsky [et al.] // Proc. of St. Petersburg IEEE Chapter, International Conference, (St. Peters-
burg, Russia, May 18–21, 2005). – St. Petersburg, Russia, 2005. – P. 81 – 86
6. Clarke L. A system to generate test data and symbolically execute programs / L. Clarke // IEEE Trans.
Software Eng. – 1976. – Vol. 2. – P. 215 – 222.
7. Wegbreit B. Symbolic execution and program testing / B. Wegbreit // Communications of ACM. –
1976. – Vol. 19. – P. 385 – 394.
Стаття надійшла до редакції 13.09.2013
|
| id | nasplib_isofts_kiev_ua-123456789-84268 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 1028-9763 |
| language | Russian |
| last_indexed | 2025-12-07T15:41:52Z |
| publishDate | 2013 |
| publisher | Інститут проблем математичних машин і систем НАН України |
| record_format | dspace |
| spelling | Летичевский, А.А. (мл.) 2015-07-05T07:12:48Z 2015-07-05T07:12:48Z 2013 Эксперименты с дедуктивным тестированием реактивных систем / А.А. Летичевский (мл.) // Математичні машини і системи. — 2013. — № 4. — С. 20-28. — Бібліогр.: 7 назв. — рос. 1028-9763 https://nasplib.isofts.kiev.ua/handle/123456789/84268 519.685/519.686 Применение дедуктивных методов в тестировании возможно при определении соответствия программного обеспечения исходным требованиям. Предполагается, что программный код разрабатывается по требованиям, которые могут быть заданы в некотором формальном языке. Техника дедуктивного тестирования с использованием символьного выполнения программы позволяет получить наиболее полное покрытие наблюдаемых данных. В данной статье рассматривается пример дедуктивного тестирования реактивной системы. Застосування дедуктивних методів у тестуванні можливе при визначенні відповідності програмного забезпечення вихідним вимогам. Передбачається, що програмний код розробляється за вимогами, які можуть бути задані в деякій формальній мові. Техніка дедуктивного тестування з використанням символьного виконання програми дозволяє отримати найбільш повне покриття спостережуваних даних. У даній статті розглядається приклад дедуктивного тестування реактивної системи. The application of deductive methods in testing technology is possible at definition of equivalence of software product to initial requirements. It is anticipated that programme code is developed due to the requirements that could be presented as formal specifications. Deductive testing technique by using symbol programme execution allows obtaining the most complete coverage of all visible data. The example of deductive testing of reactive system is considered in this paper. ru Інститут проблем математичних машин і систем НАН України Математичні машини і системи Обчислювальні системи Эксперименты с дедуктивным тестированием реактивных систем Експерименти з дедуктивним тестуванням реактивних систем Experiments with a deductive testing of reactive systems Article published earlier |
| spellingShingle | Эксперименты с дедуктивным тестированием реактивных систем Летичевский, А.А. (мл.) Обчислювальні системи |
| title | Эксперименты с дедуктивным тестированием реактивных систем |
| title_alt | Експерименти з дедуктивним тестуванням реактивних систем Experiments with a deductive testing of reactive systems |
| title_full | Эксперименты с дедуктивным тестированием реактивных систем |
| title_fullStr | Эксперименты с дедуктивным тестированием реактивных систем |
| title_full_unstemmed | Эксперименты с дедуктивным тестированием реактивных систем |
| title_short | Эксперименты с дедуктивным тестированием реактивных систем |
| title_sort | эксперименты с дедуктивным тестированием реактивных систем |
| topic | Обчислювальні системи |
| topic_facet | Обчислювальні системи |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/84268 |
| work_keys_str_mv | AT letičevskiiaaml éksperimentysdeduktivnymtestirovaniemreaktivnyhsistem AT letičevskiiaaml eksperimentizdeduktivnimtestuvannâmreaktivnihsistem AT letičevskiiaaml experimentswithadeductivetestingofreactivesystems |