COURSE PRESENTATION FORM - FORMAL METHODS - 2009/2010


COURSE NAME: Formal Methods

COURSE CODE: 70144 (BSc + MSc Old – DM 509) / 70058 (BSc Old)

LECTURER: Alessandro Artale

TEACHING ASSISTANT: Enrico Franconi

TEACHING LANGUAGE: English

CREDIT POINTS: 4

LECTURE HOURS: 24

EXERCISE HOURS: 12

TIMESPAN: 28.09.2009 - 23.01.2010

TIMETABLE: see Timetable Page

OFFICE HOURS LECTURER: Tuesday from 15:00 to 17:00 the office for contract professors is Palais Trapp, Via della Mostra 4, office 1.02

OFFICE HOURS TEACHING ASSISTANT: Tuesday from 15:00 to 17:00 the office for contract professors is Palais Trapp, Via della Mostra 4, office 1.02

PREREQUISITES
Logic

OBJECTIVES
In this module students will develop a deeper understanding of technologies based on applying formal methods for the specification and verification of hardware systems. Students will learn the most important techniques based on Model Checking to check properties of a system. In particular, the student will be able to understand how to formally specify an hardware system by means of transition systems and how to express computation properties by means of formulas in Temporal Logic. Both Linear Temporal Logic (LTL) and Computation Tree Logic (CTL) will be studied together with efficient algorithms for model checking formulas in these logics. During the lab a tutorial on NuSMV will introduce the student to one of the most successfull software used in industrial applications to specify and test syncronous concurrent systems and critical software.

SYLLABUS

• Modeling Systems as Transition Systems.
• Temporal Logics: 1. Linear Temporal Logic (LTL); 2. Computation Tree Logic (CTL and CTL*)
• Model Checking CTL formulas.
• Ordered Binary Decision Diagrams (OBDD’s).
• CTL Symbolic Model Checking.
• Model Checking Vs. Proof Theory

TEACHING FORMAT
Frontal lectures and lab

ASSESSMENT

• SMV Project (20%)
• Final Written Exam (80%)

READING LIST 

• Logic in Computer Science--Modelling and Reasoning about Systems. Michael Huth and Mark Ryan. Publisher: Cambridge University Press, 2004. (Text Book)
• Model Checking. Edmund Clarke, Orna Grumberg and Doron Peled. Publisher: MIT Press, 1999.

SOFTWARE USED
NuSMV

LEARNING OUTCOME
As a final result of this course, Students will be able to understand the techniques used to specify and verify a hardware component using a formal model checking procedure. Students will be able to understand the meaning of Temporal Logic formulas based on both LTL and CTL and to specify computation properties using such formal languages. Finally, they will be able to use and run the model checker software NuSMV.

COURSE PAGE