SW4600 Automata, Formal Specification and Run-time Verification

This course focuses on run-time monitoring and verification, a practical software verification technique based on automata and formal specifications. The automata section consists of finite automata (deterministic and non-deterministic), languages, and regular expressions. The formal specification section consists of temporal logics, real-time and time-series constraint specification, statecharts, and TLCharts. The run-time verification section will cover the practical application of formal specifications to monitoring and verification of safety critical systems. The course combines theory, examples, and practical student-driven projects. After taking this course you will know how to apply formal specifications and run-time verification to improve the dependability of defense systems.


CS3150 and MA2025

Lecture Hours


Lab Hours


Quarter Offered

  • Fall
  • As Required