| Table of Contents |
|---|
Labs & Assignments
This course includes written theory homework assignments and lab assignments. Roughly, the homework assignments and the labs are due in alternating weeks.
Labs 0 and 1 must be done individually. Later labs can be done individually or in pairs. You must choose a partner by the due date of the betabot for the lab 2. If you have difficulty finding a partner, or if problems in your working relationship arise during the semester, please get in touch with the instructor as soon as possible. Written assignments must be done individually.
Labs
In the labs, you will design and program robot controllers for increasingly more difficult challenges. You will start with developing a robot controller for a simple task (moving on a rail without any obstacles). Throughout the course of this semester, you will make your robot controller increasingly more sophisticated until it can master free motion in two dimensions, like, e.g., a corridor of a building. Your controller will need to reach its goal position but without colliding with any obstacles.
You do not need to build the robotic hardware but will build CPS programs and controllers instead.
Grading
The most important criterion is always correctness. Buggy code is useless, and is likely to get a low score. A secondary criterion is the performance of your robot controller in terms of reaching its goal and interacting with its environment. Your robot controllers will also be graded based on how they score in interaction with robot controllers by other students.
Grading for written assignments is based on the correctness of the answer and the presentation of your reasoning. Strive for clarity and conciseness, but show how you arrived at the answer. Stating an answer without explanation does not count as an answer. If you cannot solve a problem, explaining your approach and why you failed is encouraged. Such answers will be given partial credit.
Lab Overview
The mathematical theory behind core CPS principals will be covered in 5 written homework assignments, as well as a midterm and final exam.
Students will also demonstrate a working knowledge of the theory by designing autonomous robot controllers in a series of 5 lab assignments. Students will prove that their robots always operate within safety specifications, even when malicious robots (called rogue-bots) designed by other students are added to the environment. We will hold occasional simulation contests to test the efficiency of students' controllers as well as their safety. The 6th and final lab will be open-ended, allowing students to creatively demonstrate what they have learned.
Lab Schedule
Here is an outline of the lab schedule:- Lab 1a: Robot on Rails (Autobots, Roll Out)
- Lab 1b: Robot on Rails (Charging Station)
- Lab 2a: Follow the Leader, Robot on Highways (with event-driven control)
- Lab 2b: Follow the Leader, Robot on Highways (with time-triggered control)
- Lab 3a: Robot on Racetracks (stay on the circular racetrack)
- Lab 3b: Robot on Racetracks (slow down to avoid collisions)
- Lab 4a: Robot in a Plane (motion with obstacle avoidance)
- Lab 4b: Robot in a Plane (avoiding collisions with Roguebot and moving obstacles)
- Final project lab 6: Robot in Star-lab (self-defined course project entering the CPS V&V Grand Prix
 |  |
 |  |
 |
Betabots and Veribots
Before you submit your final robot (your Veribot), you will also submit a Betabot, which is a beta-version of your robot controller that you conjecture to be safe. Unlike your final robot submission, the Veribot, your Betabot does not need to be verified. In later labs, you may also have the opportunity to submit Rogue-Bots, which are robot controllers that make life difficult for the robots submitted by the other students. So we hope the course will be fun. And that you will learn to distinguish safe from unsafe CPS designs.Lab Illustrations
The robot controllers that you implement will be autonomous controllers that have to work under all circumstances. Below we just show a few example scenarios with a particular example of an obstacle.
| Lab 1a | Autobots, Roll Out |
|---|---|
 |
|
| Lab 1b | Charging Station |
 |
|
| Lab 2 | Follow the Leader |
|
|
| Lab 3 | Robots on Racetracks |
|
|
| Lab 4a | Static Obstacles |
|
|
| Lab 4b | Dynamic Obstacles |
 |
|
Lab Schedule
The Lab and Assignment Schedule is tentative!Collaboration and Academic Integrity
The university policies and procedures on academic integrity will be applied rigorously.
All work, including theory, lab assignments, models and proofs, you submit must be your own. All labs in this course must be done either by a single student or by a pair of students, at your discretion. The work must be your own and your partner's. Consulting another student's solution is prohibited. Do not look at other student's models or proofs. Do not make parts of your models or proofs available to anyone. Make sure no one else can read your files. Make repositories private if you use public source control hosts like github.
Please read the University Policy on Academic Integrity carefully to understand the penalties associated with academic dishonesty at CMU. In this class, cheating/copying/plagiarism means copying all or part of a program or homework solution, model, or proof from another student or unauthorized source such as the Internet, knowingly giving such information to another student, or giving or receiving unauthorized information during an examination. In general, each solution you submit (written assignment, lab assignment, model, proof, midterm or final exam) must be your own work. In the event that you use information by another person in your solution, you must cite the source of this information (and receive prior permission if unsure whether this is permitted). It is considered cheating to compare or discuss complete or partial solutions.
It is not considered cheating to clarify vague points in the labs, assignments, or lecture material, or to give help or receive help in general use of the computer systems or tools such as KeYmaera, or other facilities. It is permitted and encouraged to share general advice on how to use KeYmaera or general discussions about course assignments. Any assistance, though, must be limited to discussion of the problems in general, and cannot be about the solutions of the assignments. Public dissemination of your advice on Piazza is encouraged to ensure that all students can see it.
Due Dates
Labs will be submitted electronically via Autolab. Labs have two different due dates, the Betabots and the Veribots. Betabots are due at the beginning of class on the Betabot due date. Veribots are due by 22:00 on the day the lab is due. You have a total of 5 late days for the semester of which you can use at most 2 per veribot assignment (no late days can be used for Betabots nor for the final project). If you submit beyond those late days, 30% will be docked on an assignment for each additional late day.
Written assignments will be collected at the beginning of class on the date they are due. There are no late days for written assignments. If you submit after a written assignment is due, 50% will be docked on a written assignment for each late day. If you have an excused absence on an assignment due date, email TAs in advance to arrange an alternative drop off.
Extra Points for Proof Exploits
All feedback about how to improve the lecture notes and KeYmaera X is always very welcome. There is one form of feedback that is particularly helpful: feedback that concernes soundness.
Soundness is crucial and fundamental, but of special significance for the high stakes of cyber-physical systems. What good would a safety analysis of a broken cyber-physical system do if the analysis procedure itself is broken?
To reflect that, we are soliciting Proof Exploits. By which we mean proofs that exploit soundness-critical flaws in the lecture notes and soundness-critical bugs in KeYmaera X. Each new soundness-critical bug that you are the first person to report is worth 10 points of extra credit. For full credit you should also demonstrate with a proof exploit how that bug can be exploited to produce a proof of false. A proof exploit is a formal proof on paper or a test case for KeYmaera X demonstrating how the flaw can be exploited to exhibit a proof of false, which, since false is rarely true, cannot have a proof in any sound verification procedure.
Needless to say that this is not just a great way for you to earn extra credit but also a really solid preparation for questions scrutinizing what rules and axioms and proof attempts are sound and which ones aren't. Which is an invaluable skill when it comes down to analyzing CPSs.
We will award a special prize during the CPS V&V Grand Prix to the person achieving the most extra credit via proof exploits.