verifying cyber-physical systems

Slides and Code

Verifying cyberphysical systems, by Sayan Mitra. published by MIT Press, February 2021.

Chapters

  1. Introduction

  2. Modeling computation

  3. Modeling physics

    • slides pptx pdf
    • pre-lecture notes 2021 note pdf
    • post-lecture notes 2021 note pdf
    • code for simple economy model py
    • code for SIR epidemic model py
    • code for vehicle model py
    • stabilityx
    • pre-lecture notes 2021 note pdf
    • post-lecture notes 2021 note pdf

  4. Modeling cyberphysical systems

  5. Composing models

  6. Specifying requirements

    • Computational tree logic (CTL) and CTL model checking: slides pptx pdf
    • Computational tree logic (CTL) and CTL model checking: slides 2021 pptx pdf

  7. Verifying invariants

  8. Abstractions and compositional reasoning

    • Abstractions, simulation relations, substitutivity, and CEGAR: slides pptx pdf
    • pre-lecture notes 2021 note pdf

  9. Reachability analysis

    • Timed automata: slides pptx pdf
    • FSMA and Timed automata: slides 2021 pptx pdf
    • Undecidability problem for hybrid automata: slides pptx pdf
    • post-lecture notes 2021 note pdf

  10. Progress analysis

    • Progress of automata and stability of hybrid systems: slides pptx pdf
    • pre-lecture notes 2021 note pdf

  11. Data-driven verification

    • Progress of automata and stability of hybrid systems: slides pptx pdf

  12. Appendix A. Linear algebra and real analysis

  13. Appendix B. Computability and complexity

  14. Appendix C. Specification language reference

This project is maintained by sayanmitracode