Formal Methods for Functional Safety and Security in Cyber-Physical Systems
This course is designed to provide students with an introduction to formal methods as a framework for the specification, design, and verification of software-intensive embedded systems, with foci around provable functional safety and security targeted at cyber-physical systems (CPS). Formal methods topics include formal system specifications, automata theory, model checking, and automated/interactive theorem proving. Examples are driven by control systems and software systems from the automotive domain.
Students must bring their own laptop computers which should have Matlab, Advisor & Simulink installed.
What Will You Learn
- Utilize mathematical background to understand and use formal methods (set theory, propositional logic, first-order logic, automata theory, operational semantics, syntax & semantics, etc.)
- Describe and utilize modern system design flows used for embedded system design, implementation, and verification
- Define what formal methods are and how they are used in embedded systems design
- Explain how to translate informal requirements to formal specifications in languages such as linear temporal logic (LTL), signal temporal logic (STL), and hyperproperties (HyperLTL)
- Discover languages for formal specifications (LTL, STL, HyperLTL, etc.) and the applicability and appropriateness of various language choices for expressivity and efficiency
- Examine how formal specifications, formal models, and formal methods can be used in verification
- Summarize what model checking is and how it can be used in embedded systems verification
- Recite the theory behind satisfiability (SAT) solvers, satisfiability modulo theories (SMT) solvers, and model checking
- Simulate how model checking can be used for real time, continuous, and hybrid systems
- Discuss program analysis, both static and dynamic, and software tools for performing static and dynamic analysis of embedded software in languages such as C
- Contrast automated and interactive theorem proving and its use in embedded systems verification
Is This Course For You
Embedded software engineers, software testers, or engineers who have had at least a year of software or embedded systems design experience, are responsible for embedded systems and/or system architecture, and want to learn how formal methods can enhance functional safety in cyber-physical systems would benefit from attending. Familiarity with mathematics at the level of an undergraduate degree in engineering, computer science, or relevant experience in software design, implementation, and testing in software.
Module 1 - Formal Specifications and Models
This module will introduce students to formal specifications and formal models, and their use in embedded systems design and verification. The module starts with a review and introduction of background concepts that provide the mathematical foundation of formal specifications followed by formal models and semantics. Next, we focus on how to translate requirements to formal specifications and an introduction to languages (such as temporal logic) to express these specifications. The module closes with an application of formal specifications and formal models for verification as a lead in to learning modules II and III. The module will rely on use cases and examples from relevant automotive case studies.
- Introduction to Formal Methods (1.5 hours)
- What can we do? What can we not do?
- Where does this course fit in: Requirements, Requirements Compliance
- Verification vs. validation
- Comparisons to other verification methods – simulations, review, etc.
- Mathematical Background (2 hours)
- Motivation of background material with the formal verification problem
- Background and preliminaries
- Set theory, set builder notation, predicates
- Propositional logic/calculus
- Predicate/first-order logic
- Higher-order logics
- Duality between formulas and sets of states; duality between specifications and automata
- Formal Specifications and Formal Models (2 hours)
- Formal specifications: temporal logic, linear temporal logic (LTL), signal temporal logic (STL), hyperproperties (HyperLTL)
- Formal models: automata, syntax and semantics of programs, labeled transition systems
- Case Study Formal Specifications and Models (1 hour)
Module 2 - Model Checking and Formal Verification
This module introduces students to model checking and its use in embedded systems design and verification. The module starts with an introduction of model checking concepts and an overview of the variety of tools available for model checking. The next topics dive into the theory of model checking with a discussion of BDDs, SAT solvers, SMT solvers, and unbounded/bounded model checking. The next topics discuss models for real-time systems, such as timed, continuous, and hybrid systems, and how to use these models in the verification of these systems.
- Model checking (4 hours)
- Reachability analysis for safety verification
- Repeatability analysis for liveness verification
- Data structures for model checking (BDDs, etc.)
- SAT and SMT solving and solvers
- Explicit-state vs. symbolic model checking
- Software tools for model checking and SAT/SMT: NuSMV, Z3, nuXmv, Spin, etc.
- Advanced models: Real-time models (1.5 hours)
- Timed automata, hybrid automata, model checking for advanced models
- Other advanced models
- Case Study Formal Verification (1 hour)
Module 3 - Static/Dynamic Analysis, Theorem Proving, and Other Analyses
This module introduces basic theorem proving paradigms and its use in embedded systems design and verification. The module will start with an introduction to proofs and what it means for a software function to be correct, i.e., to meet its specifications. This is followed by topics on various prover techniques including inductive invariants, liveness proofs, and others. The module will introduce students to a wide variety of tools that can be used in practical automated and interactive theorem proving.
- Static and Dynamic Analysis (3 hours)
- Static analysis of source code
- Dynamic analysis of programs
- Software tools for static and dynamic analyses (Frama-C, Why3, Daikon, etc.)
- Theorem Proving (2 hours)
- Background and relation to static analysis of programs
- Software tools: Isabelle, PVS, Coq, TLA+
- Case Studies and Recent Automated/Interactive Theorem Proving Successes (1.5 hours)
- Formally verified microkernels (seL4)
- Formally verified optimizing compilers (CompCert for C)