CPSGrader is an automatic grading and feedback generation tool (auto-grader) for laboratory courses developed at the University of California, Berkeley. CPSGrader uses Signal Temporal Logic (STL) based test benches to monitor simulation traces of student solutions for faults. It is designed to work with any black-box simulator. The test benches in CPSGrader are "parameterized" to be robust to certain allowed variations in student solutions. Each test bench serves as a classifier to detect presence/absence of a particular kind of fault and we automatically synthesize the classification boundaries (in terms of ranges of test bench parameters) using a sample set of previously known correct and faulty solutions. The auto-grader is an independent library written in C++ that can plug into any simulator via an API, and the test bench synthesis is done in MATLAB using the Breach toolbox.
CPSGrader was used in conjunction with the physics-based simulation driven virtual robotics laboratory (CyberSim) for the laboratory component of the online Cyber-Physical Systems MOOC EECS 149.1x offered on edX. This is the first online course to use a physics-based virtual robotics laboratory and the first deployed auto-grader that uses formal verification. We received very positive feedback about the tool with 86% students reporting that the debugging information generated by CPSGrader was crucial for solving the lab exercises. CPSGrader is a significant step in furthering the broader agenda of use of formal methods in making engineering education fun and scalable to large number of students across the world.
Copyright ©2014, Alexandre Donzé, Garvit Juniwal, Jeff C. Jensen, and Sanjit A. Seshia. All rights reserved. CPSGrader is licensed under the BSD-3-clause license.
This work was supported in part by TerraSwarm, one of the six centers of STARnet, a Semiconductor Research Corporation program sponsored by DARPA, by the NSF ExCAPE project (CCF-1139138), and by National Instruments Corporation.