Место верификации при проектировании вычислительных систем

Согласно закону Мэрфи: Если какая-нибудь неприятность может произойти, она случается. Человек может ошибиться, поэтому он обязательно ошибается. Ошибки случаются при проектировании аппаратуры, при написании программ, при изготовлении аппаратуры. Иногда ошибки обходятся очень дорого. Приведем некоторые примеры последствий, к которым приводят такие ошибки.

В 1994 году профессор математики из Вирджинии при вычислении обратных величин простых чисел обнаружил, что микропроцессор Pentium в некоторых случаях неправильно делит числа с плавающей точкой. Через месяц фирма Intel согласилась заменить микропроцессоры с неправильно спроектированным устройством деления, что обошлось ей в 300 миллионов долларов (итоговые потери корпорации составили 500 миллионов долларов). Этот случай нанес большой ущерб репутации фирмы.

В 1991 году во время Войны в заливе (США против Ирака) батарея американских зенитных ракет «Patriot» не смогла перехватить запущенную иракцами ракету «Scud» советского производства. Ракета попала в казарму американских солдат, при этом погибло 28 человек. Причиной этого была погрешность вычисления времени. При вычислении нужно было умножать время, задаваемое тактовым генератором компьютера (оно измерялось в десятых долях секунды) на 1/10, но это десятичное число невозможно точно представить в двоичном виде. Для хранения этой константы использовался 24-разрядный регистр. Разница между точным значением 1/10 и ее неточным представлением составляет около 0, 000000095 в десятичном виде. Компьютер был включен около 100 часов, за это время накопилась ошибка в измерении времени в 0, 34 секунды. Скорость ракеты «Scud» составляла примерно 1700 м/сек, то есть за это время она прошла более 500 метров. Этого хватило для того, чтобы зенитные ракеты не смогли ее перехватить.

Слово верификация произошло от латинского verus - истинный и facere - делать. Вообще, верификация означает подтверждение того, что описание проекта полностью соответствует спецификации (техническому заданию) проектируемой системы. Спецификация — документ, подробно перечисляющий условия, которым должна соответствовать изготовляемая или проектируемая система.

Верификация определяется как разновидность анализа, имеющая целью установление соответствия двух описаний одного и того же объекта. Различают верификацию структурную и функциональную. При структурной верификации устанавливается соответствие структур, отображаемых двумя описаниями, при функциональной (параметрической) - проверяется соответствие процессов функционирования и выходных параметров, отображаемых сравниваемыми описаниями. Структурная верификация связана с меньшими затратами вычислительных ресурсов, чем функциональная. Поэтому последняя часто выполняется не в полном объеме и после того, как проверено соответствие структурных свойств. Примером структурной верификации служит установление соответствия системы электрических межсоединений на печатной плате и в принципиальной электрической схеме, заданных своими топологическими моделями в виде графов. Верификация в этом случае сводится к установлению изоморфизма графов. Функциональная верификация в данном примере выполняется путем анализа переходных процессов с учетом перекрестных помех и задержек сигналов в длинных линиях, определяемых конструктивным исполнением электронного блока.

Изоморфизм графов

Вопрос о том, изоморфны ли два данных графа, в общем случае оказывается сложным.

Для изоморфизма двух n-вершинных графов теоретически безукоризненный способ проверки состоит в проверке всех n! взаимно однозначных соответствий между множествами вершин и установлении, совмещаются ли полностью ребра графа хотя бы при одном соответствии. Однако даже весьма грубая оценка показывает, что такое решение «в лоб» практически непригодно: уже при n=20 перебор всех n! вариантов потребовал бы десятки лет машинного времени.

Подобная ситуация, естественно, толкнула многих математиков на попытки найти такой инвариант (число или систему чисел), который бы, с одной стороны, легко вычислялся по заданному графу, а с другой – обладал свойством полноты, т.е. определял граф однозначно с точностью до изоморфизма.

Инвариантом графа G(X, U) называется параметр, имеющий одно и то же значение для всех графов, изоморфных графу G.

Вначале естественно поставить вопрос: какие характеристики графов инвариантны относительно изоморфизма?

Среди самых очевидных инвариантов отметим следующие:

1. Число вершин |X| = m.

2. Число ребер |U| = k.

3. Число компонент связности р(G).

4. Последовательность степеней вершин, т.е. список степеней всех вершин в невозрастающем порядке значений rx_i.

5. Плотность f(G) – число вершин клики графа G.

6. Число внутренней устойчивости a (G).

7. Хроматическое число c(G).

8. Число Хадвигера h(G).

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

Множество инвариантов, которое позволило бы этой процедуре установить изоморфность графов за полиномиальное время, называется кодом графа. К сожалению, на сегодняшний день такое множество не найдено.

По существу, эвристический алгоритм рассматриваемого типа сводится к сравнению неполных кодов двух графов. Конечно, рассмотрение большого числа инвариантов увеличивает вероятность правильного заключения об изоморфизме при совпадении всех значений параметров, но в общем случае ничего не гарантирует.

Пример. Для графов на рис. 9.1 определим значения инвариантов.

G1

G2

Рисунок 9.1. Графы G₁ и G₂

Инвариант	G1	G2	Совпадение
m			+
k			+
р(G)			+
Список rx	3, 2, 2, 2, 2, 1	3, 2, 2, 2, 2, 1	+
f(G)			+
a (G)			+
c(G)			-
h(G)			+

Хроматические числа рассматриваемых графов разные. Это позволяет сделать вывод, что графы G₁ и G₂ не изоморфны.

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

Первые четыре инварианта относятся к группе «легко вычислимых». Наиболее «богатый» из них – упорядоченный список степеней вершин. Не будучи идеальным средством распознавания изоморфизма, список может, тем не менее, во многих случаях оказать существенную помощь.

Во-первых, если списки не совпадают, то отсюда сразу следует не изоморфизм графов G₁ и G₂.

Во-вторых, если списки совпали, то для проверки графов G₁ и G₂ на изоморфизм требуется перебор не всех n! соответствий между вершинами, а лишь тех, при которых сопоставляются вершины с одинаковой степенью. Так, в рассмотренном примере надо перебрать лишь 4! = 24 соответствия вместо 6! = 720.

Пример. Проверить на изоморфизм графы G₁ и G₂ (рис. 9.2)

 

х1

х2

х7

х3

х4

х5

х6

G1

y1

y2

y7

y3

y4

y5

y6

G2

		х1	х2	х3	х4	х5	х6	х7	ρ (x)
	х1
	х2
	х3
R(G1)=	х4
	х5
	х6
	х7

 

 

		y1	y2	y3	y4	y5	y6	y7	ρ (y)
	y1
	y2
	y3
R(G2)=	y4
	y5
	y6
	y7

 

 

Рисунок 9.2. Графы G₁ и G₂ и их матрицы соединений

Для графа G₁ Σ ρ (x)=30. Список Ρ (x) = {6, 5, 4, 4, 4, 4, 3}.

Для графа G₂ Σ ρ (y)=30. Список Ρ (y) = {6, 5, 4, 4, 4, 4, 3}.

Разобьем вершины обоих графов на классы по их степеням.

	ρ (x)= ρ (y)=6	ρ (x)= ρ (y)=5	ρ (x)= ρ (y)=4	ρ (x)= ρ (y)=3
X	x3	x4	x2, x5, x6, x7	x1
Y	y2	y4	y1, y3, y5, y6	y7

 

 

Из таблицы сразу видно соответствие вершин графов:

X	Y
x3	y2
x4	y4
x1	y7

Для определения соответствия вершин с ρ (x)=ρ (y)=4 попробуем связать вершины из классов с ρ (x)=ρ (y)=5 и ρ (x)=ρ (y)=3 с неустановленными вершинами.

X	Y
x3	x2 x5 x6 x7	y1 y3 y5 y6	y2
x4	y4
x1	y7

Анализ связей вершин показывает соответствие вершин x₂ и y₅ (соединены с установленными вершинами х₃~y₂ и х₁~y₇. С учетом этого

X	Y
x3	x5 x6 x7	y1 y3 y6	y2
x4	y4
x1	y7
x2	y5

 

 

Анализ связей вершин показывает соответствие вершин x₆ и y₁ (единственные имеют одну связь с классом вершин ρ (x)=ρ (y)=5. С учетом этого

X	Y
x3	x5 x7	y3 y6	y2
x4	y4
x1	y7
x2	y5
x6	y1

 

Анализ связей вершин показывает, что существует две пары соответствий оставшихся вершин: вершины x₅ и y₃ и вершины x₇ и y₆, или x₆ и y₃ и вершины x₇ и y_3. Это соответствует действительности, т.к. вершины x₅ и x₇ в графе G₁ и вершины y₃ и y₆ в графе G₂ смежны с одними и теми же вершинами.

Из сказанного можно сделать вывод, что графы G₁ и G₂ изоморфны.

Нахождение эйлерова цикла

Алгоритм Флери

Элегантный алгоритм нахождения эйлерова цикла был предложен М. Флери (М. Fleury) в 1883 году.

Алгоритм заключается в следующем:

1. Положить текущий граф равным G(X, U), а текущую вершину равной произвольной вершине x_i ∈ X.

2. Выбрать произвольное ребро u_ij текущего графа, инцидентное текущей вершине x_i с учетом следующего ограничения: если степень текущей вершины в текущем графе больше 1, нельзя выбирать ребро, удаление которого из текущего графа увеличит число компонент связности в нем (т.е. ребро, являющееся мостом).

3. Назначить текущей x_j вершину, инцидентную ребру u_ij.

4. Удалить u_ij из текущего графа и внести в список.

5. Если в текущем графе еще остались ребра, то положить i=j и вернуться на шаг 2.

Пример. Рассмотрим граф, изображенный на рис. 10.1 (а) (он эйлеров в силу теоремы Эйлера о циклах) и найдем в нем эйлеров цикл.

в

х1

х2

х3

х4

х5

х6

х1

х2

х3

а

х4

х5

х6

б

х1

х2

х3

х4

х5

х6

Рисунок 10.1. Исходный граф (а), текущий граф (б) и эйлеров цикл (в)

Пусть на шаге 1 выбрана вершина x₁. При выборе на шаге 2 ограничение никак не сказывается; пусть выбрано ребро (x₁, x₅). На двух следующих итерациях ограничений на выбор по-прежнему не возникает; пусть выбраны ребра (x₅, x₂) и (x₂, x₆). Тогда текущим графом становится граф, изображенный на рис. 10.1 (б) (текущая вершина − x₆). На следующей итерации нельзя выбрать ребро (x₆, x₃) из-за ограничения; пусть выбрано ребро (x₆, x₅). Дальнейший выбор ребер определен однозначно (текущая вершина всегда будет иметь степень 1), так что в итоге будет построен следующий эйлеров цикл (рис. 10.1 (в)): x₁ → x₅ → x₂ → x₆ → x₅ → x₄ → x₆ → x₃ → x₂ → x₁.

Сложность алгоритма О(k), где k = |U| − число ребер.

⇐ Предыдущая10111213141516171819Следующая ⇒

Поделиться:

Популярное:

1. A. Оказание помощи при различных травмах и повреждениях.
2. A. особая форма восприятия и познания другого человека, основанная на формировании по отношению к нему устойчивого позитивного чувства
3. B. Принципы единогласия и компенсации
4. B. умение «встать на место другого человека»
5. Cочетания кнопок при наборе текста
6. D-технология построения чертежа. Типовые объемные тела: призма, цилиндр, конус, сфера, тор, клин. Построение тел выдавливанием и вращением. Разрезы, сечения.
7. D. умение «встать на место другого человека»
8. EP 3302 Экономика предприятия
9. Exercise 5: Образуйте сравнительные степени прилагательных.
10. H. Приглаживание волос, одергивание одежды и другие подобные жесты
11. I) Получение передаточных функций разомкнутой и замкнутой системы, по возмущению относительно выходной величины, по задающему воздействию относительно рассогласования .
12. I. «Движение при закрытой автоблокировке (по путевой записке).