Course Code: CS591 Course Name: Formal Modelling and Analysis of Cyber-Physical Systems Prerequisites: Discrete Mathematics; Formal Languages and Automata Theory; or equivalent Syllabus: Modelling Discrete Systems: Finite state machines, automata, discrete-time, synchronous and asynchronous models of computation, invariants, safety and liveness requirements, deductive verification with theorem provers, satisfiability modulo theories; Temporal Logic and Model Checking: Kripke structures, branching time and linear-time temporal logics, model checking; Dynamical and hybrid system models: Continuous-time models, linear systems, feedback-control, stability, safety and reachability, hybrid dynamical models, timed automata, linear hybrid automata; Analysis techniques: Safety, reachability and stability verification, barrier certificates and Lyapunov functions, compositional techniques, abstraction and refinement, simulation and bisimulation; Advanced Topics: Verification of autonomous systems and systems with machine learning components; Case Studies: Examples of models from automotive, avionics, robotics, medical devices, etc., and their verification. References: 1. Rajeev Alur, Principles of Cyber-Physical Systems, MIT Press, 2015. 2. Sayan Mitra, Verifying Cyber-Physical systems, MIT Press, 2021. |