Spring 2024 || CS 691-002 || Jan 10, 2024 - Apr 26, 2024
Time: Mon & Wed, 3:30 pm - 4:45 pm
Location: Hardaway Hall 251
Schedule: Key dates, lecture slides, etc. posted at the end of the webpage -- scroll to the bottom of this page.
Email: bineet@ua.edu
Please add the following in subject line if you are emailing regarding the course: [S24-CS691] <your-subject>
Office: CYB 3053
Office Hours: Mon & Wed, 1:30 pm - 2:30 pm, or by appointment (bineet@ua.edu).
Last decade has a significant growth in deployment of autonomous systems in several places, such as, driving, factory floors, surgeries, wearables, and home assistants, etc. As a result of such diverse areas of its deployment, autonomous systems are required to operate in a wide range of environments with uncertainties (viz., sensor errors, timing errors, dynamic nature of the environment, etc). Such environmental uncertainties, even when present in small amounts, can have drastic impact on the safety of the system. In this course, we shall discuss formal techniques that are able to verify and design safe autonomous systems, even in the presence of such uncertainties, allowing for their trustworthy deployment in the real world.
Design and Verification of Autonomous Systems lies at the intersection of Formal Methods, Real-Time and Embedded Systems, and Control Theory, with practical applications in diverse domains such as Robotics, Automotive, Industrial and Home Automation Systems. Importantly, prior knowledge of Formal Methods, Real-Time and Embedded Systems, or Control Theory is NOT a prerequisite for this course, as we will cover the fundamental concepts during the class. The main objective of this course is to equip the students with the knowledge of techniques that guarantee performance and safety of autonomous systems, instilling trust in their deployment, especially in critical safety-critical situations.
Algorithms (CS 201/470)
Theory of Computation (CS 475)
Mathematical Maturity
Coding in Python (Or, strong background in other languages and willing to learn Python)
Speak to instructor, if unsure.
NO textbooks are required, but following textbooks can be very beneficial.
Formal Methods:
Control Systems
Introduction to Formal Methods:
Understand the fundamental concepts and principles of formal methods.
Gain insights into the techniques used for verifying the safety and correctness of programs and autonomous systems.
Explore the theoretical foundations of formal methods and their practical applications.
Autonomous Systems:
Understand the concept of autonomous systems.
Learn to model autonomous systems for formal analysis.
Learn about different types of models and their inherent properties.
Design and Verification of Safe Autonomous Systems:
Apply the formal methods introduced in the first part of the course to design and verify autonomous systems.
Explore real-world applications of safe autonomous systems, with a focus on automotive and robotics.
Review research papers related to formal methods in autonomous systems.
Engage in a course project that involves the design, verification, and practical implementation of safe autonomous systems, using knowledge from the course.
Being able to understand and use different types of formal modeling of autonomous systems.
Being able to understand and formalize safety and performance for given system in a given application scenario.
Being able to understand and apply formal techniques to prove correctness, and design safe systems.
Introduction
Autonomous systems
Notion of trust in deployment of autonomous systems
Formal Methods
Mathematical logic
Verifying correctness of programs
Software testing
Cyber-Physical and Autonomous Systems
Introduction to control theory
Linear systems
Hybrid automata
Verification of Autonomous Systems
Understanding uncertainties
Provable safety verification of autonomous systems
Designing provably safe and performance optimal systems
Homework (minimum 4): 30%
Paper presentation, and leading class discussion (1-3 papers): 30%
Final project: 30%
Class participation & student’s growth: 10%
Student’s growth. Identifies the effort being made by a student to understand the concepts being taught, despite their prior backgrounds. In other words, this can be used identify the efforts being put in by a student even if it is not being reflected in their scores. Discussing with instructor (especially during office hours) is a good way to demonstrate that.
Late work policy
One late homework submission will have
Any further late submission will result in the following deduction scheme:
Final project submission date is strict. Failure to submit the report on time will result in 0 score.
In case of emergency (or unforeseen cases), please speak to instructor. The instructor will try his best to accommodate for the situation (subject to proof) in accordance with the university policy.
Final project
Types: Survey (literature review), Application, Theory.
Logistics
Maximum of three people in a group.
Each group member is responsible to clearly identify their contribution.
1-3 reports maybe due before the final report and presentation to share progress with the class.
Presentation: 20-30 mins, followed by discussion, debate, comparative analysis.
Report: 8 page document in IEEE conference format (similar to conference paper).
The class activities are designed to promote active learning, critical thinking, and a understanding of the challenges in the design and verification of autonomous systems.
Lectures on Fundamental Topics. The initial portion of the course focuses on building a foundation by covering fundamental concepts and principles related to the design and verification of autonomous systems. These lectures provide students with essential theoretical knowledge and practical insights, ensuring they have the necessary background to engage effectively with advanced topics and projects later in the course.
Student Paper Presentations. Each student selects and presents one or more research papers relevant to the course. Following the presentation, there will be discussion, debate, comparative analysis (Note: this is the best way to demonstrate class participation and student's growth).
Though attendance will not be formally recorded, it is recommended the lectures are attended. Please note that lectures are the best way to demonstrate the student growth (which has
Further, if a student has missed noticeably many lectures (for instance, shows up only during their presentation), there will be a minimum of
Strongly recommend visiting during the office hours at least three times during the semester.
The instructor will make every effort to follow the guidelines of this syllabus as listed; however, the instructor reserves the right to amend this document as the need arises (including project due dates and test dates). In such instances, the instructor will notify students in class and/or via email and will endeavor to provide reasonable time for students to adjust to any changes.
Please refer to the university's standard course policies (Honor code, misconduct, behavior etc.) for details.
Please send me an email if you want the lecture slides
Lecture 1, Jan 10, 2024
Introduction to the course
Syllabus
Jan 15, 2024
Lecture 2, Jan 17, 2024
Introduction to autonomous systems
Why safety verification?
Role of uncertainties
Lecture 3, Jan 22, 2024
Introduction to autonomous systems verification
Introduction to designing safe autonomous systems
Lecture 4, Jan 24, 2024
Representing system models
Computing trajectories
Safety Verification
Impact of uncertainties
Lecture 5, Jan 29, 2024
Introduction to reachable sets
Homework 1 posted in Blackboard. Deadline: 11:59pm, Feb. 5, 2024.
Lecture 6, Jan 31, 2024
Introduction to formal methods
Propositional logic
Lecture 7, Feb 5, 2024
Propositional logic and its applications
Homework 1 is due today by 11:59pm.
Lecture 8, Feb 7, 2024
Practical problems with propositional logic
Natural deduction
Lecture 9, Feb 12, 2024
Semantic entailment
Soundness and completeness
Useful theorems
Homework 2 posted in Blackboard. Deadline: 11:59pm, Feb. 19, 2024.
Lecture 10, Feb 14, 2024
Predicate logic
Proof rules
Predicate logic and program verification
Lecture 11, Feb 19, 2024
Higher order logics
Hoare logic
Homework 2 is due today by 11:59pm.
Lecture 12, Feb 21, 2024
Abstract interpretation
Partial order and lattices
Lecture 13, Feb 26, 2024
In-class activity
Lecture 14, Feb 28, 2024
Abstract interpretation
Galois connection
Counter–Example Guided Abstraction Refinement (CEGAR)
Handout:
A recent paper on Monitoring Autonomous Systems (see Blackboard)
You are strongly encouraged to submit a synopsis of the paper.
Lecture 15, Mar 4, 2024
Cyber-physical systems
Lecture 16, Mar 6, 2024
Monitoring
Mar 11, Mar 13
Lecture 17, Mar 18, 2024
Modeling physical systems
State space equations
Time varying and time invariant systems
Lecture 18, Mar 20, 2024
Dynamical systems
LET paradigm
Closed loop controllers
Stability
Hands-on with Python
Key dates discussed (due dates for student presentations, final project report etc.)
List of papers posted for student presentation in Blackboard. Deadline: 11:59pm, Apr. 1, 2024.
Lecture 19, Mar 25, 2024
Stability in presence of deadline misses
Stability vs. safety
Discrete systems
Homework 3 posted in Blackboard. Deadline: 11:59pm, Apr. 1, 2024.
Lecture 20, Mar 27, 2024
Controller design
Handout on project formalization
Lecture 21, Apr 1, 2024
Revising linear algebra
State space solutions
Laplace transformation
Paper preferences due today by 11:59pm.
Homework 3 is due today by 11:59pm.
Homework 4 posted in Blackboard. Deadline: 11:59pm, Apr. 8, 2024.
Important dates discussed
Project Discussions, Apr 3, 2024
In-class activity focused on project
Lecture 22, Apr 8, 2024
Stability
Homework 4 is due today by 11:59pm.
Lecture 23, Apr 10, 2024
Stability
Student Presentations, Apr 15, 2024
Slides for student presentations due today by 3:00pm.
Student presentation
In-class activity focused on project
Student Presentations, Apr 17, 2024
Student presentation
In-class activity focused on project
Lecture 24, Apr 22, 2024
LQR Control
[Last Lecture] Lecture 25, Apr 24, 2024
LQR Control
Project progress report is due today by 11:59pm.
May 1, 2024
Final project report is due today by 11:59pm.