National University of Sciences and Technology
Home | Back
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