NEW! FORMAL METHODS FOR FUNCTIONAL SAFETY AND SECURITY IN CYBER-PHYSICAL SYSTEMS
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
Prerequisites: 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.
12
3 ways to get a no-obligation price quote to deliver a course to your company Call SAE Corporate Learning at +1.724.772.8529 | Fill out the online quote request at sae.org/corplearning Email us at Corplearn@sae.org
Made with FlippingBook Online document