Тестирование софта - статьи
ce076b8f

Литература


1.обратноStatistical Analysis of Floating Point Flaw in the Pentium Processor. Intel Corporation, November 1994.
2.обратноB. Beizer. The Pentium Bug - An Industry Watershed. Testing Techniques Newsletter (TTN), TTN Online Edition, September 1995.
3.обратноА. Wolfe. For Intel, It's a Case of FPU All Over Again. EE Times, May 1997.
4.обратноB. Meyer. Design by Contract. Technical Report TR-EI-12/CO, Interactive Software Engineering Inc., 1986.
5.обратноB. Meyer. Applying `Design by Contract'. IEEE Computer, vol. 25, No. 10, October 1992.
6.обратно
7.обратноIEEE Standard VHDL Language Reference Manual. IEEE Std 1076-1987.
8.обратноIEEE Standard Hardware Description Language Based on the Verilog Hardware Description Language. IEEE Std 1364-1995.
9.обратно
10.обратно
11.обратно
12.обратно
13.обратноI. Bourdonov, A. Kossatchev, V. Kuliamin, and A. Petrenko. UniTesK Test Suite Architecture. FME'2002. LNCS 2391, Springer-Verlag, 2002.
14.обратно
15.обратноA. Kamkin. The UniTESK Approach to Specification-Based Validation of Hardware Designs. IEEE-ISoLA'2006: The 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, November 2006.
16.обратно
17.обратноS.A. Edwards. Design and Verification Languages. Technical Report, Columbia University, New York, USA, November 2004.
18.обратноR. Armoni, L. Fix, A. Flaisher, R. Gerth, B. Ginsburg, T. Kanza, A. Landver, S. Mador-Haim, E. Singerman, A. Tiemeyer, M. Vardi, and Y. Zbar. The ForSpec Temporal Logic: A New Temporal Property-Specification Language. Tools and Algorithms for Construction and Analysis of Systems, 2002.
19.обратноI. Beer, S. Ben-David, C. Eisner, D. Fisman, A. Gringauze, and Y. Rodeh. The Temporal Logic Sugar. Lecture Notes in Computer Science, 2001.
20.обратно
21.обратноOpenVera® Language Reference Manual: Assertions. Version 1.4.1, November 2004.
22.обратно
23.обратно
24.обратноMIPS64™ Architecture For Programmers. Revision 2.0. MIPS Tecnologies Inc., June 9, 2003.

1(к тексту)Pentium - торговая марка нескольких поколений микропроцессоров семейства x86, выпускаемых компанией Intel с 22 марта 1993 года.
2(к тексту)Именно такие модели являются предметом исследования настоящей работы.
3(к тексту)Число транзисторов в современных микросхемах достигает сотней миллионов. Согласно закону Мура (Moore) это число возрастает примерно вдвое через каждые 18-24 месяцев.
4(к тексту)Мы не рассматриваем здесь разного рода неопределенные значения, часто используемые в моделировании аппаратного обеспечения.
5(к тексту)В дальнейшем будем называть такие процессы модельными процессами, чтобы отличать их от процессов операционной системы.
6(к тексту)В начале симуляции активными являются процессы, осуществляющие инициализацию.
7(к тексту)Для наглядности мы не вводим модель данных и не уточняем сигнатуры пред- и постусловий.
8(к тексту)Исключение составляет обходчик ndfsm [], позволяющий обходить графы состояний для некоторого класса недетерминированных конечных автоматов.
9(к тексту)Вариант логики LTL, используемой в ForSpec, называется FTL (ForSpec temporal logic) [].
10(к тексту)При подсчете числа входов и выходов не учитывался интерфейс JTAG (joint test action group) - стандартный интерфейс, используемый для тестирования аппаратуры с помощью метода граничного сканирования.


Содержание раздела







Главная сайта