|Formal Methods for Functional Safety and Security in Cyber-Physical Systems|
|I.D. #||C1876||Duration||3 Days|
| 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.
| By attending this seminar, you will be able to:
|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.
| DAY ONE
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.
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.
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.
|Instructor(s):||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).