NUST - PG Courses

CSE-952 Advanced Model Checking

Campus	RCMS
Programs	PG
Session	Spring Semester 2017
Course Title	Advanced Model Checking
Course Code	CSE-952
Credit Hours	3-0
Pre-Requisutes	Basic Computer Programming
Course Objectives	Having completed this course, students will be able to model the behavior of reactive systems using finite-state machines and temporal logic. They will understand and be able to use model checkers to check whether crucial properties are satisfied
Detail Content	Introduction Automata Introductory Examples A Few Definitions A Printer Manager A Few More Variables Synchronized Product Synchronization by Message Passing Synchronization by Shared Variables Temporal Logic The Language of Temporal Logic The Formal Syntax of Temporal Logic The Semantics of Temporal Logic PLTL and CTL: Two Temporal Logics The Expressivity of CTL* Model Checking Model Checking CTL Model Checking PLTL The State Explosion Problem Symbolic Model Checking Symbolic Computation of State Sets Binary Decision Diagrams (BDD) Representing Automata by BDDs BDD-based Model Checking Timed Automata Decommention of a Timed Automaton Networks of Timed Automata and Synchronization Variants and Extensions of the Basic Model Timed Temporal Logic Timed Model Checking Reachability Properties Reachability in Temporal Logic Model Checkers and Reachability Computation of the Reachability Graph Safety Properties Safety Properties in Temporal Logic A Formal Definition Safety Properties in Practice The History Variables Method Liveness Properties Simple Liveness in Temporal Logic Are Liveness Properties Useful? Liveness in the Model, Liveness in the Properties Verification under Liveness Hypotheses Bounded Liveness Deadlock-freeness Safety? Liveness? Deadlock-freeness for a Given Automaton Beware of Abstractions! Fairness Properties Fairness in Temporal Logic Fairness and Nondeterminism Fairness Properties and Fairness Hypotheses Strong Fairness and Weak Fairness Fairness in the Model or in the Property? Abstraction Methods When Is Model Abstraction Required? Abstraction by State Merging What Can Be Proved in the Abstract Automaton? Abstraction on the Variables Abstraction by Restriction Observer Automata Introduction SMV - Symbolic Model Checking What Can We DO with SMV? SMV's Essentials Describing Automata Verification Synchronizing Automata Documentation and Case Studies SMV Bibliography SPIN - Communicating Automata What Can We DO with SPIN? SPIN's Essentials Describing Processes Simulating the System Verification Documentation and Case Studies UPPAAL - Timed Systems What Can We DO with UPPAAL? UPPAAL'S Essentials Modeling Timed Systems with UPPAAL Simulating a System Verification Documentation and Case Studies HYTECH - Linear Hybrid Systems What Can We DO With HYTECH? HYTECH'S Essentials Describing Automata System Analysis Parametric Analysis Documentation and Case Studies
Text/Ref Books	E.-R. Olderog and H. Dierks: Real-Time Systems. Cambridge University Press, 2008. B. Bérard et al.: Systems and Software Verification: Model-Checking Techniques and Tools, Springer 2001. C. Baier and J.-P. Katoen: Principles of Model Checking, MIT Press, 2008. T-A. Henzinger, P-H. Ho, and H. Wong-Toi. HYTECH: A model checker for hybrid systems. International Journal on Software Tools for Technology Transfer, 1(1-2):110-122,1997. Goran Frehse. Phaver: Algorithmic verification of hybrid systems past HYTECH. In HSCC, pages 258-273, 2005 A Tutorial on UPPAAL Gerd Behrmann, Alexandre David, and Kim G. Larsen. In proceedings of the 4th International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM-RT'04). LNCS number 3185, Springer.
Time Schedule	Spring Semester 2017
Faculty/Resource Person	Dr. Jamil Ahmad PhD (Ecole Centrale de Nantes) France Discipline: Applied Computer Science Specialization: System Biology and Model Checking