|Monday||2:30 PM - 5:30 PM||lesson||Lecture Hall I|
|Tuesday||2:30 PM - 4:30 PM||lesson||Laboratory Laboratorio Ciberfisico||from Mar 15, 2016 to Jun 10, 2016|
|Tuesday||4:30 PM - 6:30 PM||lesson||Lecture Hall I|
The course presents problems related to the verification of complex systems and its related techniques.
The course introduces the problem of modeling complex and highly critical systems, such as railway systems, avionics, spatial and project control systems, and the related requirements. It presents transition systems and their symbolic representation as propositional logic. It presents temporal logic: Computation Tree Logic, Linear Temporal Logic and CTL*. It describes algorithms for model checking verification of CTL and the generalization to transition systems with fairness constraints. It presents the translation of LTL model checking into CTL model checking with fairness constraints. It presents symbolic algorithms for model checking, based on Binary Decision Diagrams (BDD), and algorithms based on propositional satisfiability (SAT). It describes aspects of reliability and analysis of systems with Triple Modular Redundancy (TMR), Fault Tree Analysis notions and algorithms to compute the cut sets and for minimization. It presents the notions of abstraction, refinement and predicate abstraction. It describes temporal systems and hybrid automata and related decidability issues. The course is integrated with exercises with the use of a BDD package and of the model checker NuSMV.
Oral examination or software project