Browse Learn C1876

Formal Methods for Functional Safety and Security in Cyber-Physical Systems C1876

Cybersecurity is a critical concern in the development of modern vehicle systems and is becoming increasingly important as demonstrated by recent vulnerabilities in the field. With the increasing integration of communications interfaces, such as through vehicle-to-smartphone infotainment systems, vehicle-to-vehicle (V2V) / vehicle-to-infrastructure (V2I)/etc. (V2X), controller area network (CAN) dongles, and others, the attack surfaces for modern vehicles have grown substantially. Formal methods provide the capability to specify, model, verify, and integrate into modern embedded systems and CPS design flows for enhancing functional safety and security. The past few years have led to substantial advancements in automated and semi-automated analysis methods, with recent successes such as the seL4 formally verified microkernel, the CompCert formally verified optimizing C compiler, and secure vehicles and drones emerging from DARPA’s High-Assurance Cyber Military Systems (HACMS) program.

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.

Learning Objectives
By attending this seminar, you will be able to:
  • 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

Who Should Attend

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.


Course attendees should have an undergraduate degree in engineering, computer science, or related fields to have at least one year of experience working in industry in software-related areas of embedded systems, CPS design and engineering, or relevant experience in software design, implementation, and testing. No prior knowledge in formal methods or formal verification is necessary.


Note: See related course, Introduction to the Secure Microkernel, seL4, for more in-depth training.

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
    • Induction
    • 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)
DAY TWO 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)
Taylor T. Johnson

Dr. Taylor T. Johnson is an Assistant Professor in the Department of Electrical Engineering and Computer Science (EECS) at Vanderbilt University, where he directs the Verification and Validation for Intelligent and Trustworthy Autonomy Laboratory (VeriVITAL) and is a Senior Research Scientist in the Institute for Software Integrated Systems (ISIS). He has published over 70 papers on verification and validation (V&V) methods building on formal methods, control theory, software engineering, and distributed systems, and their applications across CPS domains such as power and energy systems, aerospace and avionics systems, automotive systems, transportation systems, and robotics. Taylor has performed research with the US Air Force Research Laboratory (AFRL) at their Air Vehicles, Information, and Space Vehicles directorates, respectively in Dayton, OH, Rome, NY, and Albuquerque, NM. Taylor is a 2018 and 2016 recipient of the US Air Force Office of Scientific Research (AFOSR) Young Investigator Program (YIP) award, a 2015 recipient of the National Science Foundation (NSF) Computer and Information Science and Engineering (CISE) Research Initiation Initiative (CRII), and his research is / has been supported by AFRL, AFOSR, , the US Army Research Office (ARO), the MathWorks, the US Defense Advanced Research Projects Administration (DARPA), the US National Security Agency (NSA), NSF, NVIDIA, the US Office of Naval Research (ONR), Toyota, and the US Department of Transportation (USDOT), totaling over $25 million in awarded US federal research support since 2013. Taylor is a member of AAAS, ACM, AIAA, IEEE, SAE, and is registered as a TN Professional Engineer Intern (EiT).

Hotel & Travel Information

Fees: $1800.00
SAE Members: $1440.00 - $1620.00

2.0 CEUs
You must complete all course contact hours and successfully pass the learning assessment to obtain CEUs.

To register, click the Register button above or contact SAE Customer Service 1-877-606-7323 (724-776-4970 outside the U.S. and Canada) or at

Duration: 3 Days
March 4-6, 2019 (8:30 a.m. - 4:30 p.m.) - Troy, Michigan