Formal methods and machine learning together have the potential to enhance technologies for education. In this thesis, we consider the problem of designing CPSGrader, an automatic grader for laboratory-based courses in the area of cyber-physical systems. The work is motivated by a UC Berkeley course in which students program a robot for specified navigation tasks. Given a candidate student solution (control program for the robot), CPSGrader first checks whether the robot performs the task correctly under a representative set of environment conditions. If it does not, CPSGrader automatically generates feedback hinting at possible errors in the program. CPSGrader is based on a novel notion of constrained parameterized tests based on signal temporal logic (STL) that capture symptoms pointing to success or causes of failure in traces obtained from a realistic simulator. We define and solve the problem of synthesizing constraints on a parameterized test such that it is consistent with a set of reference solutions with and without the desired symptom. We also develop a clustering-based active learning technique that selects from a large database of unlabeled solutions, a small number of reference solutions for the expert to label. The goal is to achieve better accuracy of fault identification with fewer reference solutions as compared to random selection. We demonstrate the effectiveness of CPSGrader using two data sets: one obtained from an on-campus laboratory-based course at UC Berkeley, and the other from a massive open online course (MOOC) offering. In addition, CPSGrader was successfully deployed in the laboratory section of this MOOC on the edX platform.




Download Full History