VAI ALLA VERSIONE ITALIANA

OTHER ACADEMIC YEARS

Index:

Exams

Course programme

Textbooks

Class material

Class timetable

Software

Exams

Exams Rules

Please check lesson 1.

Exams Dates

N	Date	Hour	Where	Notes	Register	Deadline
1	12/06/2023	09:00 - 10:00	A1.2
2	29/06/2023	09:00 - 10:00
3	13/07/2023	09:00 - 10:00
4	07/09/2023	09:00 - 10:00
5
6
7
straord

Course Programme

Introduction to Verification

• verification problem
• testing, model checking and other methodologies

Model Checking for Finite State Systems

• Murphi, SPIN and NuSMV
• CTL and LTL
• model checking algorithms: theoretical, explicit, symbolic, bounded model checking

Testing

• main techniques: functyional and structural testing
• testing within software development process: unit, integration, regression and system testing
• JUnit

Validation

• acceptance testing

Textbooks:

• Mauro Pezzé, Michal Young: Software Testing and Analysis: Process, Principles, and Techniques, Wiley
• A version of this book is available here
• Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, Roderick Bloem (Editors): Handbook of Model Checking, Springer
• A version of this book is available here
• Christel Baier, Joost-Pieter Katoen: Principles of Model Checking, MIT Press
• A version of this book is available here

Class Material

N	Date	Material	Arguments	Notes
1	27/02/2023	slides	Introduction to testing, validation and verification of software systems	Slides 1-53
2	03/03/2023	slides Murphi models	The Murphi model checker: input language	Lesson 1: slides 54-end. Lesson 2: Slides 1-end
3	06/03/2023	slides	The Murphi model checker: verification algorithm (part 1)	Slides 1-59
	10/03/2023		CANCELED
4	13/03/2023	slides	The Murphi model checker: verification algorithm (part 2). Safety e liveness properties. LTL	Lesson 3: Slides 60-end. Lesson 4: Slides 1-25
5	17/03/2023	slides	CTL temporal logic. CTL Model Checking algoriths	Lesson 4: Slides 26-end. Lesson 5: Slides 1-18
6	20/03/2023	slides	LTL Model Checking Algorithms. SPIN and Promela (part 1)	Lession 5: Slides 19-end. Lesson 6: Slides 1-10
7	24/03/2023	See slides in lesson 6	SPIN and Promela (part 2)	Slides 11-43
8	27/03/2023	See slides in lezione 6 models	SPIN and Promela (part 3)	Slides 44-66
9	31/03/2023	slides	SPIN and Promela (conclusion). NuSMV (part 1)	Lesson 6: Slides 67-end. Lesson 7: Slides 1-14
10	03/04/2023	See slides in lesson 9	NuSMV (part 2)	Slides 15-43
11	14/04/2023	See slides in lesson 9 models and scripts	NuSMV (part 3)	Slides 44-62
12	17/04/2023	See slides in lesson 9 models and scripts	NuSMV (part 4)	Slides 63-end
13	21/04/2023	slides	Introduction to Testing	Slides 1-end
14	28/04/2023	slides	Testing: Finite Models
15	05/05/2023	slides examples	Testing: Methodologies (part 1: Category-Partition Testing)	Slides 1-42
16	08/05/2023	See slides in lesson 15	Testing: Methodologies (part 2: Catalog-Based and Pairwise Testing)	Slides 43-69
17	12/05/2023	See slides in lesson 15	Testing: Methodologies (part 3: Adequacy Criteria for Structural Testing)	Slides 70-90
18	15/05/2023	See slides in lesson 15	Testing: Methodologies (part 4: Data Flow Testing, Usage of Finite State Machine and Decision Tables in Testing)	Slides 91-119
19	19/05/2023	See slides in lesson 15	Testing: Methodologies (part 5: Usage of Control Flow Graph and Grammars in Testing; Testing of Object Oriented Software)	Slides 120-152
20	22/05/2023	See slides in lesson 15	Testing: Methodologies (part 6: Testing of Object Oriented Software)	Slides 153-180
21	26/05/2023	See slides in lesson 15	Testing: Methodologies (part 7: Scaffolding)	Slides 181-end
22	29/05/2023	slides	Integration, System, Acceptance and Regression Testing	Slides 1-end
23	05/06/2023		Review of students' projects
24	09/06/2023		Review of students' projects

Class Timetable

Day	From	To	Where
Monday	4:30PM	6:30PM	A1.2
Friday	11:30AM	13:30AM	A1.2

Room A1.2 is at second floor of the "Alan Turing" building.

Free software for this course

• CMurphi
• SPIN
• NuSMV
• JUnit