ZUT - Krajowe Ramy Kwalifikacji / Rok 2016/2017 / Wydział Informatyki / Informatyka (S2) / Sylabus przedmiotu - Testowanie i weryfikacja systemów sprzętowo-programowych

Wydział Informatyki - Informatyka (S2)

Sylabus przedmiotu Testowanie i weryfikacja systemów sprzętowo-programowych - Przedmiot obieralny II:

Informacje podstawowe

Kierunek studiów	Informatyka
Forma studiów	studia stacjonarne	Poziom	drugiego stopnia
Tytuł zawodowy absolwenta	magister
Obszary studiów	nauk technicznych
Profil	ogólnoakademicki
Moduł	—
Przedmiot	Testowanie i weryfikacja systemów sprzętowo-programowych - Przedmiot obieralny II
Specjalność	systemy komputerowe i technologie mobilne
Jednostka prowadząca	Katedra Architektury Komputerów i Telekomunikacji
Nauczyciel odpowiedzialny	Piotr Dziurzański <Piotr.Dziurzanski@zut.edu.pl>
Inni nauczyciele
ECTS (planowane)	2,0	ECTS (formy)	2,0
Forma zaliczenia	zaliczenie	Język	polski
Blok obieralny	14	Grupa obieralna	3

Formy dydaktyczne

Forma dydaktyczna	KOD	Semestr	Godziny	ECTS	Waga	Zaliczenie
laboratoria	L	2	15	0,8	0,50	zaliczenie
wykłady	W	2	15	1,2	0,50	zaliczenie

Wymagania wstępne

KOD	Wymaganie wstępne
W-1	Znajomość podstaw techniki cyfrowej

Cele przedmiotu

KOD	Cel modułu/przedmiotu
C-1	Zaznajomienie studentów z najważniejszymi technikami nowoczesnego testowania i weryfikacji systemów sprzętowo-programowych.

Treści programowe z podziałem na formy zajęć

KOD	Treść programowa	Godziny
laboratoria
T-L-1	Zapoznanie ze standardem JTAG.	2
T-L-2	Testowanie zewnętrzne i wewnętrzne z wykorzystaniem JTAG.	5
T-L-3	Formalna weryfikacja w systemie NuSMV.	2
T-L-4	Weryfikacja modeli z wykorzystaniem logiki CTL oraz LTL.	2
T-L-5	Testowanie systemów sprzętowo-programowych z wykorzystaniem języka PSL.	2
T-L-6	Weryfikacja dynamiczna z wykorzystaniem biblioteki SCV.	2
		15
wykłady
T-W-1	Walidacja a weryfikacja. Podział weryfikacji. Pokrycie kodu a pokrycie funkcjonalności. Uzysk i przyczyny zmniejszenia uzysku. Miara i jednostka jakości procesu testowania.	2
T-W-2	Kontrolowalność a obserwowalność. Ścieżka sterująca i typy SISO. Generatory wektorów testowych i sygnatury. Rodzaje rejestrów LFSR dla wielomianów prostych i odwrotnych. SISR a MISR. Tryby pracy BILBO.	2
T-W-3	Porty i rejestry w JTAG. Cztery tryby pracy komórki brzegowej. Instrukcje obowiązkowe JTAG. Instrukcje opcjonalne JTAG. Język BSDL. Podstawowe cechy standardu IEEE 1500.	3
T-W-4	Weryfikacja formalna. Logiki CTL, LTL i CTL*. Ograniczone sprawdzanie modeli.	2
T-W-5	Problem SAT dla formuły CNF. Klasy algorytmów rozwiązujących SAT. Naiwne wyszukiwanie wsteczne.	2
T-W-6	Warstwy w PSL. Operatory temporalne w PSL. Sugar Extended Regular Expressions (SEREs).	2
T-W-7	Środowisko testowe na poziomie transakcyjnym. Introspekcja danych w SCV. Nagrywanie transakcji w SCV. Typy randomizacji w SCV.	2
		15

Obciążenie pracą studenta - formy aktywności

KOD	Forma aktywności	Godziny
laboratoria
A-L-1	uczestnictwo w zajęciach	15
A-L-2	przygotowanie się do zajęć	8
A-L-3	Udzał w konsultacjach i zaliczeniu formy zajęć	2
		25
wykłady
A-W-1	uczestnictwo w zajęciach	15
A-W-2	przygotowanie się do zajęć	12
A-W-3	Udzał w konsultacjach i zaliczeniu formy zajęć	2
		29

Metody nauczania / narzędzia dydaktyczne

KOD	Metoda nauczania / narzędzie dydaktyczne
M-1	Wykład informacyjny
M-2	Wykład problemowy
M-3	Metoda przypadków
M-4	Ćwiczenia laboratoryjne

Sposoby oceny

KOD	Sposób oceny
S-1	Ocena podsumowująca: egzamin pisemny
S-2	Ocena podsumowująca: kolokwium pisemne

Zamierzone efekty kształcenia - wiedza

Zamierzone efekty kształcenia	Odniesienie do efektów kształcenia dla kierunku studiów	Odniesienie do efektów zdefiniowanych dla obszaru kształcenia	Cel przedmiotu	Treści programowe	Metody nauczania	Sposób oceny
I_2A_D18/O5/2-3_W01 Zaawansowana znajomość standardu JTAG i jego modyfikacji	I_2A_W05	T2A_W04, T2A_W07	C-1	T-W-3, T-L-1, T-L-2	M-1, M-2	S-1
I_2A_D18/O5/2-3_W02 Zaawansowana znajomość podstaw teoretycznych weryfikacji formalnej	I_2A_W01	T2A_W01	C-1	T-W-4, T-W-5, T-W-6, T-L-3, T-L-4, T-L-5	M-1, M-2	S-1

Zamierzone efekty kształcenia - umiejętności

Zamierzone efekty kształcenia	Odniesienie do efektów kształcenia dla kierunku studiów	Odniesienie do efektów zdefiniowanych dla obszaru kształcenia	Cel przedmiotu	Treści programowe	Metody nauczania	Sposób oceny
I_2A_D18/O5/2-3_U01 Potrafi przetestować funkcjonalnie system sprzętowy z wykorzystaniem zaawansowanych możliwości standardu JTAG.	I_2A_U08	T2A_U09, T2A_U18	C-1	T-W-3, T-L-1, T-L-2	M-3, M-4	S-2

Kryterium oceny - wiedza

Efekt kształcenia	Ocena	Kryterium oceny
I_2A_D18/O5/2-3_W01 Zaawansowana znajomość standardu JTAG i jego modyfikacji	2,0	nie spełnia wymogów na ocenę 3,0.
	3,0	zna budowę generatorów wektorów testowych i sygnatur, zna pojęcie rejestru LFSR, zna porty i rejestry JTAG oraz instrukcje obowiązkowe JTAG.
	3,5	jak na ocenę 3,0 oraz rozumie różnicę między SISR a MISR i zna tryby pracy obserwatora BILBO.
	4,0	jak na ocenę 3,5 oraz zna rodzaje rejestrów LFSR dla wielomianów prostych i odwrotnych, instrukcje opcjonalne JTAG oraz podstawy języka BSDL. Rozumie pojęcie introspekcji danych w SCV.
	4,5	jak na ocenę 4.0 oraz zna zaawansowane cechy języka BSDL, zna typy randomizacji w SCV.
	5,0	jak na ocenę 4,5 oraz zna podstawowe cechy standardu IEEE 1500.
I_2A_D18/O5/2-3_W02 Zaawansowana znajomość podstaw teoretycznych weryfikacji formalnej	2,0	nie spełnia wymogów na ocenę 3,0.
	3,0	zna podstawy weryfikacji formalnej w logice CTL, rozumie kwantyfikatory ścieżek oraz operatory temporalne X, F, G i U.
	3,5	jak na ocenę 3,0 oraz rozumie pojęcie formuł sprawiedliwych.
	4,0	jak na ocenę 3,5 oraz zna różnicę między logiką CTL a LTL, zna pojęcie ograniczonego sprawdzania modeli.
	4,5	jak na ocenę 4,0 oraz zna podstawy języka PSL, w tym SERE.
	5,0	jak na ocenę 4,5 oraz zna klasy algorytmów rozwiązujących SAT, a także rozumie pojęcie naiwnego wyszukiwania wstecznego.

Kryterium oceny - umiejętności

Efekt kształcenia	Ocena	Kryterium oceny
I_2A_D18/O5/2-3_U01 Potrafi przetestować funkcjonalnie system sprzętowy z wykorzystaniem zaawansowanych możliwości standardu JTAG.	2,0	nie spełnia wymogów na ocenę 3,0.
	3,0	potrafi dokonać testowania zewnętrznego z wykorzystaniem standardu JTAG, potrafi zapisać proste formuły w logice temporalnej CTL.
	3,5	jak na ocenę 3,0 oraz potrafi zaprojektować środowisko testwo z generatorem wektorów testowych i sygnatur, potrafi zapisać formuły sprawiedliwe.
	4,0	jak na ocenę 3,5 oraz potrafi wykorzystać język BSDL w procesie testowania, potrafi wykorzystywać instrukcje opcjonalne JTAG, potrafi dokonać introspekcji danych w SCV.
	4,5	jak na ocenę 4,0 oraz potrafi zapisać formuły w języku PSL (w tym SERE), potrafi wykorzystać różne cechy randomizacji w SCV.
	5,0	jak na ocenę 4,5 oraz potrafi zaplanować i przeprowadzić testowanie systemu sprzętowo-programowego z wykorzystaniem różnych technik statycznych i dynamicznych.

Literatura podstawowa

M. Fujita, I. Ghosh, M. Prasad, Verification Techniques For System-Level Design, MK, 2007
E. Clarke et. al., Model Checking, MIT Press, 1999
Kenneth P. Parker, The Boundary-scan Handbook, Springer, 2003

Literatura dodatkowa

L. Singh, L. Drucker, N. Khan, Advanced Verification Techniques: A SystemC Based Approach for Successful Tapeout, Kluwer, 2004
L.-T. Wang, C. E. Stroud, N. A. Touba, System-on-Chip Test Architectures, MK, 2007
K. Sapiecha, Testowanie i diagnostyka systemów cyfrowych, WNT, 1987
M. Zwoliński, Projektowanie układów cyfrowych z wykorzystaniem języka VHDL, WKiŁ, 2002
C. Eisner, D. Fisman, A Practical Introduction to PSL, Springer, 2006

Treści programowe - laboratoria

KOD	Treść programowa	Godziny
T-L-1	Zapoznanie ze standardem JTAG.	2
T-L-2	Testowanie zewnętrzne i wewnętrzne z wykorzystaniem JTAG.	5
T-L-3	Formalna weryfikacja w systemie NuSMV.	2
T-L-4	Weryfikacja modeli z wykorzystaniem logiki CTL oraz LTL.	2
T-L-5	Testowanie systemów sprzętowo-programowych z wykorzystaniem języka PSL.	2
T-L-6	Weryfikacja dynamiczna z wykorzystaniem biblioteki SCV.	2
		15

Treści programowe - wykłady

KOD	Treść programowa	Godziny
T-W-1	Walidacja a weryfikacja. Podział weryfikacji. Pokrycie kodu a pokrycie funkcjonalności. Uzysk i przyczyny zmniejszenia uzysku. Miara i jednostka jakości procesu testowania.	2
T-W-2	Kontrolowalność a obserwowalność. Ścieżka sterująca i typy SISO. Generatory wektorów testowych i sygnatury. Rodzaje rejestrów LFSR dla wielomianów prostych i odwrotnych. SISR a MISR. Tryby pracy BILBO.	2
T-W-3	Porty i rejestry w JTAG. Cztery tryby pracy komórki brzegowej. Instrukcje obowiązkowe JTAG. Instrukcje opcjonalne JTAG. Język BSDL. Podstawowe cechy standardu IEEE 1500.	3
T-W-4	Weryfikacja formalna. Logiki CTL, LTL i CTL*. Ograniczone sprawdzanie modeli.	2
T-W-5	Problem SAT dla formuły CNF. Klasy algorytmów rozwiązujących SAT. Naiwne wyszukiwanie wsteczne.	2
T-W-6	Warstwy w PSL. Operatory temporalne w PSL. Sugar Extended Regular Expressions (SEREs).	2
T-W-7	Środowisko testowe na poziomie transakcyjnym. Introspekcja danych w SCV. Nagrywanie transakcji w SCV. Typy randomizacji w SCV.	2
		15

Formy aktywności - laboratoria

KOD	Forma aktywności	Godziny
A-L-1	uczestnictwo w zajęciach	15
A-L-2	przygotowanie się do zajęć	8
A-L-3	Udzał w konsultacjach i zaliczeniu formy zajęć	2
		25

(*) 1 punkt ECTS, odpowiada około 30 godzinom aktywności studenta

Formy aktywności - wykłady

KOD	Forma aktywności	Godziny
A-W-1	uczestnictwo w zajęciach	15
A-W-2	przygotowanie się do zajęć	12
A-W-3	Udzał w konsultacjach i zaliczeniu formy zajęć	2
		29

(*) 1 punkt ECTS, odpowiada około 30 godzinom aktywności studenta

Pole	KOD	Znaczenie kodu
Zamierzone efekty kształcenia	I_2A_D18/O5/2-3_W01	Zaawansowana znajomość standardu JTAG i jego modyfikacji
Odniesienie do efektów kształcenia dla kierunku studiów	I_2A_W05	Ma rozszerzoną i podbudowaną teoretycznie wiedzę z zakresu metod informatyki wykorzystywanych do rozwiązywania problemów w wybranych obszarach nauki i techniki
Odniesienie do efektów zdefiniowanych dla obszaru kształcenia	T2A_W04	ma podbudowaną teoretycznie szczegółową wiedzę związaną z wybranymi zagadnieniami z zakresu studiowanego kierunku studiów
	T2A_W07	zna podstawowe metody, techniki, narzędzia i materiały stosowane przy rozwiązywaniu złożonych zadań inżynierskich z zakresu studiowanego kierunku studiów
Cel przedmiotu	C-1	Zaznajomienie studentów z najważniejszymi technikami nowoczesnego testowania i weryfikacji systemów sprzętowo-programowych.
Treści programowe	T-W-3	Porty i rejestry w JTAG. Cztery tryby pracy komórki brzegowej. Instrukcje obowiązkowe JTAG. Instrukcje opcjonalne JTAG. Język BSDL. Podstawowe cechy standardu IEEE 1500.
	T-L-1	Zapoznanie ze standardem JTAG.
	T-L-2	Testowanie zewnętrzne i wewnętrzne z wykorzystaniem JTAG.
Metody nauczania	M-1	Wykład informacyjny
Metody nauczania	M-2	Wykład problemowy
Sposób oceny	S-1	Ocena podsumowująca: egzamin pisemny
Kryteria oceny	Ocena	Kryterium oceny
	2,0	nie spełnia wymogów na ocenę 3,0.
	3,0	zna budowę generatorów wektorów testowych i sygnatur, zna pojęcie rejestru LFSR, zna porty i rejestry JTAG oraz instrukcje obowiązkowe JTAG.
	3,5	jak na ocenę 3,0 oraz rozumie różnicę między SISR a MISR i zna tryby pracy obserwatora BILBO.
	4,0	jak na ocenę 3,5 oraz zna rodzaje rejestrów LFSR dla wielomianów prostych i odwrotnych, instrukcje opcjonalne JTAG oraz podstawy języka BSDL. Rozumie pojęcie introspekcji danych w SCV.
	4,5	jak na ocenę 4.0 oraz zna zaawansowane cechy języka BSDL, zna typy randomizacji w SCV.
	5,0	jak na ocenę 4,5 oraz zna podstawowe cechy standardu IEEE 1500.

Pole	KOD	Znaczenie kodu
Zamierzone efekty kształcenia	I_2A_D18/O5/2-3_W02	Zaawansowana znajomość podstaw teoretycznych weryfikacji formalnej
Odniesienie do efektów kształcenia dla kierunku studiów	I_2A_W01	Ma poszerzoną i pogłębioną wiedzę w zakresie wybranych działów matematyki teoretycznej oraz matematyki stosowanej
Odniesienie do efektów zdefiniowanych dla obszaru kształcenia	T2A_W01	ma rozszerzoną i pogłębioną wiedzę z zakresu matematyki, fizyki, chemii i innych obszarów właściwych dla studiowanego kierunku studiów przydatną do formułowania i rozwiązywania złożonych zadań z zakresu studiowanego kierunku studiów
Cel przedmiotu	C-1	Zaznajomienie studentów z najważniejszymi technikami nowoczesnego testowania i weryfikacji systemów sprzętowo-programowych.
Treści programowe	T-W-4	Weryfikacja formalna. Logiki CTL, LTL i CTL*. Ograniczone sprawdzanie modeli.
	T-W-5	Problem SAT dla formuły CNF. Klasy algorytmów rozwiązujących SAT. Naiwne wyszukiwanie wsteczne.
	T-W-6	Warstwy w PSL. Operatory temporalne w PSL. Sugar Extended Regular Expressions (SEREs).
	T-L-3	Formalna weryfikacja w systemie NuSMV.
	T-L-4	Weryfikacja modeli z wykorzystaniem logiki CTL oraz LTL.
	T-L-5	Testowanie systemów sprzętowo-programowych z wykorzystaniem języka PSL.
Metody nauczania	M-1	Wykład informacyjny
Metody nauczania	M-2	Wykład problemowy
Sposób oceny	S-1	Ocena podsumowująca: egzamin pisemny
Kryteria oceny	Ocena	Kryterium oceny
	2,0	nie spełnia wymogów na ocenę 3,0.
	3,0	zna podstawy weryfikacji formalnej w logice CTL, rozumie kwantyfikatory ścieżek oraz operatory temporalne X, F, G i U.
	3,5	jak na ocenę 3,0 oraz rozumie pojęcie formuł sprawiedliwych.
	4,0	jak na ocenę 3,5 oraz zna różnicę między logiką CTL a LTL, zna pojęcie ograniczonego sprawdzania modeli.
	4,5	jak na ocenę 4,0 oraz zna podstawy języka PSL, w tym SERE.
	5,0	jak na ocenę 4,5 oraz zna klasy algorytmów rozwiązujących SAT, a także rozumie pojęcie naiwnego wyszukiwania wstecznego.

Pole	KOD	Znaczenie kodu
Zamierzone efekty kształcenia	I_2A_D18/O5/2-3_U01	Potrafi przetestować funkcjonalnie system sprzętowy z wykorzystaniem zaawansowanych możliwości standardu JTAG.
Odniesienie do efektów kształcenia dla kierunku studiów	I_2A_U08	Potrafi wykorzystywać narzędzia sprzętowo-programowe wspomagające rozwiązywanie wybranych problemów w różnych obszarach nauki i techniki
Odniesienie do efektów zdefiniowanych dla obszaru kształcenia	T2A_U09	potrafi wykorzystać do formułowania i rozwiązywania zadań inżynierskich i prostych problemów badawczych metody analityczne, symulacyjne i eksperymentalne
	T2A_U18	potrafi ocenić przydatność metod i narzędzi służących do rozwiązania zadania inżynierskiego, charakterystycznego dla studiowanego kierunku studiów, w tym dostrzec ograniczenia tych metod i narzędzi; potrafi - stosując także koncepcyjnie nowe metody - rozwiązywać złożone zadania inżynierskie, charakterystyczne dla studiowanego kierunku studiów, w tym zadania nietypowe oraz zadania zawierające komponent badawczy
Cel przedmiotu	C-1	Zaznajomienie studentów z najważniejszymi technikami nowoczesnego testowania i weryfikacji systemów sprzętowo-programowych.
Treści programowe	T-W-3	Porty i rejestry w JTAG. Cztery tryby pracy komórki brzegowej. Instrukcje obowiązkowe JTAG. Instrukcje opcjonalne JTAG. Język BSDL. Podstawowe cechy standardu IEEE 1500.
	T-L-1	Zapoznanie ze standardem JTAG.
	T-L-2	Testowanie zewnętrzne i wewnętrzne z wykorzystaniem JTAG.
Metody nauczania	M-3	Metoda przypadków
Metody nauczania	M-4	Ćwiczenia laboratoryjne
Sposób oceny	S-2	Ocena podsumowująca: kolokwium pisemne
Kryteria oceny	Ocena	Kryterium oceny
	2,0	nie spełnia wymogów na ocenę 3,0.
	3,0	potrafi dokonać testowania zewnętrznego z wykorzystaniem standardu JTAG, potrafi zapisać proste formuły w logice temporalnej CTL.
	3,5	jak na ocenę 3,0 oraz potrafi zaprojektować środowisko testwo z generatorem wektorów testowych i sygnatur, potrafi zapisać formuły sprawiedliwe.
	4,0	jak na ocenę 3,5 oraz potrafi wykorzystać język BSDL w procesie testowania, potrafi wykorzystywać instrukcje opcjonalne JTAG, potrafi dokonać introspekcji danych w SCV.
	4,5	jak na ocenę 4,0 oraz potrafi zapisać formuły w języku PSL (w tym SERE), potrafi wykorzystać różne cechy randomizacji w SCV.
	5,0	jak na ocenę 4,5 oraz potrafi zaplanować i przeprowadzić testowanie systemu sprzętowo-programowego z wykorzystaniem różnych technik statycznych i dynamicznych.