Course Content

  1. Fundamentals: Review of Logic and Automated Verification: (1) Propositional and First-Order Logic, (2) Program verification basics – Hoare logic; Safety properties and invariants, (3) Model checking for Linear Temporal Logic. (9 hours)

  2. Introduction to Runtime Verification (RV).: Properties and Specifications. Monitorable properties and its characteristics. Overview of different Specification Languages. Overview of Monitor synthesis and instrumentation techniques. (6 hours)

  3. RV of Concurrent Systems: Types of Concurrency Errors - Atomicity and order violations, deadlocks, starvation, and Livelocks. Monitoring of Concurrent Systems and Error Detection techniques. (6 hours)

  4. Monitoring Events that Carry Data: Propositional and Parameterized RV, First-Order Temporal Logic, Monitoring Modulo Theories, Parametric Trace Slicing, Rule-based Monitoring, and Stream Processing (12 hours)

  5. Runtime Failure Prevention and Reaction: Monitor Synthesis. Redundancy based, failure type based, variants based reaction techniques (6 hours)

  6. RV for Decentralized and Distributed Systems: Applications of RV to Cyber-Physical Systems, Distributed Monitoring (3 hours)

Learning Outcomes

  1. Specify desirable properties of a system using appropriate formal language
  2. Implement techniques to synthesize monitors from the specified properties
  3. Design solutions to provide correctness guarantees (using RV) to actual systems

Text/Reference Books

  1. Ezio Bartocci, Yliès Falcone. 2018. Lectures on Runtime Verification. Springer. ISBN: 978-3-319-75632-5
  2. Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem. 2018. Handbook of Model Checking (1st. ed.). Springer. ISBN: 978-3-319-10575-8 (Chapters 2, 3, and 20)
  3. Research publications on Runtime Verification

Past Offerings

  • Offered in Aug-Dec, 2022 by Sandeep Chandran

Course Metadata

Item Details
Course Title Runtime Verification
Course Code CS5628
Course Credits 3-0-0-3
Course Category PME
Proposing Faculty Sandeep Chandran
Approved on Senate 21 of IIT Palakkad
Course status New