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:
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.
You must complete all course contact hours and successfully pass the learning assessment to obtain CEUs.
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).