National University of Sciences and Technology
Home | Back
CSE-952 ADVANCED MODEL CHECKING
Campus RCMS
Programs PG
Session Fall Semester 2016
Course Title ADVANCED MODEL CHECKING
Course Code CSE-952
Credit Hours 3
Pre-Requisutes None
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
  • System Verification
    • Model Checking
    • Characteristics of Model Checking
    • The Model-Checking Process
    • Strengths and Weaknesses
  • Modeling Concurrent Systems
    • Transition Systems
    • Parallelism and Communication
    • The State-Space Explosion Problem
  • Linear-Time Properties
    • Deadlock
    • Linear-Time Behavior
    • Safety Properties and Invariants
    • Live ness Properties
    • Fairness
  • Regular Properties
    • Automata on Finite Words
    • Model-Checking Regular Safety Properties
    • Automata on Infinite Words
    • Model-Checking -Regular Properties
  • Linear Temporal Logic
    • Linear Temporal Logic
    • Automata-Based LTL Model Checking
  • Computation Tree Logic
    • Computation Tree Logic
    • Expressiveness of CTL vs. LTL
    • Fairness in CTL
    • Counterexamples and Witnesses
    • Symbolic CTL Model Checking
  • Equivalences and Abstraction
    • Bi-simulation
    • Bi-simulation and CT Equivalence
    • Bi-simulation-Quotienting Algorithms
    • Simulation Relations
  • Partial Order Reduction
    • The Linear-Time Ample Set Approach
    • The Branching-Time Ample Set Approach
    • Independence of Actions
  • Timed Automata
    • Timed Automata
    • TCTL Model Checking
  • Probabilistic Systems
    • Markov Chains
    • Probabilistic Computation Tree Logic
    • Linear-Time Properties
    • Markov Chains with Costs
    • Markov Decision Processes
  • Model-checking tools
    • HyTech
    • UPPAAL
    • PRISM
Course Outcomes
  • After the completion of this course, the students would be able to model and verify the dynamics of complex dynamic systems, in any discipline including biology, computer science, electronics and engineering.
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.
  • GoranFrehse.Phaver: Algorithmic verification of hybrid systems past HYTECH. In HSCC, pages 258-273, 2005
  • A Tutorial on UPPAAL .GerdBehrmann, 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
Faculty/Resource Person Assistant Professor - Dr Jamil Ahmed