CPSGrader is an automatic grading and feedback
generation tool (auto-grader) for laboratory
courses
developed at the University of California, Berkeley.
CPSGrader uses temporal logics with quantative semantics,
such as Metric Temporal Logic (MTL) or Signal Temporal Logic (STL)
to define test
benches to monitor simulation traces of student
solutions for mistakes/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 first version of our auto-grader is an
independent library written in C++ that can plug into any
simulator via an API, and our first version of the test bench synthesis is done
in MATLAB using the Breach toolbox. Our newer auto-grader has been
developed using the pyMTL and
Scenic software tools.
Deployment
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.
CPSGrader has also been used on campus at Berkeley in the course "Introduction to Embedded Systems", and the newer version has been used to run a remote/virtual laboratory for this class during the COVID-19 pandemic.
Copyright ©2014-2020, Sanjit A. Seshia, Alexandre Donzé, Garvit Juniwal, Jeff C. Jensen, Bernard Chen, Edward Kim, Hazem Torfah, and Victoria Tuck. All rights reserved. CPSGrader is licensed under the BSD-3-clause license.
This work has been 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), by the NSF VeHICaL project (CNS-1545126), and by National Instruments Corporation.
