Методы верификации аппаратно-программных компонентов вычислительных систем тема диссертации и автореферата по ВАК РФ 05.13.12, кандидат технических наук Зыков, Анатолий Геннадьевич

• Зыков, Анатолий Геннадьевич
• кандидат технических наук
• 2008

Оглавление диссертации кандидат технических наук Зыков, Анатолий Геннадьевич

Введение.

Глава 1. Обзор методов верификации аппаратных и программных компонентов вычислительных систем.

1.1 Основные термины и определения.

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

1.3 Методы верификации.

1.3.1. Методы верификации на основе темпоральных логик.

1.3.2. Методы на базе автоматных и графовых моделей.

1.3.3. Алгебраические методы.

1.3.4 Методы'верификации программ.

1.4 Современные тенденции в методологии верификации аппаратных и программных компонентов ВС.

1.5 Вычислительные процессы в логических схемах и программах.

1.5.1. Проектирование вычислительных процессов.

1.5.2. Вычислительный процесс.

1.5.3 Верификация вычислительных процессов.

1.6 Постановка задач исследования.

Выводы по главе 1.

Глава 2. Разработка моделей вычислительного процесса.

2.1 Разработка универсальной модели функционально-логической схемы.

2.2 Алгебро-топологическая модель последовательностной схемы в виде комплексного кубического покрытия.

2.3 Итерационно-рекурсивная модель вычислительных процессов в виде комплексных кубических покрытий.

2.3.1 Структурирование программ и вычислительных процессов.

2.3.2 Концептуальная итерационно-рекурсивная модель (ШМО).

2.3.3 Итерационно-рекурсивные покрытия.

2.4 Модель и примитивы вершин циклических вычислительных процессов.

2.4.1 Итерационно-рекурсивная модель вычислительного процесса. с двумя контурами обратной связи.

2.4.2 Примитивы вырожденных покрытий вершин ГАМ.

2.4.3 Построение комплексного покрытия для циклических. вычислительных процессов.

2.4.4 Машинно-ориентированное описание вершин и дуг ГАМ.

Выводы по главе 2.

Глава 3. Разработка методов верификации вычислительных процессов.

3.1 Верификации моделей разного уровня методом построения графа переходов схемы

3.2. Верификация моделей одного уровня абстракции.

3.2.1 Методы верификации цифровых схем.

3.3 Разработка методов верификации программ.

3.3.1 Метод функциональной верификации программ на основе. алгебро-топологического подхода.

3.3.2. Кубические покрытия логических условий вычислительных. процессов и программ.

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

3.4.1 Пример верификации ациклического процесса.

Выводы по главе 3.

Глава 4. Разработка структуры и алгоритмов учебно-исследовательской САПР верификации вычислительных процессов.

4.1 Структура УИ САПР ВВП ФЛС. Базы знаний и данных при построении моделей

4.2 База Знаний и База данных УИ САПР ВВП ФЛС.

4.2.1 Структура, формирование и редактирование Базы Знаний.

4.2.2 Разработка алгоритмов взаимодействия БД и БЗ. Протокол. обмена данными.

4.3 Машинно-ориентированные алгоритмы реализации операций пересечения и поглощения кубов комплексного покрытия.

4.4 Входной язык описания схемы.

4.5 Разработка алгоритма построения моделей цифровых устройств в виде комплексного кубического покрытия.

4.6 Разработка алгоритмов верификации.

4.7 Обобщенная структура УИ САПР ВВП.

Выводы по главе 4.

Введение диссертации (часть автореферата) на тему «Методы верификации аппаратно-программных компонентов вычислительных систем»

Актуальность проблематики диссертационной работы

Проблема анализа качества аппаратного и программного обеспечения становится сегодня все более острой, особенно по мере расширения использования нанотехнологий в приборостроении и информационных технологий при разработке программного обеспечения. Экспоненциальный рост сложности аппаратного и программного обеспечения вычислительных процессов порождает повышенные требования к бездефектному проектированию. Известны примеры, как дорого обходятся ошибки, допущенные на различных этапах проектирования, поэтому все современные САПР обязательно снабжаются методологическими, программными и инструментальными средствами анализа разрабатываемого изделия на всех этапах автоматизированного проектирования. Не менее актуальными являются проблемы, связанные с обеспечением проектирования надежных программ. Большой вклад в становление и развитие методов решения данной проблемы внесли отечественные ученые Пархоменко П.П., Липаев В.В., Согомонян Е.С., Майоров С.А., Не-молочнов О.Ф., Рябов Г.Г., Селютин В.А., Курейчик В.М. и многие другие.

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

Цель работы является исследование и разработка методов верификации аппаратно-программных компонентов вычислительных систем; разработка машинно-ориентированных алгоритмов построения комплексных кубических покрытий цифровых схем и графо-аналитических моделей программ; разработка структуры и основных подсистем учебно-исследовательской САПР (УИ САПР) верификации вычислительных процессов.

Для достижения поставленной цели в работе решались следующие основные задачи:

• сравнительный анализ существующих методов верификации проектов;

• разработка универсальной модели последовательностной схемы;

• разработка модели вычислительного процесса;

• разработка методов и алгоритмов построения комплексных кубических покрытий цифровых схем и программ;

• разработка методов верификации аппаратно-программных компонентов вычислительных систем;

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

Научная новизна. В работе получены следующие существенные результаты:

• разработана универсальная модель функционально-логической схемы, позволяющая описывать состояния и переходы схемы в виде комплексного кубического покрытия;

• разработана концептуальная итерационно-рекурсивная двухконтурная модель вычислительного процесса;

• разработан метод построения комплексного кубического покрытия цифровой схемы;

• разработан метод построения комплексного кубического покрытия графо-аналитической модели (ГАМ) программы;

• разработаны методы верификации моделей аппаратно-программных компонентов вычислительных систем различного уровня.

• на основе разработанных методов предложены алгоритмы работы учебно-исследовательской САПР верификации вычислительных процессов и отдельных подсистем.

Практическая ценность. Разработаны методы, алгоритмы и программы, осуществляющие построение комплексных кубических покрытий цифровых схем и ГАМ программ на уровне исполняемого кода. Разработаны алгоритмы и программы локальной и глобальной оптимизации построения комплексных кубических покрытий цифровых схем. Разработаны алгоритмы и программы, осуществляющие верификацию аппаратных и программных компонентов вычислительных систем. Разработана структура и алгоритмы УИ САПР верификации и тестирования аппаратных и программных компонентов вычислительных систем.

Внедрение результатов работы. Основные результаты работы использованы в СПб ГУ ИТМО на кафедре информатики и прикладной математики в учебных дисциплинах «Верификация моделей», «Системное программное обеспечение», «Технология программирования» для студентов специальности 220100 «Вычислительные машины, системы, комплексы и сети» и по курсу «Автоматизация логического проектирования ЭВС» для студентов специальности 210202 «Проектирование и технология вычислительных средств».

Результаты работы были использованы при выполнении проекта «Рефрен - Н» в ФГУП СПб ОКБ «Электроавтоматика», а также в ФГУП «Научно-исследовательский институт физической оптики, оптики лазеров и информационных оптических систем» Всероссийского научного центра «Государственный оптический институт им. С.И. Вавилова».

Апробация работы: Основные результаты диссертационной работы докладывались и получили одобрение на научных и учебно-методических конференциях профессорско-преподавательского состава ГИТМО(ТУ) (С.Петербург 1996 - 2000, 2002, 2003 г.г.) и СПб ГУ ИТМО (С.-Петербург 2004 -2008 г.г.); на Межвуз. науч. -техн. семинаре с междунар. участием «Автоматизация проектирования, технология элементов и узлов компьютерных систем». - СПб: 1998; на Всероссийской НТК «Интеллектуальные САПР-94», Таганрог, 1994; на Юбилейной НТК 1111С, посвященная 100-летию университета 29-31 марта 2000 года.- СПб.: СПб ГИТМО (ТУ), 2000; на 6-й МНПК «Безопасность и защита информации сетевых технологий. COMMON CRITERIA" СПб, 13-15 июня 2001.- СПб.: СПб ГИТМО (ТУ), 2001; на 9-й научно-технической конференции «Теория и технология программирования и защиты информации, применение вычислительной техники» -СПб: СПбГУ ИТМО 2002г.; на Международных научно-технических конференциях «Интеллектуальные системы» (IEEE AIS'04) и «Интеллектуальные САПР» (CAD-2002, 2004 - 2008) Дивноморское; на 11-ой международной научно-практической конференции «Теория и технология программирования и защиты информации»/ СПб: СПбГУ ИТМО, 18 мая 2007; на Первом СПб конгрессе «Профессиональное образование, наука, инновации в XXI веке» / СПб: СПбГУ ИТМО, 26-27 октября 2007.

Публикации. По материалам диссертации опубликовано 36 работ, в том числе - 12 из списка, рекомендованного ВАК.

Структура и объем работы Диссертация состоит из введения, четырех глав, заключения, библиографического списка из 92 наименований, содержит 105 страниц текста, 44 рисунка и 5 таблиц.

Заключение диссертации по теме «Системы автоматизации проектирования (по отраслям)», Зыков, Анатолий Геннадьевич

Выводы по главе 4

1. Разработаны машинно-ориентированные методы реализации основных операций построения комплексных кубических покрытий ФЛС.

2. Разработаны методы, алгоритмы и программы верификации аппаратно-программных компонентов вычислительных систем.

3. На основе предложенных методов разработана структура, основные алгоритмы и программы учебно-исследовательской САПР верификации вычислительных процессов.

4. Намечены пути дальнейших исследований в области верификации аппаратно-программных компонентов ВС.

Заключение

В диссертационной работе исследована проблема верификации аппаратно-программных компонентов вычислительных систем и доказана теоретическая и практическая ценность следующих полученных научных результатов.

1. Предложена универсальная модель последовательностной схемы. На основе предложенной модели разработана методика построения комплексного кубического покрытия схемы для различных задач анализа в САПР.

2. Разработана концептуальная итерационно-рекурсивная двухкон-турная модель вычислительного процесса.

3. Предложена модель вычислительного процесса в виде орграфа и кубических покрытий условий-предикатов для вычисляемых переменных.

4. Для машинно-ориентированного описания ГАМ предложены примитивы и вырожденные покрытия типовых вершин.

5. Предложены методы верификации через эквивалентность покрытий и перекрестное тестирование вычислительного процесса вне зависимости от его физической реализации.

6. Разработана методика структурирования вычислительного процесса путем разбиения множества команд машинного кода на замкнутые подмножества команд с одной точкой входа и одной точкой выхода.

7. Разработана структура экспериментальной учебно-исследовательской САПР верификации вычислительных процессов, алгоритмы и программы решения основных задач, в частности: построение комплексного покрытия схемы, построение графа и покрытий частично определённых булевых функций, моделирования логических неисправностей условий-предикатов, верификации аппаратно-программных компонентов вычислительных систем.

Список литературы диссертационного исследования кандидат технических наук Зыков, Анатолий Геннадьевич, 2008 год

1. Системы автоматизированного проектирования: Иллюстрированный словарь / Под ред. И.П. Норенкова. М.: Высшая школа, 1986.

2. CMMI for Systems Engineering/Software Engineering, Version 1.02 (CMMI-SE/SW, VI.02) CMU/SEI-2000-TR-018 ESC-TR-2000-018 November 2000, P. 598

3. Липаев B.B. Обеспечение качества программных средств. Методы и стандарты / Издательство: Синтер; Серия: Информационные технологии, 380 стр., 2001 г.

4. C.B. Зеленов, Н.В. Пакулин. Верификация компиляторов систематический подход/ Труды Института системного программирования РАН.

5. Г. Майерс. Надежность программного обеспечения. М.: «Мир», 1980. 360 с.

6. Грушин А.И. Верификация в вычислительной технике. //Потенциал, №4,2007: hltp://potcntia1.org.ru/Info/ArtDl200704151927РНЗ C4J4

7. M. Blum, H. Wasserman / Reflections on the Pentium Division Bug. IEEE Trans. On Computers, vol. 45, no. 1996, 4, April

8. Синицын C.B., Налютин Н.Ю. Верификация программного обеспечения // БИНОМ. Лаборатория знаний, Интернет-университет информационных технологий ИНТУИТ.ру, 2008

9. А.Лохов. Функциональная верификация СБИС в свете решений Mentor Graphics//3JIEKTP0HHKA: Наука, Технология, Бизнес Выпуск № 1/2004 С.58-62.10. 2001 Dataquest Sub-Market Analysis On Combined Verification Technologies. www.dalaquesi.com.

10. Дейкстра Э. Дисциплина программирования: Пер. с англ.- М.: Мир, 1978. -275с.

11. Грис Д. Наука программирования: Пер. с англ.- М.: Мир, 1984.416с.

12. Манна 3. Правильность программ // Кибернетический сборник. Новая серия. М., 1970.- Вып.7.-С.85-93.

13. Непомнящий В.А. Практические методы верификации программ // Кибернетика. 1984.- №2,- С.21-28, 43.

14. Непомнящий В.А., Рякин О.М. Прикладные методы верификации программ. — М.: Радио и связь, 1988.- 256с.

15. Bakker J.W. Mathematical Theory of Program Correctness.- London: Prentice-ITall, 1980,- 505c.

16. Clarke E., Mishra B. Automatic Verification of Asyncronous Circuits // Logic of Programs. Proc. 1983 / E. Clarke and D.Kozen (eds.). Berlin: Springer, 1984.- P.101-115-(LNCS; 164).

17. Clarke E.M., Brawne M.C., Emerson E.A. Using Temporal Logic for Automatic Verification of Finish State Systems // Logics and Models of Concurrent Systems. Proc. 1984 / Ed. by K.P.Apt. Berlin: Springer, 1985.- P.3-26.-(NATO ASI Series F; Vol.13).

18. Brawne M.C., Clarke E.M., Dill D.L. Automatic Verification of Sequential Circuits Using Temporal Logic // IEEE Transactions on Computers. 1986.-Vol/C-35, No. 12.- P. 1035-1044.

19. Kroger F. Temporal Logic of Programs. Berlin: Springer, 1985.- 148p. (EATCS Monographs on Theoreticals Computer Science; Vol.8).

20. Manna Z., Pnueli A. Verification of Concurrent Programs: The Temporal Framework // The Correctness Problem in Computer Science / R.S.Boyer and J.S.Moore (eds.). London: Academic Press, 1981.- P.215-273.

21. Логика и компьютер. Моделирование рассуждений и проверка правильности'программ. -М.: Наука, 1990,- 240с.

22. Э.М. Кларк, О. Грамберг, Д. Пелед. "Верификация моделей программ". Москва, 2002, изд-во МЦНМО, 415 с.

23. Fujita M., Kono S., Tanaka H. Aid to Hierarchical and Structured Logic Desine Using Temporal Logic and Prolog // IEE Proceedings. — 1986.-Vol.l33-E, No.5.- P.283-294.

24. Аникин A.B. Верификация проектов цифровых устройств с использованием метода Дейкстры-Гриса // Изв. ЛЭТИ: Сб. науч. тр./ Ленингр. элек-тротехн. ин-т им. В.И. Ульянова (Ленина).- Л. 1989.- Вып.415.-С.30-35.

25. Автоматное управление асинхронными процессами в ЭВ1Ч4 и дискретных системах / Под ред. В.И. Варшавского. — М.: Наука, 1986.- 400с.

26. Ачасова С.М., Вандман О.Л. Корректность параллельных вычислительных процессов.- Новосибирск: Наука, 1990.- 253с.

27. Варшавский В.И., Кишиневский М.А., Кондратьев А.Ю. Модели для спецификации и анализа процессов в асинхронных схемах // Изв. АН СССР. Техническая кибернетика.-1988.-№2,- С.171-190.

28. Котов В.Е. Сети Петри. М.:Наука, 1984.-160с.

29. Питерсон Дж. Теория сетей Петри и моделирование систем: Пер. с англ. -М.: Мир, 1984.- 264с.

30. Kreisel G., Krivine J.L. Elements of Mathematical Logic (Model Theory).- Amsterdam: North-Holland, 1971.- 232p.

31. Jahanian F., Mok A.K.-L. A Graph-Theoretical Approach for Timing Analysis and its Implementation // IEEE Transactions on Computers.- 1987.- Vol. C-36, No,8.- P.961-975.

32. Berthet C., Cerny E. An Algebraic Model for Asynchronous Circuit Verification // IEEE Transactions on Computers.- 1988.- Vol. 37, No,7.- P.835-837.

33. Александр Петренко, Елена Бритвина, Сергей Грошев, Александр Монахов, Ольга Петренко Тестирование на основе моделей // Открытые системы, #09/2003

34. Е. Clarke, О. Grumberg, D, Long Model Checking, In Springer-Verlag Nato ASI Series F, Volume 152, 1996

35. Зелковиц M., Шоу А., Гэннон Дж. Принципы разработки программного обеспечения. М.: Мир, 1982. - 368 с.

36. Липаев B.B. Отладка сложных программ. Методы, средства, технология. М.: Энергоатомиздат, 1993. -384 с.

37. Липаев В.В. Управление разработкой программных средств: Методы, стандарты, технология. М.: Финансы и статистика, 1993.

38. Майерс Г. Искусство тестирования программ. М.: Мир, 1982. 212с.

39. Грис. Д. Конструирование компиляторов для цифровых вычислительных машин. М.: Мир, 1975. - 544с.

40. Липаев В.В. Проектирование программных средств. М.: Высшая школа, 1990.

41. Андерсон Р. Доказательство правильности программ. —М.: Мир. — 1982.- 168с.

42. Бейбер Л.Р. Программное обеспечение без ошибок. М. Радио и связь. 1996. 173 с.

43. И.Б.Бурдонов, А.В.Демаков, А.С.Косачев, А.В.Максимов, А.К.Петренко Формальные спецификации в технологиях обратной инженерии и верификации программ.// Труды Института системного программирования Российской Академии наук. N 1, 1999.

44. Э. Дейкстра. Заметки по структурному программированию. //У. Дал, Э. Дейкстра, К. Хоор. Структурное программирование. М.: Мир, 1975.

45. Непомнящий В.А., Рякин О.М. Прикладные методы верификации программ. М.: Радио и связь, 1988.

46. Основы верификационного анализа безопасности исполняемого кода программ. / Матвеев В.А., Молотков C.B., Зегжда Д.П.,Мешков A.B., Семьянов П.В., Шведов Д.В. Под редакцией проф. Зегжды П.Д. СПб.: СПбГТУ, 1994. 58с.

47. Alur R., Henzinger T., Pei-Hsin Ho. Automatic symbolic verification of embedded systems //IEEE Trans, on Software Eng. 1996. N3.

48. Липаев B.B. Надежность программных средств. M.: СИНТЕГ, 1998,-232 с.

49. Lowry M Analytic Verification and Validation for Space Missions. NASA Ames Research Center http://is.arc.nasa.gov/AR/projects/AtnVrf.html

50. Черноножкин C.K. Меры сложности программ // Системная информатика. Новосибирск: Наука. Сиб. отд-ние, 1997. Вып. 5. Архитектурные, формальные и программные модели

51. Гацко Г. Тестирование ПО как один из элементов системы качества // Открытые системы. 1998. N6.

52. Коул Дженнифер, Горэм Томас, МакДональд Марк, Спарджеон Роберт. Принципы тестирования ПО // Открытые системы (Изд-во "Открытые системы"). 1998. № 2.

53. Никифоров В.В., Домарацкий Я.А. Системное тестирование программных изделий. // Программные продукты и системы. 1998. N 4. С. 40-46.

54. А.К. Поляков "Языки VHDL и VERILOG в проектировании цифровой аппаратуры" М., Солон-Пресс, 2003

55. М. R. A. Huth, M.D. Ryan. Logic in Computer Science: Modelling f and Reasoning about Systems. Cambridge University Press, 2002, 387 p.

56. Липаев B.B. Сопровождение и управление сложных программных средств. -М.: СИНТЕГ, 2006. -372с.

57. Проектирование цифровых вычислительных машин / С.А. Майоров, Г.И. Новиков, О.Ф. Немолочнов и др. Под ред. С.А. Майорова. М.: Высш.шк., 1972. 344 с.

58. Зыков А.Г., Немолочнов О.Ф., Виноградов Ю.Н., Поляков В.И. Верификация как средство отладки моделей различного уровня. «Известия вузов. Приборостроение»/ Том 46, №2, 2003, С.51-55.

59. Итерационно-рекурсивная модель вычислительных процессов, порождаемых программами / Немолочнов О.Ф., Зыков А.Г., Поляков В.И., Осовецкий Л.Г., Сидоров A.B. Кулагин B.C.- «Известия вузов. Приборостроение»/ Том 48, №12, СПб, 2005, С.14-20.

60. Деметрович Я., Кнут Е., Радо П. . Автоматизированные методы спецификации. М.: Мир, 1989).

61. В.Е. Котов, Л.А. Черкасова Исчисление процессов, в кн. «Системная информатика». Вып. 2, Новосибирск, «Наука», 1993.

62. M.K. Molloy Performance Analesis Using Stochastic Petri Nets // IEEE Transactions on Computers.- Vol. C-31, 1982, September

63. Стешенко В.Б. Примеры проектирования цифровых устройств с использованием языков описания аппаратуры / «Схемотехника», 2001, № 7, С. 42; №8, С.32; № 10, С.42; № 11, С.46.

64. Климович Ф., Соловьев В.В. Логическое проектирование цифровых систем на основе программируемых логических интегральных схем. М.: Радио и связь, 2008. 376 с.

65. Лаздин A.B., Немолочнов О.Ф. Оценка сложности графа функциональной программы / Научно-технический вестник СПБ ГИТМО (ТУ). Выпуск 6. Информационные, вычислительные и управляющие системы / Гл. ред. В.Н. Васильев. СПб.: СПбГИТМО (ТУ), 2002.

66. Немолочнов О.Ф. Методы технической диагностики / Методическое пособие / ЛИТМО, Ленинград, 1977 г.

67. Немолочнов О.Ф. Контроль и диагностика сочетаний неисправностей в комбинированных системах / УС и М, №4, Киев, 1973 г.

68. Майоров С.А., Новиков Г.И. Принципы организации цифровых машин. Д., «Машиностроение», 1974. 432 с.

69. Баранов С.И., Синёв В.Н. Автоматы и программируемые матрицы. Мн., «Выс. школа», 1980. 136 с.

70. Чжен Г., Мэннинг Е., Метц Г. Диагностика отказов цифровых вычислительных систем. Пер. с англ. под ред. И. Б. Михайлова. М., «Мир», 1972. 232 с.

71. Липаев В.В. Функциональная безопасность программных средств. Сер. Управление качеством. М.: Синтег, 2004.

72. Зыков А.Г., Немолочнов О.Ф., Поляков В.И. Универсальная модель последовательностных схем в САПР / Научно-технический вестник СПБ

73. ГИТМО (ТУ). Выпуск 6. Информационные, вычислительные и управляющие системы / Гл. ред. В.Н. Васильев.- СПб.: СПб ГИТМО (ТУ), 2002. с. 107-108.

74. Ope О. Теория графов. М.: «Наука», 1968. — 352с.

75. Карибский В.В., Пархоменко П.П., Согомонян Е.С., Халчев В.Ф. / Основы технической диагностики. Кн.1.- М.: Энергия, 1976

76. Графы и алгоритмы. Структуры данных. Модели вычислений: Учебник / В.Б. Алексеев, В.А. Таланов. М.: Интернет-Университет Информационных технологий; БИНОМ. Лаборатория знаний, 2006. - 320с.

77. Немолочнов О.Ф., Усвятский А.Е., Звягин В.Ф., Голыничев В.Н. Промышленная система автоматизации проектирования тестов.// УС и М. 1981. №5

78. Блохин В.Н., Голованевский Г.Л., Зыков А.Г., Немолочнов О.Ф. Доступная система контроля цифровых узлов и верификация логических модулей. / Сб. «ЭВМ в проектировании и производстве» / Вып. 4, «Машиностроение», 1989.

79. Зыков А.Г., Немолочнов О.Ф. Автоматная модель устройства управления в САПР при верификации проекта. / Межвузовский сборник научных трудов «Автоматизированное проектирование в радиоэлектронике и приборостроении», С.-Пб, ГЭТУ, 1994. С. 21-23.

80. Модель и примитивы покрытий вершин циклических вычислительных процессов / Немолочнов О.Ф., Зыков А.Г., Осовецкий Л.Г., Поляков В.И. //Известия вузов. Приборостроение. 2007. Том 50, №8, С. 18-23.

81. Тестирование логических неисправностей вычислительных процессов в программах / Немолочнов О.Ф., Зыков А.Г., Осовецкий Л.Г., Поляков В.И., Петров К.В. / Журнал «Информационные технологии» / №12, М., 2007, С.2-5.

82. Functional Verification of a Multiple-Issue, Out of Order, Superscalar Alpha Processor. DAC, 1998.