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

Wydział Informatyki - Informatyka (S1)

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

Informacje podstawowe

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

Formy dydaktyczne

Forma dydaktyczna	KOD	Semestr	Godziny	ECTS	Waga	Zaliczenie
laboratoria	L	7	15	1,5	0,38	zaliczenie
wykłady	W	7	15	1,5	0,62	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ęć	20
A-L-3	Udział w zaliczeniu i konsultacjach	2
A-L-4	Przygotowanie sprawozdań	7
		44
wykłady
A-W-1	uczestnictwo w zajęciach	15
A-W-2	przygotowanie się do zajęć	22
A-W-3	Udział w zaliczeniu i konsultacjach	2
A-W-4	Przygotowanie się do zaliczenia wykładu	5
		44

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: Ocena wiedzy i umiejętności wykazana na egzaminie pisemnym o charakterze problemowym

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	Odniesienie do efektów kształcenia prowadzących do uzyskania tytułu zawodowego inżyniera	Cel przedmiotu	Treści programowe	Metody nauczania	Sposób oceny
I_1A_O4/10_W01 Znajomość testowania dynamicznego systemów sprzętowo-programowych oraz standardu JTAG	I_1A_W03	—	—	C-1	T-L-1, T-L-2, T-W-3	M-1, M-2, M-3, M-4	S-1
I_1A_O4/10_W02 Znajomość podstaw teoretycznych weryfikacji formalnej	I_1A_W01	—	—	C-1	T-L-4, T-L-5, T-L-6, T-L-3, T-W-4, T-W-5, T-W-6, T-W-7	M-1, M-2, M-3, M-4	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	Odniesienie do efektów kształcenia prowadzących do uzyskania tytułu zawodowego inżyniera	Cel przedmiotu	Treści programowe	Metody nauczania	Sposób oceny
I_1A_O4/10_U01 Przeprowadzanie testów układów cyfrowych z wykorzystaniem standardu JTAG oraz przeprowadzania weryfikacji formalnej i systemów sprzętowo-programowych	I_1A_U01, I_1A_U02, I_1A_U04, I_1A_U18	—	—	C-1	T-L-1, T-L-2, T-W-3	M-1, M-2, M-3, M-4	S-1

Kryterium oceny - wiedza

Efekt kształcenia	Ocena	Kryterium oceny
I_1A_O4/10_W01 Znajomość testowania dynamicznego systemów sprzętowo-programowych oraz standardu JTAG	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_1A_O4/10_W02 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_1A_O4/10_U01 Przeprowadzanie testów układów cyfrowych z wykorzystaniem standardu JTAG oraz przeprowadzania weryfikacji formalnej i systemów sprzętowo-programowych	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ęć	20
A-L-3	Udział w zaliczeniu i konsultacjach	2
A-L-4	Przygotowanie sprawozdań	7
		44

(*) 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ęć	22
A-W-3	Udział w zaliczeniu i konsultacjach	2
A-W-4	Przygotowanie się do zaliczenia wykładu	5
		44

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

Pole	KOD	Znaczenie kodu
Zamierzone efekty kształcenia	I_1A_O4/10_W01	Znajomość testowania dynamicznego systemów sprzętowo-programowych oraz standardu JTAG
Odniesienie do efektów kształcenia dla kierunku studiów	I_1A_W03	zna podstawy elektroniki, techniki analogowej i cyfrowej, ze szczególnym uwzględnieniem ich stosowanych aspektów, niezbędne do opisu i analizy działania systemów elektronicznych, w tym systemów zawierających układy programowalne
Cel przedmiotu	C-1	Zaznajomienie studentów z najważniejszymi technikami nowoczesnego testowania i weryfikacji systemów sprzętowo-programowych.
Treści programowe	T-L-1	Zapoznanie ze standardem JTAG.
	T-L-2	Testowanie zewnętrzne i wewnętrzne z wykorzystaniem JTAG.
	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.
Metody nauczania	M-1	Wykład informacyjny
	M-2	Wykład problemowy
	M-3	Metoda przypadków
	M-4	Ćwiczenia laboratoryjne
Sposób oceny	S-1	Ocena podsumowująca: Ocena wiedzy i umiejętności wykazana na egzaminie pisemnym o charakterze problemowym
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_1A_O4/10_W02	Znajomość podstaw teoretycznych weryfikacji formalnej
Odniesienie do efektów kształcenia dla kierunku studiów	I_1A_W01	ma wiedzę z matematyki teoretycznej ze szczególnym uwzględnieniem jej stosowanych aspektów, matematyki dyskretnej oraz matematyki stosowanej
Cel przedmiotu	C-1	Zaznajomienie studentów z najważniejszymi technikami nowoczesnego testowania i weryfikacji systemów sprzętowo-programowych.
Treści programowe	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.
	T-L-6	Weryfikacja dynamiczna z wykorzystaniem biblioteki SCV.
	T-L-3	Formalna weryfikacja w systemie NuSMV.
	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-W-7	Środowisko testowe na poziomie transakcyjnym. Introspekcja danych w SCV. Nagrywanie transakcji w SCV. Typy randomizacji w SCV.
Metody nauczania	M-1	Wykład informacyjny
	M-2	Wykład problemowy
	M-3	Metoda przypadków
	M-4	Ćwiczenia laboratoryjne
Sposób oceny	S-1	Ocena podsumowująca: Ocena wiedzy i umiejętności wykazana na egzaminie pisemnym o charakterze problemowym
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_1A_O4/10_U01	Przeprowadzanie testów układów cyfrowych z wykorzystaniem standardu JTAG oraz przeprowadzania weryfikacji formalnej i systemów sprzętowo-programowych
Odniesienie do efektów kształcenia dla kierunku studiów	I_1A_U01	potrafi w zakresie podstawowym projektować, implementować i testować oprogramowanie
	I_1A_U02	potrafi aktywnie uczestniczyć w pracach projektowych zespołowych i indywidualnych
	I_1A_U04	ma podstawowe umiejętności w zakresie programowania i podnoszenia niezawodności systemów wbudowanych
	I_1A_U18	umie opisywać i analizować działanie prostych systemów elektronicznych, w tym systemów zawierających układy programowalne
Cel przedmiotu	C-1	Zaznajomienie studentów z najważniejszymi technikami nowoczesnego testowania i weryfikacji systemów sprzętowo-programowych.
Treści programowe	T-L-1	Zapoznanie ze standardem JTAG.
	T-L-2	Testowanie zewnętrzne i wewnętrzne z wykorzystaniem JTAG.
	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.
Metody nauczania	M-1	Wykład informacyjny
	M-2	Wykład problemowy
	M-3	Metoda przypadków
	M-4	Ćwiczenia laboratoryjne
Sposób oceny	S-1	Ocena podsumowująca: Ocena wiedzy i umiejętności wykazana na egzaminie pisemnym o charakterze problemowym
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.